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	|- G = ( 1st ` R )
	maxidln0.2	|- H = ( 2nd ` R )
	maxidln0.3	|- Z = ( GId ` G )
	maxidln0.4	|- U = ( GId ` H )
Assertion	maxidln0	|- ( ( R e. RingOps /\ M e. ( MaxIdl ` R ) ) -> U =/= Z )

Proof

Step	Hyp	Ref	Expression
1		maxidln0.1	|- G = ( 1st ` R )
2		maxidln0.2	|- H = ( 2nd ` R )
3		maxidln0.3	|- Z = ( GId ` G )
4		maxidln0.4	|- U = ( GId ` H )
5		maxidlidl	|- ( ( R e. RingOps /\ M e. ( MaxIdl ` R ) ) -> M e. ( Idl ` R ) )
6	1 3	idl0cl	|- ( ( R e. RingOps /\ M e. ( Idl ` R ) ) -> Z e. M )
7	5 6	syldan	|- ( ( R e. RingOps /\ M e. ( MaxIdl ` R ) ) -> Z e. M )
8	2 4	maxidln1	|- ( ( R e. RingOps /\ M e. ( MaxIdl ` R ) ) -> -. U e. M )
9		nelneq	|- ( ( Z e. M /\ -. U e. M ) -> -. Z = U )
10	7 8 9	syl2anc	|- ( ( R e. RingOps /\ M e. ( MaxIdl ` R ) ) -> -. Z = U )
11	10	neqned	|- ( ( R e. RingOps /\ M e. ( MaxIdl ` R ) ) -> Z =/= U )
12	11	necomd	|- ( ( R e. RingOps /\ M e. ( MaxIdl ` R ) ) -> U =/= Z )