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=\mathrm{Unit}\left(R\right)$$
	0unit.2	$$⊢\underset{\dot{}}{0}=0_R$$
	0unit.3	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	0unit	$$⊢R\in \mathrm{Ring}\to \left(\underset{\dot{}}{0}\in U\leftrightarrow \underset{\dot{}}{1}=\underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		0unit.1	$$⊢U=\mathrm{Unit}\left(R\right)$$
2		0unit.2	$$⊢\underset{\dot{}}{0}=0_R$$
3		0unit.3	$$⊢\underset{\dot{}}{1}=1_R$$
4		eqid	$$⊢{inv}_r\left(R\right)={inv}_r\left(R\right)$$
5		eqid	$$⊢{\cdot }_R={\cdot }_R$$
6	1 4 5 3	unitrinv	$$⊢\left(R\in \mathrm{Ring}\wedge \underset{\dot{}}{0}\in U\right)\to \underset{\dot{}}{0}{\cdot }_R{inv}_r\left(R\right)\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{1}$$
7		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
8	1 4 7	ringinvcl	$$⊢\left(R\in \mathrm{Ring}\wedge \underset{\dot{}}{0}\in U\right)\to {inv}_r\left(R\right)\left(\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_R$$
9	7 5 2	ringlz	$$⊢\left(R\in \mathrm{Ring}\wedge {inv}_r\left(R\right)\left(\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_R\right)\to \underset{\dot{}}{0}{\cdot }_R{inv}_r\left(R\right)\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
10	8 9	syldan	$$⊢\left(R\in \mathrm{Ring}\wedge \underset{\dot{}}{0}\in U\right)\to \underset{\dot{}}{0}{\cdot }_R{inv}_r\left(R\right)\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
11	6 10	eqtr3d	$$⊢\left(R\in \mathrm{Ring}\wedge \underset{\dot{}}{0}\in U\right)\to \underset{\dot{}}{1}=\underset{\dot{}}{0}$$
12		simpr	$$⊢\left(R\in \mathrm{Ring}\wedge \underset{\dot{}}{1}=\underset{\dot{}}{0}\right)\to \underset{\dot{}}{1}=\underset{\dot{}}{0}$$
13	1 3	1unit	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in U$$
14	13	adantr	$$⊢\left(R\in \mathrm{Ring}\wedge \underset{\dot{}}{1}=\underset{\dot{}}{0}\right)\to \underset{\dot{}}{1}\in U$$
15	12 14	eqeltrrd	$$⊢\left(R\in \mathrm{Ring}\wedge \underset{\dot{}}{1}=\underset{\dot{}}{0}\right)\to \underset{\dot{}}{0}\in U$$
16	11 15	impbida	$$⊢R\in \mathrm{Ring}\to \left(\underset{\dot{}}{0}\in U\leftrightarrow \underset{\dot{}}{1}=\underset{\dot{}}{0}\right)$$