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

Metamath Proof Explorer

Theorem maxidln1

Description: One is not contained in any maximal ideal. (Contributed by Jeff Madsen, 17-Jun-2011)

Ref Expression
Hypotheses maxidln1.1 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
maxidln1.2 ⊢ 𝑈 = ( GId ‘ 𝐻 )
Assertion maxidln1 ( ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ) → ¬ 𝑈 ∈ 𝑀 )

Proof

Step Hyp Ref Expression
1 maxidln1.1 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
2 maxidln1.2 ⊢ 𝑈 = ( GId ‘ 𝐻 )
3 eqid ⊢ ( 1st ‘ 𝑅 ) = ( 1st ‘ 𝑅 )
4 eqid ⊢ ran ( 1st ‘ 𝑅 ) = ran ( 1st ‘ 𝑅 )
5 3 4 maxidlnr ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ) → 𝑀 ≠ ran ( 1st ‘ 𝑅 ) )
6 maxidlidl ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ) → 𝑀 ∈ ( Idl ‘ 𝑅 ) )
7 3 1 4 2 1idl ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( Idl ‘ 𝑅 ) ) → ( 𝑈 ∈ 𝑀 ↔ 𝑀 = ran ( 1st ‘ 𝑅 ) ) )
8 7 necon3bbid ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( Idl ‘ 𝑅 ) ) → ( ¬ 𝑈 ∈ 𝑀 ↔ 𝑀 ≠ ran ( 1st ‘ 𝑅 ) ) )
9 6 8 syldan ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ) → ( ¬ 𝑈 ∈ 𝑀 ↔ 𝑀 ≠ ran ( 1st ‘ 𝑅 ) ) )
10 5 9 mpbird ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ) → ¬ 𝑈 ∈ 𝑀 )