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

Metamath Proof Explorer

Theorem mxidlmax

Description: A maximal ideal is a maximal proper ideal. (Contributed by Jeff Madsen, 16-Jun-2011) (Revised by Thierry Arnoux, 19-Jan-2024)

Ref Expression
Hypothesis mxidlval.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion mxidlmax ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑀 ⊆ 𝐼 ) ) → ( 𝐼 = 𝑀 ∨ 𝐼 = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 mxidlval.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 sseq2 ⊢ ( 𝑗 = 𝐼 → ( 𝑀 ⊆ 𝑗 ↔ 𝑀 ⊆ 𝐼 ) )
3 eqeq1 ⊢ ( 𝑗 = 𝐼 → ( 𝑗 = 𝑀 ↔ 𝐼 = 𝑀 ) )
4 eqeq1 ⊢ ( 𝑗 = 𝐼 → ( 𝑗 = 𝐵 ↔ 𝐼 = 𝐵 ) )
5 3 4 orbi12d ⊢ ( 𝑗 = 𝐼 → ( ( 𝑗 = 𝑀 ∨ 𝑗 = 𝐵 ) ↔ ( 𝐼 = 𝑀 ∨ 𝐼 = 𝐵 ) ) )
6 2 5 imbi12d ⊢ ( 𝑗 = 𝐼 → ( ( 𝑀 ⊆ 𝑗 → ( 𝑗 = 𝑀 ∨ 𝑗 = 𝐵 ) ) ↔ ( 𝑀 ⊆ 𝐼 → ( 𝐼 = 𝑀 ∨ 𝐼 = 𝐵 ) ) ) )
7 1 ismxidl ⊢ ( 𝑅 ∈ Ring → ( 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ↔ ( 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑀 ≠ 𝐵 ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀 ⊆ 𝑗 → ( 𝑗 = 𝑀 ∨ 𝑗 = 𝐵 ) ) ) ) )
8 7 biimpa ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ( 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑀 ≠ 𝐵 ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀 ⊆ 𝑗 → ( 𝑗 = 𝑀 ∨ 𝑗 = 𝐵 ) ) ) )
9 8 simp3d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀 ⊆ 𝑗 → ( 𝑗 = 𝑀 ∨ 𝑗 = 𝐵 ) ) )
10 9 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀 ⊆ 𝑗 → ( 𝑗 = 𝑀 ∨ 𝑗 = 𝐵 ) ) )
11 simpr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
12 6 10 11 rspcdva ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 𝑀 ⊆ 𝐼 → ( 𝐼 = 𝑀 ∨ 𝐼 = 𝐵 ) ) )
13 12 impr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑀 ⊆ 𝐼 ) ) → ( 𝐼 = 𝑀 ∨ 𝐼 = 𝐵 ) )