Theorem 1unit

Description: The multiplicative identity is a unit. (Contributed by Mario Carneiro, 1-Dec-2014)

	Ref	Expression
Hypotheses	unit.1	$$⊢U=\mathrm{Unit}\left(R\right)$$
	unit.2	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	1unit	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in U$$

Proof

Step	Hyp	Ref	Expression
1		unit.1	$$⊢U=\mathrm{Unit}\left(R\right)$$
2		unit.2	$$⊢\underset{\dot{}}{1}=1_R$$
3		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
4	3 2	ringidcl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_R$$
5		eqid	$$⊢{\parallel }_r\left(R\right)={\parallel }_r\left(R\right)$$
6	3 5	dvdsrid	$$⊢\left(R\in \mathrm{Ring}\wedge \underset{\dot{}}{1}\in {\mathrm{Base}}_R\right)\to \underset{\dot{}}{1}{\parallel }_r\left(R\right)\underset{\dot{}}{1}$$
7	4 6	mpdan	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}{\parallel }_r\left(R\right)\underset{\dot{}}{1}$$
8		eqid	$$⊢{opp}_r\left(R\right)={opp}_r\left(R\right)$$
9	8	opprring	$$⊢R\in \mathrm{Ring}\to {opp}_r\left(R\right)\in \mathrm{Ring}$$
10	8 3	opprbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{{opp}_r\left(R\right)}$$
11		eqid	$$⊢{\parallel }_r\left({opp}_r\left(R\right)\right)={\parallel }_r\left({opp}_r\left(R\right)\right)$$
12	10 11	dvdsrid	$$⊢\left({opp}_r\left(R\right)\in \mathrm{Ring}\wedge \underset{\dot{}}{1}\in {\mathrm{Base}}_R\right)\to \underset{\dot{}}{1}{\parallel }_r\left({opp}_r\left(R\right)\right)\underset{\dot{}}{1}$$
13	9 4 12	syl2anc	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}{\parallel }_r\left({opp}_r\left(R\right)\right)\underset{\dot{}}{1}$$
14	1 2 5 8 11	isunit	$$⊢\underset{\dot{}}{1}\in U\leftrightarrow \left(\underset{\dot{}}{1}{\parallel }_r\left(R\right)\underset{\dot{}}{1}\wedge \underset{\dot{}}{1}{\parallel }_r\left({opp}_r\left(R\right)\right)\underset{\dot{}}{1}\right)$$
15	7 13 14	sylanbrc	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in U$$