Metamath Proof Explorer


Theorem mgpsca

Description: The multiplication monoid has the same (if any) scalars as the original ring. Mostly to simplify pwsmgp . (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Mario Carneiro, 5-May-2015)

Ref Expression
Hypotheses mgpbas.1 M = mulGrp R
mgpsca.s S = Scalar R
Assertion mgpsca S = Scalar M

Proof

Step Hyp Ref Expression
1 mgpbas.1 M = mulGrp R
2 mgpsca.s S = Scalar R
3 eqid R = R
4 1 3 mgpval M = R sSet + ndx R
5 scaid Scalar = Slot Scalar ndx
6 scandxnplusgndx Scalar ndx + ndx
7 4 5 6 setsplusg Scalar R = Scalar M
8 2 7 eqtri S = Scalar M