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 ⊢ O = opp r ⁡ R
oppr2idl.2 ⊢ φ → R ∈ Ring
Assertion opprlidlabs ⊢ φ → LIdeal ⁡ R = LIdeal ⁡ opp r ⁡ O

Proof

Step Hyp Ref Expression
1 oppreqg.o ⊢ O = opp r ⁡ R
2 oppr2idl.2 ⊢ φ → R ∈ Ring
3 eqid ⊢ Base O = Base O
4 eqid ⊢ ⋅ O = ⋅ O
5 eqid ⊢ opp r ⁡ O = opp r ⁡ O
6 eqid ⊢ ⋅ opp r ⁡ O = ⋅ opp r ⁡ O
7 3 4 5 6 opprmul ⊢ x ⋅ opp r ⁡ O a = a ⋅ O x
8 eqid ⊢ Base R = Base R
9 eqid ⊢ ⋅ R = ⋅ R
10 8 9 1 4 opprmul ⊢ a ⋅ O x = x ⋅ R a
11 7 10 eqtr2i ⊢ x ⋅ R a = x ⋅ opp r ⁡ O a
12 11 a1i ⊢ φ ∧ x ∈ Base R ∧ a ∈ i ∧ b ∈ i → x ⋅ R a = x ⋅ opp r ⁡ O a
13 12 oveq1d ⊢ φ ∧ x ∈ Base R ∧ a ∈ i ∧ b ∈ i → x ⋅ R a + R b = x ⋅ opp r ⁡ O a + R b
14 13 eleq1d ⊢ φ ∧ x ∈ Base R ∧ a ∈ i ∧ b ∈ i → x ⋅ R a + R b ∈ i ↔ x ⋅ opp r ⁡ O a + R b ∈ i
15 14 ralbidva ⊢ φ ∧ x ∈ Base R ∧ a ∈ i → ∀ b ∈ i x ⋅ R a + R b ∈ i ↔ ∀ b ∈ i x ⋅ opp r ⁡ O a + R b ∈ i
16 15 anasss ⊢ φ ∧ x ∈ Base R ∧ a ∈ i → ∀ b ∈ i x ⋅ R a + R b ∈ i ↔ ∀ b ∈ i x ⋅ opp r ⁡ O a + R b ∈ i
17 16 2ralbidva ⊢ φ → ∀ x ∈ Base R ∀ a ∈ i ∀ b ∈ i x ⋅ R a + R b ∈ i ↔ ∀ x ∈ Base R ∀ a ∈ i ∀ b ∈ i x ⋅ opp r ⁡ O a + R b ∈ i
18 17 3anbi3d ⊢ φ → i ⊆ Base R ∧ i ≠ ∅ ∧ ∀ x ∈ Base R ∀ a ∈ i ∀ b ∈ i x ⋅ R a + R b ∈ i ↔ i ⊆ Base R ∧ i ≠ ∅ ∧ ∀ x ∈ Base R ∀ a ∈ i ∀ b ∈ i x ⋅ opp r ⁡ O a + R b ∈ i
19 eqid ⊢ LIdeal ⁡ R = LIdeal ⁡ R
20 eqid ⊢ + R = + R
21 19 8 20 9 islidl ⊢ i ∈ LIdeal ⁡ R ↔ i ⊆ Base R ∧ i ≠ ∅ ∧ ∀ x ∈ Base R ∀ a ∈ i ∀ b ∈ i x ⋅ R a + R b ∈ i
22 eqid ⊢ LIdeal ⁡ opp r ⁡ O = LIdeal ⁡ opp r ⁡ O
23 1 8 opprbas ⊢ Base R = Base O
24 5 23 opprbas ⊢ Base R = Base opp r ⁡ O
25 1 20 oppradd ⊢ + R = + O
26 5 25 oppradd ⊢ + R = + opp r ⁡ O
27 22 24 26 6 islidl ⊢ i ∈ LIdeal ⁡ opp r ⁡ O ↔ i ⊆ Base R ∧ i ≠ ∅ ∧ ∀ x ∈ Base R ∀ a ∈ i ∀ b ∈ i x ⋅ opp r ⁡ O a + R b ∈ i
28 18 21 27 3bitr4g ⊢ φ → i ∈ LIdeal ⁡ R ↔ i ∈ LIdeal ⁡ opp r ⁡ O
29 28 eqrdv ⊢ φ → LIdeal ⁡ R = LIdeal ⁡ opp r ⁡ O