Metamath Proof Explorer

Theorem crngmxidl

Description: In a commutative ring, maximal ideals of the opposite ring coincide with maximal ideals. (Contributed by Thierry Arnoux, 13-Mar-2025)

Ref Expression
Hypotheses crngmxidl.i ⊢ M = MaxIdeal ⁡ R
crngmxidl.o ⊢ O = opp r ⁡ R
Assertion crngmxidl ⊢ R ∈ CRing → M = MaxIdeal ⁡ O

Proof

Step Hyp Ref Expression
1 crngmxidl.i ⊢ M = MaxIdeal ⁡ R
2 crngmxidl.o ⊢ O = opp r ⁡ R
3 1 eleq2i ⊢ m ∈ M ↔ m ∈ MaxIdeal ⁡ R
4 eqid ⊢ LIdeal ⁡ R = LIdeal ⁡ R
5 4 2 crngridl ⊢ R ∈ CRing → LIdeal ⁡ R = LIdeal ⁡ O
6 5 eleq2d ⊢ R ∈ CRing → m ∈ LIdeal ⁡ R ↔ m ∈ LIdeal ⁡ O
7 5 raleqdv ⊢ R ∈ CRing → ∀ j ∈ LIdeal ⁡ R m ⊆ j → j = m ∨ j = Base R ↔ ∀ j ∈ LIdeal ⁡ O m ⊆ j → j = m ∨ j = Base R
8 6 7 3anbi13d ⊢ R ∈ CRing → m ∈ LIdeal ⁡ R ∧ m ≠ Base R ∧ ∀ j ∈ LIdeal ⁡ R m ⊆ j → j = m ∨ j = Base R ↔ m ∈ LIdeal ⁡ O ∧ m ≠ Base R ∧ ∀ j ∈ LIdeal ⁡ O m ⊆ j → j = m ∨ j = Base R
9 crngring ⊢ R ∈ CRing → R ∈ Ring
10 eqid ⊢ Base R = Base R
11 10 ismxidl ⊢ R ∈ Ring → m ∈ MaxIdeal ⁡ R ↔ m ∈ LIdeal ⁡ R ∧ m ≠ Base R ∧ ∀ j ∈ LIdeal ⁡ R m ⊆ j → j = m ∨ j = Base R
12 9 11 syl ⊢ R ∈ CRing → m ∈ MaxIdeal ⁡ R ↔ m ∈ LIdeal ⁡ R ∧ m ≠ Base R ∧ ∀ j ∈ LIdeal ⁡ R m ⊆ j → j = m ∨ j = Base R
13 2 opprring ⊢ R ∈ Ring → O ∈ Ring
14 2 10 opprbas ⊢ Base R = Base O
15 14 ismxidl ⊢ O ∈ Ring → m ∈ MaxIdeal ⁡ O ↔ m ∈ LIdeal ⁡ O ∧ m ≠ Base R ∧ ∀ j ∈ LIdeal ⁡ O m ⊆ j → j = m ∨ j = Base R
16 9 13 15 3syl ⊢ R ∈ CRing → m ∈ MaxIdeal ⁡ O ↔ m ∈ LIdeal ⁡ O ∧ m ≠ Base R ∧ ∀ j ∈ LIdeal ⁡ O m ⊆ j → j = m ∨ j = Base R
17 8 12 16 3bitr4d ⊢ R ∈ CRing → m ∈ MaxIdeal ⁡ R ↔ m ∈ MaxIdeal ⁡ O
18 3 17 bitrid ⊢ R ∈ CRing → m ∈ M ↔ m ∈ MaxIdeal ⁡ O
19 18 eqrdv ⊢ R ∈ CRing → M = MaxIdeal ⁡ O