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

Metamath Proof Explorer

Theorem rlmmulr

Description: Ring multiplication in the ring module. (Contributed by Mario Carneiro, 6-Oct-2015)

		Ref	Expression
	Assertion	rlmmulr	$⊢ \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	sramulr	$⊢ ⊤ \to \cdot_{R} = \cdot_{ringLMod (R)}$
5	4	mptru	$⊢ \cdot_{R} = \cdot_{ringLMod (R)}$