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