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

Metamath Proof Explorer

Theorem isridlrng

Description: A right ideal is a left ideal of the opposite non-unital ring. This theorem shows that this definition corresponds to the usual textbook definition of a right ideal of a ring to be a subgroup of the additive group of the ring which is closed under right-multiplication by elements of the full ring. (Contributed by AV, 21-Mar-2025)

Ref Expression
Hypotheses isridlrng.u 
|- U = ( LIdeal ` ( oppR ` R ) )
isridlrng.b 
|- B = ( Base ` R )
isridlrng.t 
|- .x. = ( .r ` R )
Assertion isridlrng 
|- ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) -> ( I e. U <-> A. x e. B A. y e. I ( y .x. x ) e. I ) )

Proof

Step Hyp Ref Expression
1 isridlrng.u 
 |-  U = ( LIdeal ` ( oppR ` R ) )
2 isridlrng.b 
 |-  B = ( Base ` R )
3 isridlrng.t 
 |-  .x. = ( .r ` R )
4 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
5 4 opprrng 
 |-  ( R e. Rng -> ( oppR ` R ) e. Rng )
6 4 opprsubg 
 |-  ( SubGrp ` R ) = ( SubGrp ` ( oppR ` R ) )
7 6 a1i 
 |-  ( R e. Rng -> ( SubGrp ` R ) = ( SubGrp ` ( oppR ` R ) ) )
8 7 eleq2d 
 |-  ( R e. Rng -> ( I e. ( SubGrp ` R ) <-> I e. ( SubGrp ` ( oppR ` R ) ) ) )
9 8 biimpa 
 |-  ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) -> I e. ( SubGrp ` ( oppR ` R ) ) )
10 4 2 opprbas 
 |-  B = ( Base ` ( oppR ` R ) )
11 eqid 
 |-  ( .r ` ( oppR ` R ) ) = ( .r ` ( oppR ` R ) )
12 1 10 11 dflidl2rng 
 |-  ( ( ( oppR ` R ) e. Rng /\ I e. ( SubGrp ` ( oppR ` R ) ) ) -> ( I e. U <-> A. x e. B A. y e. I ( x ( .r ` ( oppR ` R ) ) y ) e. I ) )
13 5 9 12 syl2an2r 
 |-  ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) -> ( I e. U <-> A. x e. B A. y e. I ( x ( .r ` ( oppR ` R ) ) y ) e. I ) )
14 2 3 4 11 opprmul 
 |-  ( x ( .r ` ( oppR ` R ) ) y ) = ( y .x. x )
15 14 eleq1i 
 |-  ( ( x ( .r ` ( oppR ` R ) ) y ) e. I <-> ( y .x. x ) e. I )
16 15 a1i 
 |-  ( ( ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) /\ x e. B ) /\ y e. I ) -> ( ( x ( .r ` ( oppR ` R ) ) y ) e. I <-> ( y .x. x ) e. I ) )
17 16 ralbidva 
 |-  ( ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) /\ x e. B ) -> ( A. y e. I ( x ( .r ` ( oppR ` R ) ) y ) e. I <-> A. y e. I ( y .x. x ) e. I ) )
18 17 ralbidva 
 |-  ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) -> ( A. x e. B A. y e. I ( x ( .r ` ( oppR ` R ) ) y ) e. I <-> A. x e. B A. y e. I ( y .x. x ) e. I ) )
19 13 18 bitrd 
 |-  ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) -> ( I e. U <-> A. x e. B A. y e. I ( y .x. x ) e. I ) )