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	$⊢ \underset{˙}{0} = 0_{R}$
	0unit.3	$⊢ \underset{˙}{1} = 1_{R}$
Assertion	0unit	$⊢ R \in Ring \to (\underset{˙}{0} \in U \leftrightarrow \underset{˙}{1} = \underset{˙}{0})$

Step	Hyp	Ref	Expression
1		0unit.1	$⊢ U = Unit (R)$
2		0unit.2	$⊢ \underset{˙}{0} = 0_{R}$
3		0unit.3	$⊢ \underset{˙}{1} = 1_{R}$
4		eqid	$⊢ {inv}_{r} (R) = {inv}_{r} (R)$
5		eqid	$⊢ \cdot_{R} = \cdot_{R}$
6	1 4 5 3	unitrinv	$⊢ (R \in Ring \land \underset{˙}{0} \in U) \to \underset{˙}{0} \cdot_{R} {inv}_{r} (R) (\underset{˙}{0}) = \underset{˙}{1}$
7		eqid	$⊢ {Base}_{R} = {Base}_{R}$
8	1 4 7	ringinvcl	$⊢ (R \in Ring \land \underset{˙}{0} \in U) \to {inv}_{r} (R) (\underset{˙}{0}) \in {Base}_{R}$
9	7 5 2	ringlz	$⊢ (R \in Ring \land {inv}_{r} (R) (\underset{˙}{0}) \in {Base}_{R}) \to \underset{˙}{0} \cdot_{R} {inv}_{r} (R) (\underset{˙}{0}) = \underset{˙}{0}$
10	8 9	syldan	$⊢ (R \in Ring \land \underset{˙}{0} \in U) \to \underset{˙}{0} \cdot_{R} {inv}_{r} (R) (\underset{˙}{0}) = \underset{˙}{0}$
11	6 10	eqtr3d	$⊢ (R \in Ring \land \underset{˙}{0} \in U) \to \underset{˙}{1} = \underset{˙}{0}$
12		simpr	$⊢ (R \in Ring \land \underset{˙}{1} = \underset{˙}{0}) \to \underset{˙}{1} = \underset{˙}{0}$
13	1 3	1unit	$⊢ R \in Ring \to \underset{˙}{1} \in U$
14	13	adantr	$⊢ (R \in Ring \land \underset{˙}{1} = \underset{˙}{0}) \to \underset{˙}{1} \in U$
15	12 14	eqeltrrd	$⊢ (R \in Ring \land \underset{˙}{1} = \underset{˙}{0}) \to \underset{˙}{0} \in U$
16	11 15	impbida	$⊢ R \in Ring \to (\underset{˙}{0} \in U \leftrightarrow \underset{˙}{1} = \underset{˙}{0})$

Metamath Proof Explorer