Theorem mgpscaOLD

Description: Obsolete version of mgpsca as of 18-Oct-2024. 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) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mgpbas.1	$$⊢M={\mathrm{mulGrp}}_R$$
	mgpsca.s	$$⊢S=\mathrm{Scalar}\left(R\right)$$
Assertion	mgpscaOLD	$$⊢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		df-sca	$$⊢\mathrm{Scalar}=\mathrm{Slot}5$$
4		5nn	$$⊢5\in \mathbb{N}$$
5		2re	$$⊢2\in ℝ$$
6		2lt5	$$⊢2<5$$
7	5 6	gtneii	$$⊢5\ne 2$$
8	1 3 4 7	mgplemOLD	$$⊢\mathrm{Scalar}\left(R\right)=\mathrm{Scalar}\left(M\right)$$
9	2 8	eqtri	$$⊢S=\mathrm{Scalar}\left(M\right)$$