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

Metamath Proof Explorer

Theorem 0unit

Description: The additive identity is a unit if and only if 1 = 0 , i.e. we are in the zero ring. (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Hypotheses 0unit.1 
|- U = ( Unit ` R )
0unit.2 
|- .0. = ( 0g ` R )
0unit.3 
|- .1. = ( 1r ` R )
Assertion 0unit 
|- ( R e. Ring -> ( .0. e. U <-> .1. = .0. ) )

Proof

Step Hyp Ref Expression
1 0unit.1 
 |-  U = ( Unit ` R )
2 0unit.2 
 |-  .0. = ( 0g ` R )
3 0unit.3 
 |-  .1. = ( 1r ` R )
4 eqid 
 |-  ( invr ` R ) = ( invr ` R )
5 eqid 
 |-  ( .r ` R ) = ( .r ` R )
6 1 4 5 3 unitrinv 
 |-  ( ( R e. Ring /\ .0. e. U ) -> ( .0. ( .r ` R ) ( ( invr ` R ) ` .0. ) ) = .1. )
7 eqid 
 |-  ( Base ` R ) = ( Base ` R )
8 1 4 7 ringinvcl 
 |-  ( ( R e. Ring /\ .0. e. U ) -> ( ( invr ` R ) ` .0. ) e. ( Base ` R ) )
9 7 5 2 ringlz 
 |-  ( ( R e. Ring /\ ( ( invr ` R ) ` .0. ) e. ( Base ` R ) ) -> ( .0. ( .r ` R ) ( ( invr ` R ) ` .0. ) ) = .0. )
10 8 9 syldan 
 |-  ( ( R e. Ring /\ .0. e. U ) -> ( .0. ( .r ` R ) ( ( invr ` R ) ` .0. ) ) = .0. )
11 6 10 eqtr3d 
 |-  ( ( R e. Ring /\ .0. e. U ) -> .1. = .0. )
12 simpr 
 |-  ( ( R e. Ring /\ .1. = .0. ) -> .1. = .0. )
13 1 3 1unit 
 |-  ( R e. Ring -> .1. e. U )
14 13 adantr 
 |-  ( ( R e. Ring /\ .1. = .0. ) -> .1. e. U )
15 12 14 eqeltrrd 
 |-  ( ( R e. Ring /\ .1. = .0. ) -> .0. e. U )
16 11 15 impbida 
 |-  ( R e. Ring -> ( .0. e. U <-> .1. = .0. ) )