Theorem unitcl

Description: A unit is an element of the base set. (Contributed by Mario Carneiro, 1-Dec-2014)

	Ref	Expression
Hypotheses	unitcl.1	$$⊢B={\mathrm{Base}}_R$$
	unitcl.2	$$⊢U=\mathrm{Unit}\left(R\right)$$
Assertion	unitcl	$$⊢X\in U\to X\in B$$

Proof

Step	Hyp	Ref	Expression
1		unitcl.1	$$⊢B={\mathrm{Base}}_R$$
2		unitcl.2	$$⊢U=\mathrm{Unit}\left(R\right)$$
3		eqid	$$⊢1_R=1_R$$
4		eqid	$$⊢{\parallel }_r\left(R\right)={\parallel }_r\left(R\right)$$
5		eqid	$$⊢{opp}_r\left(R\right)={opp}_r\left(R\right)$$
6		eqid	$$⊢{\parallel }_r\left({opp}_r\left(R\right)\right)={\parallel }_r\left({opp}_r\left(R\right)\right)$$
7	2 3 4 5 6	isunit	$$⊢X\in U\leftrightarrow \left(X{\parallel }_r\left(R\right)1_R\wedge X{\parallel }_r\left({opp}_r\left(R\right)\right)1_R\right)$$
8	7	simplbi	$$⊢X\in U\to X{\parallel }_r\left(R\right)1_R$$
9	1 4	dvdsrcl	$$⊢X{\parallel }_r\left(R\right)1_R\to X\in B$$
10	8 9	syl	$$⊢X\in U\to X\in B$$