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

Metamath Proof Explorer

Theorem isridl

Description: A right ideal is a left ideal of the opposite 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, 13-Feb-2025)

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

Proof

Step Hyp Ref Expression
1 isridl.u 
 |-  U = ( LIdeal ` ( oppR ` R ) )
2 isridl.b 
 |-  B = ( Base ` R )
3 isridl.t 
 |-  .x. = ( .r ` R )
4 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
5 4 opprring 
 |-  ( R e. Ring -> ( oppR ` R ) e. Ring )
6 4 2 opprbas 
 |-  B = ( Base ` ( oppR ` R ) )
7 eqid 
 |-  ( .r ` ( oppR ` R ) ) = ( .r ` ( oppR ` R ) )
8 1 6 7 dflidl2 
 |-  ( ( oppR ` R ) e. Ring -> ( I e. U <-> ( I e. ( SubGrp ` ( oppR ` R ) ) /\ A. x e. B A. y e. I ( x ( .r ` ( oppR ` R ) ) y ) e. I ) ) )
9 5 8 syl 
 |-  ( R e. Ring -> ( I e. U <-> ( I e. ( SubGrp ` ( oppR ` R ) ) /\ A. x e. B A. y e. I ( x ( .r ` ( oppR ` R ) ) y ) e. I ) ) )
10 4 opprsubg 
 |-  ( SubGrp ` R ) = ( SubGrp ` ( oppR ` R ) )
11 10 eqcomi 
 |-  ( SubGrp ` ( oppR ` R ) ) = ( SubGrp ` R )
12 11 a1i 
 |-  ( R e. Ring -> ( SubGrp ` ( oppR ` R ) ) = ( SubGrp ` R ) )
13 12 eleq2d 
 |-  ( R e. Ring -> ( I e. ( SubGrp ` ( oppR ` R ) ) <-> I e. ( SubGrp ` R ) ) )
14 2 3 4 7 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. Ring /\ x e. B ) /\ y e. I ) -> ( ( x ( .r ` ( oppR ` R ) ) y ) e. I <-> ( y .x. x ) e. I ) )
17 16 ralbidva 
 |-  ( ( R e. Ring /\ 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. Ring -> ( 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 anbi12d 
 |-  ( R e. Ring -> ( ( I e. ( SubGrp ` ( oppR ` R ) ) /\ A. x e. B A. y e. I ( x ( .r ` ( oppR ` R ) ) y ) e. I ) <-> ( I e. ( SubGrp ` R ) /\ A. x e. B A. y e. I ( y .x. x ) e. I ) ) )
20 9 19 bitrd 
 |-  ( R e. Ring -> ( I e. U <-> ( I e. ( SubGrp ` R ) /\ A. x e. B A. y e. I ( y .x. x ) e. I ) ) )