linc0scn0

Description: If a set contains the zero element of a module, there is a linear combination being 0 where not all scalars are 0. (Contributed by AV, 13-Apr-2019)

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

Proof

Step	Hyp	Ref	Expression
1		linc0scn0.b	$⊢ B = {Base}_{M}$
2		linc0scn0.s	$⊢ S = Scalar (M)$
3		linc0scn0.0	$⊢ \underset{˙}{0} = 0_{S}$
4		linc0scn0.1	$⊢ \underset{˙}{1} = 1_{S}$
5		linc0scn0.z	$⊢ Z = 0_{M}$
6		linc0scn0.f	$⊢ F = (x \in V ⟼ if (x = Z, \underset{˙}{1}, \underset{˙}{0}))$
7		simpl	$⊢ (M \in LMod \land V \in 𝒫 B) \to M \in LMod$
8	2	lmodring	$⊢ M \in LMod \to S \in Ring$
9	2	eqcomi	$⊢ Scalar (M) = S$
10	9	fveq2i	$⊢ {Base}_{Scalar (M)} = {Base}_{S}$
11	10 4	ringidcl	$⊢ S \in Ring \to \underset{˙}{1} \in {Base}_{Scalar (M)}$
12	10 3	ring0cl	$⊢ S \in Ring \to \underset{˙}{0} \in {Base}_{Scalar (M)}$
13	11 12	jca	$⊢ S \in Ring \to (\underset{˙}{1} \in {Base}_{Scalar (M)} \land \underset{˙}{0} \in {Base}_{Scalar (M)})$
14	8 13	syl	$⊢ M \in LMod \to (\underset{˙}{1} \in {Base}_{Scalar (M)} \land \underset{˙}{0} \in {Base}_{Scalar (M)})$
15	14	ad2antrr	$⊢ ((M \in LMod \land V \in 𝒫 B) \land x \in V) \to (\underset{˙}{1} \in {Base}_{Scalar (M)} \land \underset{˙}{0} \in {Base}_{Scalar (M)})$
16		ifcl	$⊢ (\underset{˙}{1} \in {Base}_{Scalar (M)} \land \underset{˙}{0} \in {Base}_{Scalar (M)}) \to if (x = Z, \underset{˙}{1}, \underset{˙}{0}) \in {Base}_{Scalar (M)}$
17	15 16	syl	$⊢ ((M \in LMod \land V \in 𝒫 B) \land x \in V) \to if (x = Z, \underset{˙}{1}, \underset{˙}{0}) \in {Base}_{Scalar (M)}$
18	17 6	fmptd	$⊢ (M \in LMod \land V \in 𝒫 B) \to F : V ⟶ {Base}_{Scalar (M)}$
19		fvex	$⊢ {Base}_{Scalar (M)} \in V$
20	19	a1i	$⊢ M \in LMod \to {Base}_{Scalar (M)} \in V$
21		elmapg	$⊢ ({Base}_{Scalar (M)} \in V \land V \in 𝒫 B) \to (F \in ({Base}_{Scalar (M)}^{V}) \leftrightarrow F : V ⟶ {Base}_{Scalar (M)})$
22	20 21	sylan	$⊢ (M \in LMod \land V \in 𝒫 B) \to (F \in ({Base}_{Scalar (M)}^{V}) \leftrightarrow F : V ⟶ {Base}_{Scalar (M)})$
23	18 22	mpbird	$⊢ (M \in LMod \land V \in 𝒫 B) \to F \in ({Base}_{Scalar (M)}^{V})$
24	1	pweqi	$⊢ 𝒫 B = 𝒫 {Base}_{M}$
25	24	eleq2i	$⊢ V \in 𝒫 B \leftrightarrow V \in 𝒫 {Base}_{M}$
26	25	bilani	$⊢ (M \in LMod \land V \in 𝒫 B) \to V \in 𝒫 {Base}_{M}$
27		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)$
28	7 23 26 27	syl3anc	$⊢ (M \in LMod \land V \in 𝒫 B) \to F linC (M) V = \underset{v \in V}{\sum_{M}} (F (v) \cdot_{M} v)$
29		simpr	$⊢ ((M \in LMod \land V \in 𝒫 B) \land v \in V) \to v \in V$
30	4	fvexi	$⊢ \underset{˙}{1} \in V$
31	3	fvexi	$⊢ \underset{˙}{0} \in V$
32	30 31	ifex	$⊢ if (v = Z, \underset{˙}{1}, \underset{˙}{0}) \in V$
33		eqeq1	$⊢ x = v \to (x = Z \leftrightarrow v = Z)$
34	33	ifbid	$⊢ x = v \to if (x = Z, \underset{˙}{1}, \underset{˙}{0}) = if (v = Z, \underset{˙}{1}, \underset{˙}{0})$
35	34 6	fvmptg	$⊢ (v \in V \land if (v = Z, \underset{˙}{1}, \underset{˙}{0}) \in V) \to F (v) = if (v = Z, \underset{˙}{1}, \underset{˙}{0})$
36	29 32 35	sylancl	$⊢ ((M \in LMod \land V \in 𝒫 B) \land v \in V) \to F (v) = if (v = Z, \underset{˙}{1}, \underset{˙}{0})$
37	36	oveq1d	$⊢ ((M \in LMod \land V \in 𝒫 B) \land v \in V) \to F (v) \cdot_{M} v = if (v = Z, \underset{˙}{1}, \underset{˙}{0}) \cdot_{M} v$
38		ovif	$⊢ if (v = Z, \underset{˙}{1}, \underset{˙}{0}) \cdot_{M} v = if (v = Z, \underset{˙}{1} \cdot_{M} v, \underset{˙}{0} \cdot_{M} v)$
39	38	a1i	$⊢ ((M \in LMod \land V \in 𝒫 B) \land v \in V) \to if (v = Z, \underset{˙}{1}, \underset{˙}{0}) \cdot_{M} v = if (v = Z, \underset{˙}{1} \cdot_{M} v, \underset{˙}{0} \cdot_{M} v)$
40		oveq2	$⊢ v = Z \to \underset{˙}{1} \cdot_{M} v = \underset{˙}{1} \cdot_{M} Z$
41	40	adantl	$⊢ (((M \in LMod \land V \in 𝒫 B) \land v \in V) \land v = Z) \to \underset{˙}{1} \cdot_{M} v = \underset{˙}{1} \cdot_{M} Z$
42		eqid	$⊢ {Base}_{S} = {Base}_{S}$
43	2 42 4	lmod1cl	$⊢ M \in LMod \to \underset{˙}{1} \in {Base}_{S}$
44	43	ancli	$⊢ M \in LMod \to (M \in LMod \land \underset{˙}{1} \in {Base}_{S})$
45	44	adantr	$⊢ (M \in LMod \land V \in 𝒫 B) \to (M \in LMod \land \underset{˙}{1} \in {Base}_{S})$
46	45	ad2antrr	$⊢ (((M \in LMod \land V \in 𝒫 B) \land v \in V) \land v = Z) \to (M \in LMod \land \underset{˙}{1} \in {Base}_{S})$
47		eqid	$⊢ \cdot_{M} = \cdot_{M}$
48	2 47 42 5	lmodvs0	$⊢ (M \in LMod \land \underset{˙}{1} \in {Base}_{S}) \to \underset{˙}{1} \cdot_{M} Z = Z$
49	46 48	syl	$⊢ (((M \in LMod \land V \in 𝒫 B) \land v \in V) \land v = Z) \to \underset{˙}{1} \cdot_{M} Z = Z$
50	41 49	eqtrd	$⊢ (((M \in LMod \land V \in 𝒫 B) \land v \in V) \land v = Z) \to \underset{˙}{1} \cdot_{M} v = Z$
51	7	adantr	$⊢ ((M \in LMod \land V \in 𝒫 B) \land v \in V) \to M \in LMod$
52		elelpwi	$⊢ (v \in V \land V \in 𝒫 B) \to v \in B$
53	52	expcom	$⊢ V \in 𝒫 B \to (v \in V \to v \in B)$
54	53	adantl	$⊢ (M \in LMod \land V \in 𝒫 B) \to (v \in V \to v \in B)$
55	54	imp	$⊢ ((M \in LMod \land V \in 𝒫 B) \land v \in V) \to v \in B$
56	1 2 47 3 5	lmod0vs	$⊢ (M \in LMod \land v \in B) \to \underset{˙}{0} \cdot_{M} v = Z$
57	51 55 56	syl2anc	$⊢ ((M \in LMod \land V \in 𝒫 B) \land v \in V) \to \underset{˙}{0} \cdot_{M} v = Z$
58	57	adantr	$⊢ (((M \in LMod \land V \in 𝒫 B) \land v \in V) \land \neg v = Z) \to \underset{˙}{0} \cdot_{M} v = Z$
59	50 58	ifeqda	$⊢ ((M \in LMod \land V \in 𝒫 B) \land v \in V) \to if (v = Z, \underset{˙}{1} \cdot_{M} v, \underset{˙}{0} \cdot_{M} v) = Z$
60	37 39 59	3eqtrd	$⊢ ((M \in LMod \land V \in 𝒫 B) \land v \in V) \to F (v) \cdot_{M} v = Z$
61	60	mpteq2dva	$⊢ (M \in LMod \land V \in 𝒫 B) \to (v \in V ⟼ F (v) \cdot_{M} v) = (v \in V ⟼ Z)$
62	61	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$
63		lmodgrp	$⊢ M \in LMod \to M \in Grp$
64	63	grpmndd	$⊢ M \in LMod \to M \in Mnd$
65	5	gsumz	$⊢ (M \in Mnd \land V \in 𝒫 B) \to \underset{v \in V}{\sum_{M}} Z = Z$
66	64 65	sylan	$⊢ (M \in LMod \land V \in 𝒫 B) \to \underset{v \in V}{\sum_{M}} Z = Z$
67	28 62 66	3eqtrd	$⊢ (M \in LMod \land V \in 𝒫 B) \to F linC (M) V = Z$

Metamath Proof Explorer

Theorem linc0scn0

Proof