Step |
Hyp |
Ref |
Expression |
1 |
|
crng2idl.i |
⊢ 𝐼 = ( LIdeal ‘ 𝑅 ) |
2 |
|
inidm |
⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼 |
3 |
|
eqid |
⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 ) |
4 |
1 3
|
crngridl |
⊢ ( 𝑅 ∈ CRing → 𝐼 = ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ) |
5 |
4
|
ineq2d |
⊢ ( 𝑅 ∈ CRing → ( 𝐼 ∩ 𝐼 ) = ( 𝐼 ∩ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ) ) |
6 |
2 5
|
eqtr3id |
⊢ ( 𝑅 ∈ CRing → 𝐼 = ( 𝐼 ∩ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ) ) |
7 |
|
eqid |
⊢ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) = ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) |
8 |
|
eqid |
⊢ ( 2Ideal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 ) |
9 |
1 3 7 8
|
2idlval |
⊢ ( 2Ideal ‘ 𝑅 ) = ( 𝐼 ∩ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ) |
10 |
6 9
|
eqtr4di |
⊢ ( 𝑅 ∈ CRing → 𝐼 = ( 2Ideal ‘ 𝑅 ) ) |