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	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
	mgpsca.s	⊢ 𝑆 = ( Scalar ‘ 𝑅 )
Assertion	mgpsca	⊢ 𝑆 = ( Scalar ‘ 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		mgpbas.1	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
2		mgpsca.s	⊢ 𝑆 = ( Scalar ‘ 𝑅 )
3		df-sca	⊢ Scalar = Slot 5
4		5nn	⊢ 5 ∈ ℕ
5		2re	⊢ 2 ∈ ℝ
6		2lt5	⊢ 2 < 5
7	5 6	gtneii	⊢ 5 ≠ 2
8	1 3 4 7	mgplem	⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑀 )
9	2 8	eqtri	⊢ 𝑆 = ( Scalar ‘ 𝑀 )