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 ‘ 𝑂 ) )