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

Metamath Proof Explorer

Theorem maxidlmax

Description: A maximal ideal is a maximal proper ideal. (Contributed by Jeff Madsen, 16-Jun-2011)

Ref Expression
Hypotheses maxidlnr.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
maxidlnr.2 ⊢ 𝑋 = ran 𝐺
Assertion maxidlmax ( ( ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑀 ⊆ 𝐼 ) ) → ( 𝐼 = 𝑀 ∨ 𝐼 = 𝑋 ) )

Proof

Step Hyp Ref Expression
1 maxidlnr.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 maxidlnr.2 ⊢ 𝑋 = ran 𝐺
3 1 2 ismaxidl ⊢ ( 𝑅 ∈ RingOps → ( 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ↔ ( 𝑀 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑀 ≠ 𝑋 ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑀 ⊆ 𝑗 → ( 𝑗 = 𝑀 ∨ 𝑗 = 𝑋 ) ) ) ) )
4 3 biimpa ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ) → ( 𝑀 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑀 ≠ 𝑋 ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑀 ⊆ 𝑗 → ( 𝑗 = 𝑀 ∨ 𝑗 = 𝑋 ) ) ) )
5 4 simp3d ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ) → ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑀 ⊆ 𝑗 → ( 𝑗 = 𝑀 ∨ 𝑗 = 𝑋 ) ) )
6 sseq2 ⊢ ( 𝑗 = 𝐼 → ( 𝑀 ⊆ 𝑗 ↔ 𝑀 ⊆ 𝐼 ) )
7 eqeq1 ⊢ ( 𝑗 = 𝐼 → ( 𝑗 = 𝑀 ↔ 𝐼 = 𝑀 ) )
8 eqeq1 ⊢ ( 𝑗 = 𝐼 → ( 𝑗 = 𝑋 ↔ 𝐼 = 𝑋 ) )
9 7 8 orbi12d ⊢ ( 𝑗 = 𝐼 → ( ( 𝑗 = 𝑀 ∨ 𝑗 = 𝑋 ) ↔ ( 𝐼 = 𝑀 ∨ 𝐼 = 𝑋 ) ) )
10 6 9 imbi12d ⊢ ( 𝑗 = 𝐼 → ( ( 𝑀 ⊆ 𝑗 → ( 𝑗 = 𝑀 ∨ 𝑗 = 𝑋 ) ) ↔ ( 𝑀 ⊆ 𝐼 → ( 𝐼 = 𝑀 ∨ 𝐼 = 𝑋 ) ) ) )
11 10 rspcva ⊢ ( ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑀 ⊆ 𝑗 → ( 𝑗 = 𝑀 ∨ 𝑗 = 𝑋 ) ) ) → ( 𝑀 ⊆ 𝐼 → ( 𝐼 = 𝑀 ∨ 𝐼 = 𝑋 ) ) )
12 5 11 sylan2 ⊢ ( ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ) ) → ( 𝑀 ⊆ 𝐼 → ( 𝐼 = 𝑀 ∨ 𝐼 = 𝑋 ) ) )
13 12 ancoms ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ) ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → ( 𝑀 ⊆ 𝐼 → ( 𝐼 = 𝑀 ∨ 𝐼 = 𝑋 ) ) )
14 13 impr ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑀 ⊆ 𝐼 ) ) → ( 𝐼 = 𝑀 ∨ 𝐼 = 𝑋 ) )