Metamath Proof Explorer

Theorem crngridl

Description: In a commutative ring, the left and right ideals coincide. (Contributed by Mario Carneiro, 14-Jun-2015)

Ref Expression
Hypotheses crng2idl.i 
|- I = ( LIdeal ` R )
crngridl.o 
|- O = ( oppR ` R )
Assertion crngridl 
|- ( R e. CRing -> I = ( LIdeal ` O ) )

Proof

Step Hyp Ref Expression
1 crng2idl.i 
 |-  I = ( LIdeal ` R )
2 crngridl.o 
 |-  O = ( oppR ` R )
3 eqidd 
 |-  ( R e. CRing -> ( Base ` R ) = ( Base ` R ) )
4 eqid 
 |-  ( Base ` R ) = ( Base ` R )
5 2 4 opprbas 
 |-  ( Base ` R ) = ( Base ` O )
6 5 a1i 
 |-  ( R e. CRing -> ( Base ` R ) = ( Base ` O ) )
7 ssv 
 |-  ( Base ` R ) C_ _V
8 7 a1i 
 |-  ( R e. CRing -> ( Base ` R ) C_ _V )
9 eqid 
 |-  ( +g ` R ) = ( +g ` R )
10 2 9 oppradd 
 |-  ( +g ` R ) = ( +g ` O )
11 10 oveqi 
 |-  ( x ( +g ` R ) y ) = ( x ( +g ` O ) y )
12 11 a1i 
 |-  ( ( R e. CRing /\ ( x e. _V /\ y e. _V ) ) -> ( x ( +g ` R ) y ) = ( x ( +g ` O ) y ) )
13 ovexd 
 |-  ( ( R e. CRing /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( x ( .r ` R ) y ) e. _V )
14 eqid 
 |-  ( .r ` R ) = ( .r ` R )
15 eqid 
 |-  ( .r ` O ) = ( .r ` O )
16 4 14 2 15 crngoppr 
 |-  ( ( R e. CRing /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( x ( .r ` R ) y ) = ( x ( .r ` O ) y ) )
17 16 3expb 
 |-  ( ( R e. CRing /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( x ( .r ` R ) y ) = ( x ( .r ` O ) y ) )
18 3 6 8 12 13 17 lidlrsppropd 
 |-  ( R e. CRing -> ( ( LIdeal ` R ) = ( LIdeal ` O ) /\ ( RSpan ` R ) = ( RSpan ` O ) ) )
19 18 simpld 
 |-  ( R e. CRing -> ( LIdeal ` R ) = ( LIdeal ` O ) )
20 1 19 syl5eq 
 |-  ( R e. CRing -> I = ( LIdeal ` O ) )