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	biimpi	$⊢ V \in 𝒫 B \to V \in 𝒫 {Base}_{M}$
27	26	adantl	$⊢ (M \in LMod \land V \in 𝒫 B) \to V \in 𝒫 {Base}_{M}$
28		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)$
29	7 23 27 28	syl3anc	$⊢ (M \in LMod \land V \in 𝒫 B) \to F linC (M) V = \underset{v \in V}{\sum_{M}} (F (v) \cdot_{M} v)$
30		simpr	$⊢ ((M \in LMod \land V \in 𝒫 B) \land v \in V) \to v \in V$
31	4	fvexi	$⊢ \underset{˙}{1} \in V$
32	3	fvexi	$⊢ \underset{˙}{0} \in V$
33	31 32	ifex	$⊢ if (v = Z, \underset{˙}{1}, \underset{˙}{0}) \in V$
34		eqeq1	$⊢ x = v \to (x = Z \leftrightarrow v = Z)$
35	34	ifbid	$⊢ x = v \to if (x = Z, \underset{˙}{1}, \underset{˙}{0}) = if (v = Z, \underset{˙}{1}, \underset{˙}{0})$
36	35 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})$
37	30 33 36	sylancl	$⊢ ((M \in LMod \land V \in 𝒫 B) \land v \in V) \to F (v) = if (v = Z, \underset{˙}{1}, \underset{˙}{0})$
38	37	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$
39		ovif	$⊢ if (v = Z, \underset{˙}{1}, \underset{˙}{0}) \cdot_{M} v = if (v = Z, \underset{˙}{1} \cdot_{M} v, \underset{˙}{0} \cdot_{M} v)$
40	39	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)$
41		oveq2	$⊢ v = Z \to \underset{˙}{1} \cdot_{M} v = \underset{˙}{1} \cdot_{M} Z$
42	41	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$
43		eqid	$⊢ {Base}_{S} = {Base}_{S}$
44	2 43 4	lmod1cl	$⊢ M \in LMod \to \underset{˙}{1} \in {Base}_{S}$
45	44	ancli	$⊢ M \in LMod \to (M \in LMod \land \underset{˙}{1} \in {Base}_{S})$
46	45	adantr	$⊢ (M \in LMod \land V \in 𝒫 B) \to (M \in LMod \land \underset{˙}{1} \in {Base}_{S})$
47	46	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})$
48		eqid	$⊢ \cdot_{M} = \cdot_{M}$
49	2 48 43 5	lmodvs0	$⊢ (M \in LMod \land \underset{˙}{1} \in {Base}_{S}) \to \underset{˙}{1} \cdot_{M} Z = Z$
50	47 49	syl	$⊢ (((M \in LMod \land V \in 𝒫 B) \land v \in V) \land v = Z) \to \underset{˙}{1} \cdot_{M} Z = Z$
51	42 50	eqtrd	$⊢ (((M \in LMod \land V \in 𝒫 B) \land v \in V) \land v = Z) \to \underset{˙}{1} \cdot_{M} v = Z$
52	7	adantr	$⊢ ((M \in LMod \land V \in 𝒫 B) \land v \in V) \to M \in LMod$
53		elelpwi	$⊢ (v \in V \land V \in 𝒫 B) \to v \in B$
54	53	expcom	$⊢ V \in 𝒫 B \to (v \in V \to v \in B)$
55	54	adantl	$⊢ (M \in LMod \land V \in 𝒫 B) \to (v \in V \to v \in B)$
56	55	imp	$⊢ ((M \in LMod \land V \in 𝒫 B) \land v \in V) \to v \in B$
57	1 2 48 3 5	lmod0vs	$⊢ (M \in LMod \land v \in B) \to \underset{˙}{0} \cdot_{M} v = Z$
58	52 56 57	syl2anc	$⊢ ((M \in LMod \land V \in 𝒫 B) \land v \in V) \to \underset{˙}{0} \cdot_{M} v = Z$
59	58	adantr	$⊢ (((M \in LMod \land V \in 𝒫 B) \land v \in V) \land \neg v = Z) \to \underset{˙}{0} \cdot_{M} v = Z$
60	51 59	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$
61	38 40 60	3eqtrd	$⊢ ((M \in LMod \land V \in 𝒫 B) \land v \in V) \to F (v) \cdot_{M} v = Z$
62	61	mpteq2dva	$⊢ (M \in LMod \land V \in 𝒫 B) \to (v \in V ⟼ F (v) \cdot_{M} v) = (v \in V ⟼ Z)$
63	62	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$
64		lmodgrp	$⊢ M \in LMod \to M \in Grp$
65	64	grpmndd	$⊢ M \in LMod \to M \in Mnd$
66	5	gsumz	$⊢ (M \in Mnd \land V \in 𝒫 B) \to \underset{v \in V}{\sum_{M}} Z = Z$
67	65 66	sylan	$⊢ (M \in LMod \land V \in 𝒫 B) \to \underset{v \in V}{\sum_{M}} Z = Z$
68	29 63 67	3eqtrd	$⊢ (M \in LMod \land V \in 𝒫 B) \to F linC (M) V = Z$

Metamath Proof Explorer

Theorem linc0scn0

Proof