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

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 ⊢ 𝑀 = ( MaxIdeal ‘ 𝑅 )
crngmxidl.o ⊢ 𝑂 = ( oppr ‘ 𝑅 )
Assertion crngmxidl ( 𝑅 ∈ CRing → 𝑀 = ( MaxIdeal ‘ 𝑂 ) )

Proof

Step Hyp Ref Expression
1 crngmxidl.i ⊢ 𝑀 = ( MaxIdeal ‘ 𝑅 )
2 crngmxidl.o ⊢ 𝑂 = ( oppr ‘ 𝑅 )
3 1 eleq2i ⊢ ( 𝑚 ∈ 𝑀 ↔ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) )
4 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
5 4 2 crngridl ⊢ ( 𝑅 ∈ CRing → ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑂 ) )
6 5 eleq2d ⊢ ( 𝑅 ∈ CRing → ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ↔ 𝑚 ∈ ( LIdeal ‘ 𝑂 ) ) )
7 5 raleqdv ⊢ ( 𝑅 ∈ CRing → ( ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑚 ⊆ 𝑗 → ( 𝑗 = 𝑚 ∨ 𝑗 = ( Base ‘ 𝑅 ) ) ) ↔ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑂 ) ( 𝑚 ⊆ 𝑗 → ( 𝑗 = 𝑚 ∨ 𝑗 = ( Base ‘ 𝑅 ) ) ) ) )
8 6 7 3anbi13d ⊢ ( 𝑅 ∈ CRing → ( ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑚 ≠ ( Base ‘ 𝑅 ) ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑚 ⊆ 𝑗 → ( 𝑗 = 𝑚 ∨ 𝑗 = ( Base ‘ 𝑅 ) ) ) ) ↔ ( 𝑚 ∈ ( LIdeal ‘ 𝑂 ) ∧ 𝑚 ≠ ( Base ‘ 𝑅 ) ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑂 ) ( 𝑚 ⊆ 𝑗 → ( 𝑗 = 𝑚 ∨ 𝑗 = ( Base ‘ 𝑅 ) ) ) ) ) )
9 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
10 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
11 10 ismxidl ⊢ ( 𝑅 ∈ Ring → ( 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ↔ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑚 ≠ ( Base ‘ 𝑅 ) ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑚 ⊆ 𝑗 → ( 𝑗 = 𝑚 ∨ 𝑗 = ( Base ‘ 𝑅 ) ) ) ) ) )
12 9 11 syl ⊢ ( 𝑅 ∈ CRing → ( 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ↔ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑚 ≠ ( Base ‘ 𝑅 ) ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑚 ⊆ 𝑗 → ( 𝑗 = 𝑚 ∨ 𝑗 = ( Base ‘ 𝑅 ) ) ) ) ) )
13 2 opprring ⊢ ( 𝑅 ∈ Ring → 𝑂 ∈ Ring )
14 2 10 opprbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 )
15 14 ismxidl ⊢ ( 𝑂 ∈ Ring → ( 𝑚 ∈ ( MaxIdeal ‘ 𝑂 ) ↔ ( 𝑚 ∈ ( LIdeal ‘ 𝑂 ) ∧ 𝑚 ≠ ( Base ‘ 𝑅 ) ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑂 ) ( 𝑚 ⊆ 𝑗 → ( 𝑗 = 𝑚 ∨ 𝑗 = ( Base ‘ 𝑅 ) ) ) ) ) )
16 9 13 15 3syl ⊢ ( 𝑅 ∈ CRing → ( 𝑚 ∈ ( MaxIdeal ‘ 𝑂 ) ↔ ( 𝑚 ∈ ( LIdeal ‘ 𝑂 ) ∧ 𝑚 ≠ ( Base ‘ 𝑅 ) ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑂 ) ( 𝑚 ⊆ 𝑗 → ( 𝑗 = 𝑚 ∨ 𝑗 = ( Base ‘ 𝑅 ) ) ) ) ) )
17 8 12 16 3bitr4d ⊢ ( 𝑅 ∈ CRing → ( 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ↔ 𝑚 ∈ ( MaxIdeal ‘ 𝑂 ) ) )
18 3 17 bitrid ⊢ ( 𝑅 ∈ CRing → ( 𝑚 ∈ 𝑀 ↔ 𝑚 ∈ ( MaxIdeal ‘ 𝑂 ) ) )
19 18 eqrdv ⊢ ( 𝑅 ∈ CRing → 𝑀 = ( MaxIdeal ‘ 𝑂 ) )