This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oppr2idl

Description: Two sided ideal of the opposite ring. (Contributed by Thierry Arnoux, 9-Mar-2025)

Ref Expression
Hypotheses oppreqg.o ⊢ 𝑂 = ( oppr ‘ 𝑅 )
oppr2idl.2 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
Assertion oppr2idl ( 𝜑 → ( 2Ideal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑂 ) )

Proof

Step Hyp Ref Expression
1 oppreqg.o ⊢ 𝑂 = ( oppr ‘ 𝑅 )
2 oppr2idl.2 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
3 incom ⊢ ( ( LIdeal ‘ 𝑅 ) ∩ ( LIdeal ‘ 𝑂 ) ) = ( ( LIdeal ‘ 𝑂 ) ∩ ( LIdeal ‘ 𝑅 ) )
4 1 2 opprlidlabs ⊢ ( 𝜑 → ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ ( oppr ‘ 𝑂 ) ) )
5 4 ineq2d ⊢ ( 𝜑 → ( ( LIdeal ‘ 𝑂 ) ∩ ( LIdeal ‘ 𝑅 ) ) = ( ( LIdeal ‘ 𝑂 ) ∩ ( LIdeal ‘ ( oppr ‘ 𝑂 ) ) ) )
6 3 5 eqtrid ⊢ ( 𝜑 → ( ( LIdeal ‘ 𝑅 ) ∩ ( LIdeal ‘ 𝑂 ) ) = ( ( LIdeal ‘ 𝑂 ) ∩ ( LIdeal ‘ ( oppr ‘ 𝑂 ) ) ) )
7 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
8 eqid ⊢ ( LIdeal ‘ 𝑂 ) = ( LIdeal ‘ 𝑂 )
9 eqid ⊢ ( 2Ideal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 )
10 7 1 8 9 2idlval ⊢ ( 2Ideal ‘ 𝑅 ) = ( ( LIdeal ‘ 𝑅 ) ∩ ( LIdeal ‘ 𝑂 ) )
11 eqid ⊢ ( oppr ‘ 𝑂 ) = ( oppr ‘ 𝑂 )
12 eqid ⊢ ( LIdeal ‘ ( oppr ‘ 𝑂 ) ) = ( LIdeal ‘ ( oppr ‘ 𝑂 ) )
13 eqid ⊢ ( 2Ideal ‘ 𝑂 ) = ( 2Ideal ‘ 𝑂 )
14 8 11 12 13 2idlval ⊢ ( 2Ideal ‘ 𝑂 ) = ( ( LIdeal ‘ 𝑂 ) ∩ ( LIdeal ‘ ( oppr ‘ 𝑂 ) ) )
15 6 10 14 3eqtr4g ⊢ ( 𝜑 → ( 2Ideal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑂 ) )