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 𝐼 = ( LIdeal ‘ 𝑅 )
crngridl.o 𝑂 = ( oppr𝑅 )
Assertion crngridl ( 𝑅 ∈ CRing → 𝐼 = ( LIdeal ‘ 𝑂 ) )

Proof

Step Hyp Ref Expression
1 crng2idl.i 𝐼 = ( LIdeal ‘ 𝑅 )
2 crngridl.o 𝑂 = ( oppr𝑅 )
3 eqidd ( 𝑅 ∈ CRing → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) )
4 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5 2 4 opprbas ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 )
6 5 a1i ( 𝑅 ∈ CRing → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 ) )
7 ssv ( Base ‘ 𝑅 ) ⊆ V
8 7 a1i ( 𝑅 ∈ CRing → ( Base ‘ 𝑅 ) ⊆ V )
9 eqid ( +g𝑅 ) = ( +g𝑅 )
10 2 9 oppradd ( +g𝑅 ) = ( +g𝑂 )
11 10 oveqi ( 𝑥 ( +g𝑅 ) 𝑦 ) = ( 𝑥 ( +g𝑂 ) 𝑦 )
12 11 a1i ( ( 𝑅 ∈ CRing ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) → ( 𝑥 ( +g𝑅 ) 𝑦 ) = ( 𝑥 ( +g𝑂 ) 𝑦 ) )
13 ovexd ( ( 𝑅 ∈ CRing ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ V )
14 eqid ( .r𝑅 ) = ( .r𝑅 )
15 eqid ( .r𝑂 ) = ( .r𝑂 )
16 4 14 2 15 crngoppr ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( .r𝑅 ) 𝑦 ) = ( 𝑥 ( .r𝑂 ) 𝑦 ) )
17 16 3expb ( ( 𝑅 ∈ CRing ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 ( .r𝑅 ) 𝑦 ) = ( 𝑥 ( .r𝑂 ) 𝑦 ) )
18 3 6 8 12 13 17 lidlrsppropd ( 𝑅 ∈ CRing → ( ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑂 ) ∧ ( RSpan ‘ 𝑅 ) = ( RSpan ‘ 𝑂 ) ) )
19 18 simpld ( 𝑅 ∈ CRing → ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑂 ) )
20 1 19 syl5eq ( 𝑅 ∈ CRing → 𝐼 = ( LIdeal ‘ 𝑂 ) )