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 
|- 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 )