Metamath Proof Explorer

Theorem ring1ne0

Description: If a ring has at least two elements, its one and zero are different. (Contributed by AV, 13-Apr-2019)

Ref Expression
Hypotheses ring1ne0.b 
|- B = ( Base ` R )
ring1ne0.u 
|- .1. = ( 1r ` R )
ring1ne0.z 
|- .0. = ( 0g ` R )
Assertion ring1ne0 
|- ( ( R e. Ring /\ 1 < ( # ` B ) ) -> .1. =/= .0. )

Proof

Step Hyp Ref Expression
1 ring1ne0.b 
 |-  B = ( Base ` R )
2 ring1ne0.u 
 |-  .1. = ( 1r ` R )
3 ring1ne0.z 
 |-  .0. = ( 0g ` R )
4 1 fvexi 
 |-  B e. _V
5 hashgt12el 
 |-  ( ( B e. _V /\ 1 < ( # ` B ) ) -> E. x e. B E. y e. B x =/= y )
6 4 5 mpan 
 |-  ( 1 < ( # ` B ) -> E. x e. B E. y e. B x =/= y )
7 6 adantl 
 |-  ( ( R e. Ring /\ 1 < ( # ` B ) ) -> E. x e. B E. y e. B x =/= y )
8 1 2 3 ring1eq0 
 |-  ( ( R e. Ring /\ x e. B /\ y e. B ) -> ( .1. = .0. -> x = y ) )
9 8 necon3d 
 |-  ( ( R e. Ring /\ x e. B /\ y e. B ) -> ( x =/= y -> .1. =/= .0. ) )
10 9 3expib 
 |-  ( R e. Ring -> ( ( x e. B /\ y e. B ) -> ( x =/= y -> .1. =/= .0. ) ) )
11 10 adantr 
 |-  ( ( R e. Ring /\ 1 < ( # ` B ) ) -> ( ( x e. B /\ y e. B ) -> ( x =/= y -> .1. =/= .0. ) ) )
12 11 com3l 
 |-  ( ( x e. B /\ y e. B ) -> ( x =/= y -> ( ( R e. Ring /\ 1 < ( # ` B ) ) -> .1. =/= .0. ) ) )
13 12 rexlimivv 
 |-  ( E. x e. B E. y e. B x =/= y -> ( ( R e. Ring /\ 1 < ( # ` B ) ) -> .1. =/= .0. ) )
14 7 13 mpcom 
 |-  ( ( R e. Ring /\ 1 < ( # ` B ) ) -> .1. =/= .0. )