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

Metamath Proof Explorer

Theorem maxidlidl

Description: A maximal ideal is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011)

Ref Expression
Assertion maxidlidl ( ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ) → 𝑀 ∈ ( Idl ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( 1st ‘ 𝑅 ) = ( 1st ‘ 𝑅 )
2 eqid ⊢ ran ( 1st ‘ 𝑅 ) = ran ( 1st ‘ 𝑅 )
3 1 2 ismaxidl ⊢ ( 𝑅 ∈ RingOps → ( 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ↔ ( 𝑀 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑀 ≠ ran ( 1st ‘ 𝑅 ) ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑀 ⊆ 𝑗 → ( 𝑗 = 𝑀 ∨ 𝑗 = ran ( 1st ‘ 𝑅 ) ) ) ) ) )
4 3anass ⊢ ( ( 𝑀 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑀 ≠ ran ( 1st ‘ 𝑅 ) ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑀 ⊆ 𝑗 → ( 𝑗 = 𝑀 ∨ 𝑗 = ran ( 1st ‘ 𝑅 ) ) ) ) ↔ ( 𝑀 ∈ ( Idl ‘ 𝑅 ) ∧ ( 𝑀 ≠ ran ( 1st ‘ 𝑅 ) ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑀 ⊆ 𝑗 → ( 𝑗 = 𝑀 ∨ 𝑗 = ran ( 1st ‘ 𝑅 ) ) ) ) ) )
5 3 4 bitrdi ⊢ ( 𝑅 ∈ RingOps → ( 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ↔ ( 𝑀 ∈ ( Idl ‘ 𝑅 ) ∧ ( 𝑀 ≠ ran ( 1st ‘ 𝑅 ) ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑀 ⊆ 𝑗 → ( 𝑗 = 𝑀 ∨ 𝑗 = ran ( 1st ‘ 𝑅 ) ) ) ) ) ) )
6 5 simprbda ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ) → 𝑀 ∈ ( Idl ‘ 𝑅 ) )