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

Metamath Proof Explorer

Theorem opprmxidlabs

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

Ref Expression
Hypotheses oppreqg.o ⊢ 𝑂 = ( oppr ‘ 𝑅 )
oppr2idl.2 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
opprmxidl.3 ⊢ ( 𝜑 → 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) )
Assertion opprmxidlabs ( 𝜑 → 𝑀 ∈ ( MaxIdeal ‘ ( oppr ‘ 𝑂 ) ) )

Proof

Step Hyp Ref Expression
1 oppreqg.o ⊢ 𝑂 = ( oppr ‘ 𝑅 )
2 oppr2idl.2 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
3 opprmxidl.3 ⊢ ( 𝜑 → 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) )
4 1 opprring ⊢ ( 𝑅 ∈ Ring → 𝑂 ∈ Ring )
5 eqid ⊢ ( oppr ‘ 𝑂 ) = ( oppr ‘ 𝑂 )
6 5 opprring ⊢ ( 𝑂 ∈ Ring → ( oppr ‘ 𝑂 ) ∈ Ring )
7 2 4 6 3syl ⊢ ( 𝜑 → ( oppr ‘ 𝑂 ) ∈ Ring )
8 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9 8 mxidlidl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑀 ∈ ( LIdeal ‘ 𝑅 ) )
10 2 3 9 syl2anc ⊢ ( 𝜑 → 𝑀 ∈ ( LIdeal ‘ 𝑅 ) )
11 1 2 opprlidlabs ⊢ ( 𝜑 → ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ ( oppr ‘ 𝑂 ) ) )
12 10 11 eleqtrd ⊢ ( 𝜑 → 𝑀 ∈ ( LIdeal ‘ ( oppr ‘ 𝑂 ) ) )
13 8 mxidlnr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑀 ≠ ( Base ‘ 𝑅 ) )
14 2 3 13 syl2anc ⊢ ( 𝜑 → 𝑀 ≠ ( Base ‘ 𝑅 ) )
15 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( LIdeal ‘ ( oppr ‘ 𝑂 ) ) ) ∧ 𝑀 ⊆ 𝑗 ) → 𝑅 ∈ Ring )
16 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( LIdeal ‘ ( oppr ‘ 𝑂 ) ) ) ∧ 𝑀 ⊆ 𝑗 ) → 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) )
17 simplr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( LIdeal ‘ ( oppr ‘ 𝑂 ) ) ) ∧ 𝑀 ⊆ 𝑗 ) → 𝑗 ∈ ( LIdeal ‘ ( oppr ‘ 𝑂 ) ) )
18 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( LIdeal ‘ ( oppr ‘ 𝑂 ) ) ) ∧ 𝑀 ⊆ 𝑗 ) → ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ ( oppr ‘ 𝑂 ) ) )
19 17 18 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( LIdeal ‘ ( oppr ‘ 𝑂 ) ) ) ∧ 𝑀 ⊆ 𝑗 ) → 𝑗 ∈ ( LIdeal ‘ 𝑅 ) )
20 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( LIdeal ‘ ( oppr ‘ 𝑂 ) ) ) ∧ 𝑀 ⊆ 𝑗 ) → 𝑀 ⊆ 𝑗 )
21 8 mxidlmax ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ ( 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑀 ⊆ 𝑗 ) ) → ( 𝑗 = 𝑀 ∨ 𝑗 = ( Base ‘ 𝑅 ) ) )
22 15 16 19 20 21 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( LIdeal ‘ ( oppr ‘ 𝑂 ) ) ) ∧ 𝑀 ⊆ 𝑗 ) → ( 𝑗 = 𝑀 ∨ 𝑗 = ( Base ‘ 𝑅 ) ) )
23 22 ex ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( LIdeal ‘ ( oppr ‘ 𝑂 ) ) ) → ( 𝑀 ⊆ 𝑗 → ( 𝑗 = 𝑀 ∨ 𝑗 = ( Base ‘ 𝑅 ) ) ) )
24 23 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ ( LIdeal ‘ ( oppr ‘ 𝑂 ) ) ( 𝑀 ⊆ 𝑗 → ( 𝑗 = 𝑀 ∨ 𝑗 = ( Base ‘ 𝑅 ) ) ) )
25 1 8 opprbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 )
26 5 25 opprbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( oppr ‘ 𝑂 ) )
27 26 ismxidl ⊢ ( ( oppr ‘ 𝑂 ) ∈ Ring → ( 𝑀 ∈ ( MaxIdeal ‘ ( oppr ‘ 𝑂 ) ) ↔ ( 𝑀 ∈ ( LIdeal ‘ ( oppr ‘ 𝑂 ) ) ∧ 𝑀 ≠ ( Base ‘ 𝑅 ) ∧ ∀ 𝑗 ∈ ( LIdeal ‘ ( oppr ‘ 𝑂 ) ) ( 𝑀 ⊆ 𝑗 → ( 𝑗 = 𝑀 ∨ 𝑗 = ( Base ‘ 𝑅 ) ) ) ) ) )
28 27 biimpar ⊢ ( ( ( oppr ‘ 𝑂 ) ∈ Ring ∧ ( 𝑀 ∈ ( LIdeal ‘ ( oppr ‘ 𝑂 ) ) ∧ 𝑀 ≠ ( Base ‘ 𝑅 ) ∧ ∀ 𝑗 ∈ ( LIdeal ‘ ( oppr ‘ 𝑂 ) ) ( 𝑀 ⊆ 𝑗 → ( 𝑗 = 𝑀 ∨ 𝑗 = ( Base ‘ 𝑅 ) ) ) ) ) → 𝑀 ∈ ( MaxIdeal ‘ ( oppr ‘ 𝑂 ) ) )
29 7 12 14 24 28 syl13anc ⊢ ( 𝜑 → 𝑀 ∈ ( MaxIdeal ‘ ( oppr ‘ 𝑂 ) ) )