Theorem unitgrpbas

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

	Ref	Expression
Hypotheses	unitmulcl.1	|- U = ( Unit ` R )
	unitgrp.2	|- G = ( ( mulGrp ` R ) |`s U )
Assertion	unitgrpbas	|- U = ( Base ` G )

Proof

Step	Hyp	Ref	Expression
1		unitmulcl.1	|- U = ( Unit ` R )
2		unitgrp.2	|- G = ( ( mulGrp ` R ) |`s U )
3		eqid	|- ( Base ` R ) = ( Base ` R )
4	3 1	unitss	|- U C_ ( Base ` R )
5		eqid	|- ( mulGrp ` R ) = ( mulGrp ` R )
6	5 3	mgpbas	|- ( Base ` R ) = ( Base ` ( mulGrp ` R ) )
7	2 6	ressbas2	|- ( U C_ ( Base ` R ) -> U = ( Base ` G ) )
8	4 7	ax-mp	|- U = ( Base ` G )