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={\mathrm{mulGrp}}_R$$
	mgpsca.s	$$⊢S=\mathrm{Scalar}\left(R\right)$$
Assertion	mgpsca	$$⊢S=\mathrm{Scalar}\left(M\right)$$

Proof

Step	Hyp	Ref	Expression
1		mgpbas.1	$$⊢M={\mathrm{mulGrp}}_R$$
2		mgpsca.s	$$⊢S=\mathrm{Scalar}\left(R\right)$$
3		eqid	$$⊢{\cdot }_R={\cdot }_R$$
4	1 3	mgpval	$$⊢M=R\mathrm{sSet}⟨{+}_{\mathrm{ndx}},{\cdot }_R⟩$$
5		scaid	$$⊢\mathrm{Scalar}=\mathrm{Slot}\mathrm{Scalar}\left(\mathrm{ndx}\right)$$
6		scandxnplusgndx	$$⊢\mathrm{Scalar}\left(\mathrm{ndx}\right)\ne {+}_{\mathrm{ndx}}$$
7	4 5 6	setsplusg	$$⊢\mathrm{Scalar}\left(R\right)=\mathrm{Scalar}\left(M\right)$$
8	2 7	eqtri	$$⊢S=\mathrm{Scalar}\left(M\right)$$