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