lincvalsc0

Description: The linear combination where all scalars are 0. (Contributed by AV, 12-Apr-2019)

	Ref	Expression
Hypotheses	lincvalsc0.b	$⊢ B = {Base}_{M}$
	lincvalsc0.s	$⊢ S = Scalar (M)$
	lincvalsc0.0	$⊢ \underset{˙}{0} = 0_{S}$
	lincvalsc0.z	$⊢ Z = 0_{M}$
	lincvalsc0.f	$⊢ F = (x \in V ⟼ \underset{˙}{0})$
Assertion	lincvalsc0	$⊢ (M \in LMod \land V \in 𝒫 B) \to F linC (M) V = Z$

Proof

Step	Hyp	Ref	Expression
1		lincvalsc0.b	$⊢ B = {Base}_{M}$
2		lincvalsc0.s	$⊢ S = Scalar (M)$
3		lincvalsc0.0	$⊢ \underset{˙}{0} = 0_{S}$
4		lincvalsc0.z	$⊢ Z = 0_{M}$
5		lincvalsc0.f	$⊢ F = (x \in V ⟼ \underset{˙}{0})$
6		simpl	$⊢ (M \in LMod \land V \in 𝒫 B) \to M \in LMod$
7	2	eqcomi	$⊢ Scalar (M) = S$
8	7	fveq2i	$⊢ {Base}_{Scalar (M)} = {Base}_{S}$
9	2 8 3	lmod0cl	$⊢ M \in LMod \to \underset{˙}{0} \in {Base}_{Scalar (M)}$
10	9	adantr	$⊢ (M \in LMod \land V \in 𝒫 B) \to \underset{˙}{0} \in {Base}_{Scalar (M)}$
11	10	adantr	$⊢ ((M \in LMod \land V \in 𝒫 B) \land x \in V) \to \underset{˙}{0} \in {Base}_{Scalar (M)}$
12	11 5	fmptd	$⊢ (M \in LMod \land V \in 𝒫 B) \to F : V ⟶ {Base}_{Scalar (M)}$
13		fvexd	$⊢ M \in LMod \to {Base}_{Scalar (M)} \in V$
14		elmapg	$⊢ ({Base}_{Scalar (M)} \in V \land V \in 𝒫 B) \to (F \in ({Base}_{Scalar (M)}^{V}) \leftrightarrow F : V ⟶ {Base}_{Scalar (M)})$
15	13 14	sylan	$⊢ (M \in LMod \land V \in 𝒫 B) \to (F \in ({Base}_{Scalar (M)}^{V}) \leftrightarrow F : V ⟶ {Base}_{Scalar (M)})$
16	12 15	mpbird	$⊢ (M \in LMod \land V \in 𝒫 B) \to F \in ({Base}_{Scalar (M)}^{V})$
17	1	pweqi	$⊢ 𝒫 B = 𝒫 {Base}_{M}$
18	17	eleq2i	$⊢ V \in 𝒫 B \leftrightarrow V \in 𝒫 {Base}_{M}$
19	18	biimpi	$⊢ V \in 𝒫 B \to V \in 𝒫 {Base}_{M}$
20	19	adantl	$⊢ (M \in LMod \land V \in 𝒫 B) \to V \in 𝒫 {Base}_{M}$
21		lincval	$⊢ (M \in LMod \land F \in ({Base}_{Scalar (M)}^{V}) \land V \in 𝒫 {Base}_{M}) \to F linC (M) V = \underset{v \in V}{\sum_{M}} (F (v) \cdot_{M} v)$
22	6 16 20 21	syl3anc	$⊢ (M \in LMod \land V \in 𝒫 B) \to F linC (M) V = \underset{v \in V}{\sum_{M}} (F (v) \cdot_{M} v)$
23		simpr	$⊢ ((M \in LMod \land V \in 𝒫 B) \land v \in V) \to v \in V$
24	3	fvexi	$⊢ \underset{˙}{0} \in V$
25		eqidd	$⊢ x = v \to \underset{˙}{0} = \underset{˙}{0}$
26	25 5	fvmptg	$⊢ (v \in V \land \underset{˙}{0} \in V) \to F (v) = \underset{˙}{0}$
27	23 24 26	sylancl	$⊢ ((M \in LMod \land V \in 𝒫 B) \land v \in V) \to F (v) = \underset{˙}{0}$
28	27	oveq1d	$⊢ ((M \in LMod \land V \in 𝒫 B) \land v \in V) \to F (v) \cdot_{M} v = \underset{˙}{0} \cdot_{M} v$
29	6	adantr	$⊢ ((M \in LMod \land V \in 𝒫 B) \land v \in V) \to M \in LMod$
30		elelpwi	$⊢ (v \in V \land V \in 𝒫 B) \to v \in B$
31	30	expcom	$⊢ V \in 𝒫 B \to (v \in V \to v \in B)$
32	31	adantl	$⊢ (M \in LMod \land V \in 𝒫 B) \to (v \in V \to v \in B)$
33	32	imp	$⊢ ((M \in LMod \land V \in 𝒫 B) \land v \in V) \to v \in B$
34		eqid	$⊢ \cdot_{M} = \cdot_{M}$
35	1 2 34 3 4	lmod0vs	$⊢ (M \in LMod \land v \in B) \to \underset{˙}{0} \cdot_{M} v = Z$
36	29 33 35	syl2anc	$⊢ ((M \in LMod \land V \in 𝒫 B) \land v \in V) \to \underset{˙}{0} \cdot_{M} v = Z$
37	28 36	eqtrd	$⊢ ((M \in LMod \land V \in 𝒫 B) \land v \in V) \to F (v) \cdot_{M} v = Z$
38	37	mpteq2dva	$⊢ (M \in LMod \land V \in 𝒫 B) \to (v \in V ⟼ F (v) \cdot_{M} v) = (v \in V ⟼ Z)$
39	38	oveq2d	$⊢ (M \in LMod \land V \in 𝒫 B) \to \underset{v \in V}{\sum_{M}} (F (v) \cdot_{M} v) = \underset{v \in V}{\sum_{M}} Z$
40		lmodgrp	$⊢ M \in LMod \to M \in Grp$
41	40	grpmndd	$⊢ M \in LMod \to M \in Mnd$
42	4	gsumz	$⊢ (M \in Mnd \land V \in 𝒫 B) \to \underset{v \in V}{\sum_{M}} Z = Z$
43	41 42	sylan	$⊢ (M \in LMod \land V \in 𝒫 B) \to \underset{v \in V}{\sum_{M}} Z = Z$
44	22 39 43	3eqtrd	$⊢ (M \in LMod \land V \in 𝒫 B) \to F linC (M) V = Z$

Metamath Proof Explorer

Theorem lincvalsc0

Proof