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 = ( mulGrp ` R )
	mgpsca.s	|- S = ( Scalar ` R )
Assertion	mgpscaOLD	|- S = ( Scalar ` M )

Proof

Step	Hyp	Ref	Expression
1		mgpbas.1	|- M = ( mulGrp ` R )
2		mgpsca.s	|- S = ( Scalar ` R )
3		df-sca	|- Scalar = Slot 5
4		5nn	|- 5 e. NN
5		2re	|- 2 e. RR
6		2lt5	|- 2 < 5
7	5 6	gtneii	|- 5 =/= 2
8	1 3 4 7	mgplemOLD	|- ( Scalar ` R ) = ( Scalar ` M )
9	2 8	eqtri	|- S = ( Scalar ` M )