Theorem unitgrpbas

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

	Ref	Expression
Hypotheses	unitmulcl.1	⊢ 𝑈 = ( Unit ‘ 𝑅 )
	unitgrp.2	⊢ 𝐺 = ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 )
Assertion	unitgrpbas	⊢ 𝑈 = ( Base ‘ 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		unitmulcl.1	⊢ 𝑈 = ( Unit ‘ 𝑅 )
2		unitgrp.2	⊢ 𝐺 = ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 )
3		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4	3 1	unitss	⊢ 𝑈 ⊆ ( Base ‘ 𝑅 )
5		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
6	5 3	mgpbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
7	2 6	ressbas2	⊢ ( 𝑈 ⊆ ( Base ‘ 𝑅 ) → 𝑈 = ( Base ‘ 𝐺 ) )
8	4 7	ax-mp	⊢ 𝑈 = ( Base ‘ 𝐺 )