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 ‘ 𝑅 ) ) → 𝑈 ≠ 𝑍 )