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