Theorem opprlidlabs

Description: The ideals of the opposite ring's opposite ring are the ideals of the original ring. (Contributed by Thierry Arnoux, 9-Mar-2025)

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

Proof

Step	Hyp	Ref	Expression
1		oppreqg.o	⊢ 𝑂 = ( oppr ‘ 𝑅 )
2		oppr2idl.2	⊢ ( 𝜑 → 𝑅 ∈ Ring )
3		eqid	⊢ ( Base ‘ 𝑂 ) = ( Base ‘ 𝑂 )
4		eqid	⊢ ( .r ‘ 𝑂 ) = ( .r ‘ 𝑂 )
5		eqid	⊢ ( oppr ‘ 𝑂 ) = ( oppr ‘ 𝑂 )
6		eqid	⊢ ( .r ‘ ( oppr ‘ 𝑂 ) ) = ( .r ‘ ( oppr ‘ 𝑂 ) )
7	3 4 5 6	opprmul	⊢ ( 𝑥 ( .r ‘ ( oppr ‘ 𝑂 ) ) 𝑎 ) = ( 𝑎 ( .r ‘ 𝑂 ) 𝑥 )
8		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
10	8 9 1 4	opprmul	⊢ ( 𝑎 ( .r ‘ 𝑂 ) 𝑥 ) = ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 )
11	7 10	eqtr2i	⊢ ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) = ( 𝑥 ( .r ‘ ( oppr ‘ 𝑂 ) ) 𝑎 )
12	11	a1i	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ 𝑖 ) ∧ 𝑏 ∈ 𝑖 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) = ( 𝑥 ( .r ‘ ( oppr ‘ 𝑂 ) ) 𝑎 ) )
13	12	oveq1d	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ 𝑖 ) ∧ 𝑏 ∈ 𝑖 ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) = ( ( 𝑥 ( .r ‘ ( oppr ‘ 𝑂 ) ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) )
14	13	eleq1d	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ 𝑖 ) ∧ 𝑏 ∈ 𝑖 ) → ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ↔ ( ( 𝑥 ( .r ‘ ( oppr ‘ 𝑂 ) ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) )
15	14	ralbidva	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ 𝑖 ) → ( ∀ 𝑏 ∈ 𝑖 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ↔ ∀ 𝑏 ∈ 𝑖 ( ( 𝑥 ( .r ‘ ( oppr ‘ 𝑂 ) ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) )
16	15	anasss	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ 𝑖 ) ) → ( ∀ 𝑏 ∈ 𝑖 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ↔ ∀ 𝑏 ∈ 𝑖 ( ( 𝑥 ( .r ‘ ( oppr ‘ 𝑂 ) ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) )
17	16	2ralbidva	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑎 ∈ 𝑖 ∀ 𝑏 ∈ 𝑖 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑎 ∈ 𝑖 ∀ 𝑏 ∈ 𝑖 ( ( 𝑥 ( .r ‘ ( oppr ‘ 𝑂 ) ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) )
18	17	3anbi3d	⊢ ( 𝜑 → ( ( 𝑖 ⊆ ( Base ‘ 𝑅 ) ∧ 𝑖 ≠ ∅ ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑎 ∈ 𝑖 ∀ 𝑏 ∈ 𝑖 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ↔ ( 𝑖 ⊆ ( Base ‘ 𝑅 ) ∧ 𝑖 ≠ ∅ ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑎 ∈ 𝑖 ∀ 𝑏 ∈ 𝑖 ( ( 𝑥 ( .r ‘ ( oppr ‘ 𝑂 ) ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ) )
19		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
20		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
21	19 8 20 9	islidl	⊢ ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↔ ( 𝑖 ⊆ ( Base ‘ 𝑅 ) ∧ 𝑖 ≠ ∅ ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑎 ∈ 𝑖 ∀ 𝑏 ∈ 𝑖 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) )
22		eqid	⊢ ( LIdeal ‘ ( oppr ‘ 𝑂 ) ) = ( LIdeal ‘ ( oppr ‘ 𝑂 ) )
23	1 8	opprbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 )
24	5 23	opprbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( oppr ‘ 𝑂 ) )
25	1 20	oppradd	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑂 )
26	5 25	oppradd	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ ( oppr ‘ 𝑂 ) )
27	22 24 26 6	islidl	⊢ ( 𝑖 ∈ ( LIdeal ‘ ( oppr ‘ 𝑂 ) ) ↔ ( 𝑖 ⊆ ( Base ‘ 𝑅 ) ∧ 𝑖 ≠ ∅ ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑎 ∈ 𝑖 ∀ 𝑏 ∈ 𝑖 ( ( 𝑥 ( .r ‘ ( oppr ‘ 𝑂 ) ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) )
28	18 21 27	3bitr4g	⊢ ( 𝜑 → ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↔ 𝑖 ∈ ( LIdeal ‘ ( oppr ‘ 𝑂 ) ) ) )
29	28	eqrdv	⊢ ( 𝜑 → ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ ( oppr ‘ 𝑂 ) ) )