This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rlmvsca

Description: Scalar multiplication in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015)

		Ref	Expression
	Assertion	rlmvsca	$⊢ \cdot_{R} = \cdot_{ringLMod (R)}$

Step	Hyp	Ref	Expression
1		rlmval	$⊢ ringLMod (R) = subringAlg (R) ({Base}_{R})$
2	1	a1i	$⊢ ⊤ \to ringLMod (R) = subringAlg (R) ({Base}_{R})$
3		ssidd	$⊢ ⊤ \to {Base}_{R} \subseteq {Base}_{R}$
4	2 3	sravsca	$⊢ ⊤ \to \cdot_{R} = \cdot_{ringLMod (R)}$
5	4	mptru	$⊢ \cdot_{R} = \cdot_{ringLMod (R)}$