This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ↾ 𝑠 U
Assertion unitgrpbas ⊢ U = Base G

Proof

Step Hyp Ref Expression
1 unitmulcl.1 ⊢ U = Unit ⁡ R
2 unitgrp.2 ⊢ G = mulGrp R ↾ 𝑠 U
3 eqid ⊢ Base R = Base R
4 3 1 unitss ⊢ U ⊆ Base R
5 eqid ⊢ mulGrp R = mulGrp R
6 5 3 mgpbas ⊢ Base R = Base mulGrp R
7 2 6 ressbas2 ⊢ U ⊆ Base R → U = Base G
8 4 7 ax-mp ⊢ U = Base G