Theorem unitgrpbas

Description: The base set of the group of units. (Contributed by Mario Carneiro, 25-Dec-2014)

	Ref	Expression
Hypotheses	unitmulcl.1	$$⊢U=\mathrm{Unit}\left(R\right)$$
	unitgrp.2	$$⊢G={\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U$$
Assertion	unitgrpbas	$$⊢U={\mathrm{Base}}_G$$

Proof

Step	Hyp	Ref	Expression
1		unitmulcl.1	$$⊢U=\mathrm{Unit}\left(R\right)$$
2		unitgrp.2	$$⊢G={\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U$$
3		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
4	3 1	unitss	$$⊢U\subseteq {\mathrm{Base}}_R$$
5		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
6	5 3	mgpbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
7	2 6	ressbas2	$$⊢U\subseteq {\mathrm{Base}}_R\to U={\mathrm{Base}}_G$$
8	4 7	ax-mp	$$⊢U={\mathrm{Base}}_G$$