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

Metamath Proof Explorer

Theorem mgpbas

Description: Base set of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014) (Revised by Mario Carneiro, 5-Oct-2015)

Ref Expression
Hypotheses mgpbas.1 ⊢ M = mulGrp R
mgpbas.2 ⊢ B = Base R
Assertion mgpbas ⊢ B = Base M

Proof

Step Hyp Ref Expression
1 mgpbas.1 ⊢ M = mulGrp R
2 mgpbas.2 ⊢ B = Base R
3 eqid ⊢ ⋅ R = ⋅ R
4 1 3 mgpval ⊢ M = R sSet + ndx ⋅ R
5 baseid ⊢ Base = Slot Base ndx
6 basendxnplusgndx ⊢ Base ndx ≠ + ndx
7 4 5 6 setsplusg ⊢ Base R = Base M
8 2 7 eqtri ⊢ B = Base M