This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rngridlmcl

Description: A right ideal (which is a left ideal over the opposite ring) containing the zero element is closed under right-multiplication by elements of the full non-unital ring. (Contributed by AV, 19-Feb-2025)

Ref Expression
Hypotheses rnglidlmcl.z 
|- .0. = ( 0g ` R )
rnglidlmcl.b 
|- B = ( Base ` R )
rnglidlmcl.t 
|- .x. = ( .r ` R )
rngridlmcl.u 
|- U = ( LIdeal ` ( oppR ` R ) )
Assertion rngridlmcl 
|- ( ( ( R e. Rng /\ I e. U /\ .0. e. I ) /\ ( X e. B /\ Y e. I ) ) -> ( Y .x. X ) e. I )

Proof

Step Hyp Ref Expression
1 rnglidlmcl.z 
 |-  .0. = ( 0g ` R )
2 rnglidlmcl.b 
 |-  B = ( Base ` R )
3 rnglidlmcl.t 
 |-  .x. = ( .r ` R )
4 rngridlmcl.u 
 |-  U = ( LIdeal ` ( oppR ` R ) )
5 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
6 eqid 
 |-  ( .r ` ( oppR ` R ) ) = ( .r ` ( oppR ` R ) )
7 2 3 5 6 opprmul 
 |-  ( X ( .r ` ( oppR ` R ) ) Y ) = ( Y .x. X )
8 5 opprrng 
 |-  ( R e. Rng -> ( oppR ` R ) e. Rng )
9 id 
 |-  ( I e. U -> I e. U )
10 1 eleq1i 
 |-  ( .0. e. I <-> ( 0g ` R ) e. I )
11 10 biimpi 
 |-  ( .0. e. I -> ( 0g ` R ) e. I )
12 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
13 5 12 oppr0 
 |-  ( 0g ` R ) = ( 0g ` ( oppR ` R ) )
14 5 2 opprbas 
 |-  B = ( Base ` ( oppR ` R ) )
15 13 14 6 4 rnglidlmcl 
 |-  ( ( ( ( oppR ` R ) e. Rng /\ I e. U /\ ( 0g ` R ) e. I ) /\ ( X e. B /\ Y e. I ) ) -> ( X ( .r ` ( oppR ` R ) ) Y ) e. I )
16 8 9 11 15 syl3anl 
 |-  ( ( ( R e. Rng /\ I e. U /\ .0. e. I ) /\ ( X e. B /\ Y e. I ) ) -> ( X ( .r ` ( oppR ` R ) ) Y ) e. I )
17 7 16 eqeltrrid 
 |-  ( ( ( R e. Rng /\ I e. U /\ .0. e. I ) /\ ( X e. B /\ Y e. I ) ) -> ( Y .x. X ) e. I )