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

Metamath Proof Explorer

Theorem ring1eq0

Description: If one and zero are equal, then any two elements of a ring are equal. Alternately, every ring has one distinct from zero except the zero ring containing the single element { 0 } . (Contributed by Mario Carneiro, 10-Sep-2014)

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

Proof

Step Hyp Ref Expression
1 ring1eq0.b 
 |-  B = ( Base ` R )
2 ring1eq0.u 
 |-  .1. = ( 1r ` R )
3 ring1eq0.z 
 |-  .0. = ( 0g ` R )
4 simpr 
 |-  ( ( ( R e. Ring /\ X e. B /\ Y e. B ) /\ .1. = .0. ) -> .1. = .0. )
5 4 oveq1d 
 |-  ( ( ( R e. Ring /\ X e. B /\ Y e. B ) /\ .1. = .0. ) -> ( .1. ( .r ` R ) X ) = ( .0. ( .r ` R ) X ) )
6 4 oveq1d 
 |-  ( ( ( R e. Ring /\ X e. B /\ Y e. B ) /\ .1. = .0. ) -> ( .1. ( .r ` R ) Y ) = ( .0. ( .r ` R ) Y ) )
7 simpl1 
 |-  ( ( ( R e. Ring /\ X e. B /\ Y e. B ) /\ .1. = .0. ) -> R e. Ring )
8 simpl2 
 |-  ( ( ( R e. Ring /\ X e. B /\ Y e. B ) /\ .1. = .0. ) -> X e. B )
9 eqid 
 |-  ( .r ` R ) = ( .r ` R )
10 1 9 3 ringlz 
 |-  ( ( R e. Ring /\ X e. B ) -> ( .0. ( .r ` R ) X ) = .0. )
11 7 8 10 syl2anc 
 |-  ( ( ( R e. Ring /\ X e. B /\ Y e. B ) /\ .1. = .0. ) -> ( .0. ( .r ` R ) X ) = .0. )
12 simpl3 
 |-  ( ( ( R e. Ring /\ X e. B /\ Y e. B ) /\ .1. = .0. ) -> Y e. B )
13 1 9 3 ringlz 
 |-  ( ( R e. Ring /\ Y e. B ) -> ( .0. ( .r ` R ) Y ) = .0. )
14 7 12 13 syl2anc 
 |-  ( ( ( R e. Ring /\ X e. B /\ Y e. B ) /\ .1. = .0. ) -> ( .0. ( .r ` R ) Y ) = .0. )
15 11 14 eqtr4d 
 |-  ( ( ( R e. Ring /\ X e. B /\ Y e. B ) /\ .1. = .0. ) -> ( .0. ( .r ` R ) X ) = ( .0. ( .r ` R ) Y ) )
16 6 15 eqtr4d 
 |-  ( ( ( R e. Ring /\ X e. B /\ Y e. B ) /\ .1. = .0. ) -> ( .1. ( .r ` R ) Y ) = ( .0. ( .r ` R ) X ) )
17 5 16 eqtr4d 
 |-  ( ( ( R e. Ring /\ X e. B /\ Y e. B ) /\ .1. = .0. ) -> ( .1. ( .r ` R ) X ) = ( .1. ( .r ` R ) Y ) )
18 1 9 2 ringlidm 
 |-  ( ( R e. Ring /\ X e. B ) -> ( .1. ( .r ` R ) X ) = X )
19 7 8 18 syl2anc 
 |-  ( ( ( R e. Ring /\ X e. B /\ Y e. B ) /\ .1. = .0. ) -> ( .1. ( .r ` R ) X ) = X )
20 1 9 2 ringlidm 
 |-  ( ( R e. Ring /\ Y e. B ) -> ( .1. ( .r ` R ) Y ) = Y )
21 7 12 20 syl2anc 
 |-  ( ( ( R e. Ring /\ X e. B /\ Y e. B ) /\ .1. = .0. ) -> ( .1. ( .r ` R ) Y ) = Y )
22 17 19 21 3eqtr3d 
 |-  ( ( ( R e. Ring /\ X e. B /\ Y e. B ) /\ .1. = .0. ) -> X = Y )
23 22 ex 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( .1. = .0. -> X = Y ) )