lmod0vs

Description: Zero times a vector is the zero vector. Equation 1a of Kreyszig p. 51. ( ax-hvmul0 analog.) (Contributed by NM, 12-Jan-2014) (Revised by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	lmod0vs.v	$⊢ V = {Base}_{W}$
	lmod0vs.f	$⊢ F = Scalar (W)$
	lmod0vs.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	lmod0vs.o	$⊢ O = 0_{F}$
	lmod0vs.z	$⊢ \underset{˙}{0} = 0_{W}$
Assertion	lmod0vs	$⊢ (W \in LMod \land X \in V) \to O \underset{˙}{\cdot} X = \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		lmod0vs.v	$⊢ V = {Base}_{W}$
2		lmod0vs.f	$⊢ F = Scalar (W)$
3		lmod0vs.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
4		lmod0vs.o	$⊢ O = 0_{F}$
5		lmod0vs.z	$⊢ \underset{˙}{0} = 0_{W}$
6		simpl	$⊢ (W \in LMod \land X \in V) \to W \in LMod$
7	2	lmodring	$⊢ W \in LMod \to F \in Ring$
8	7	adantr	$⊢ (W \in LMod \land X \in V) \to F \in Ring$
9		eqid	$⊢ {Base}_{F} = {Base}_{F}$
10	9 4	ring0cl	$⊢ F \in Ring \to O \in {Base}_{F}$
11	8 10	syl	$⊢ (W \in LMod \land X \in V) \to O \in {Base}_{F}$
12		simpr	$⊢ (W \in LMod \land X \in V) \to X \in V$
13		eqid	$⊢ +_{W} = +_{W}$
14		eqid	$⊢ +_{F} = +_{F}$
15	1 13 2 3 9 14	lmodvsdir	$⊢ (W \in LMod \land (O \in {Base}_{F} \land O \in {Base}_{F} \land X \in V)) \to (O +_{F} O) \underset{˙}{\cdot} X = (O \underset{˙}{\cdot} X) +_{W} (O \underset{˙}{\cdot} X)$
16	6 11 11 12 15	syl13anc	$⊢ (W \in LMod \land X \in V) \to (O +_{F} O) \underset{˙}{\cdot} X = (O \underset{˙}{\cdot} X) +_{W} (O \underset{˙}{\cdot} X)$
17		ringgrp	$⊢ F \in Ring \to F \in Grp$
18	8 17	syl	$⊢ (W \in LMod \land X \in V) \to F \in Grp$
19	9 14 4	grplid	$⊢ (F \in Grp \land O \in {Base}_{F}) \to O +_{F} O = O$
20	18 11 19	syl2anc	$⊢ (W \in LMod \land X \in V) \to O +_{F} O = O$
21	20	oveq1d	$⊢ (W \in LMod \land X \in V) \to (O +_{F} O) \underset{˙}{\cdot} X = O \underset{˙}{\cdot} X$
22	16 21	eqtr3d	$⊢ (W \in LMod \land X \in V) \to (O \underset{˙}{\cdot} X) +_{W} (O \underset{˙}{\cdot} X) = O \underset{˙}{\cdot} X$
23	1 2 3 9	lmodvscl	$⊢ (W \in LMod \land O \in {Base}_{F} \land X \in V) \to O \underset{˙}{\cdot} X \in V$
24	6 11 12 23	syl3anc	$⊢ (W \in LMod \land X \in V) \to O \underset{˙}{\cdot} X \in V$
25	1 13 5	lmod0vid	$⊢ (W \in LMod \land O \underset{˙}{\cdot} X \in V) \to ((O \underset{˙}{\cdot} X) +_{W} (O \underset{˙}{\cdot} X) = O \underset{˙}{\cdot} X \leftrightarrow \underset{˙}{0} = O \underset{˙}{\cdot} X)$
26	24 25	syldan	$⊢ (W \in LMod \land X \in V) \to ((O \underset{˙}{\cdot} X) +_{W} (O \underset{˙}{\cdot} X) = O \underset{˙}{\cdot} X \leftrightarrow \underset{˙}{0} = O \underset{˙}{\cdot} X)$
27	22 26	mpbid	$⊢ (W \in LMod \land X \in V) \to \underset{˙}{0} = O \underset{˙}{\cdot} X$
28	27	eqcomd	$⊢ (W \in LMod \land X \in V) \to O \underset{˙}{\cdot} X = \underset{˙}{0}$

Metamath Proof Explorer

Theorem lmod0vs

Proof