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

Metamath Proof Explorer

Theorem maxidln0

Description: A ring with a maximal ideal is not the zero ring. (Contributed by Jeff Madsen, 17-Jun-2011)

Ref Expression
Hypotheses maxidln0.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
maxidln0.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
maxidln0.3 ⊢ 𝑍 = ( GId ‘ 𝐺 )
maxidln0.4 ⊢ 𝑈 = ( GId ‘ 𝐻 )
Assertion maxidln0 ( ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ) → 𝑈 ≠ 𝑍 )

Proof

Step Hyp Ref Expression
1 maxidln0.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 maxidln0.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3 maxidln0.3 ⊢ 𝑍 = ( GId ‘ 𝐺 )
4 maxidln0.4 ⊢ 𝑈 = ( GId ‘ 𝐻 )
5 maxidlidl ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ) → 𝑀 ∈ ( Idl ‘ 𝑅 ) )
6 1 3 idl0cl ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( Idl ‘ 𝑅 ) ) → 𝑍 ∈ 𝑀 )
7 5 6 syldan ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ) → 𝑍 ∈ 𝑀 )
8 2 4 maxidln1 ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ) → ¬ 𝑈 ∈ 𝑀 )
9 nelneq ⊢ ( ( 𝑍 ∈ 𝑀 ∧ ¬ 𝑈 ∈ 𝑀 ) → ¬ 𝑍 = 𝑈 )
10 7 8 9 syl2anc ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ) → ¬ 𝑍 = 𝑈 )
11 10 neqned ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ) → 𝑍 ≠ 𝑈 )
12 11 necomd ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ) → 𝑈 ≠ 𝑍 )