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

Metamath Proof Explorer

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