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 ‘ 𝑅 ) ) → ¬ 𝑈𝑀 )