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

Metamath Proof Explorer

Theorem rlm0

Description: Zero vector in the ring module. (Contributed by Stefan O'Rear, 6-Dec-2014) (Revised by Mario Carneiro, 2-Oct-2015)

		Ref	Expression
	Assertion	rlm0	$⊢ 0_{R} = 0_{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		eqidd	$⊢ ⊤ \to 0_{R} = 0_{R}$
4		ssidd	$⊢ ⊤ \to {Base}_{R} \subseteq {Base}_{R}$
5	2 3 4	sralmod0	$⊢ ⊤ \to 0_{R} = 0_{ringLMod (R)}$
6	5	mptru	$⊢ 0_{R} = 0_{ringLMod (R)}$