linc1

Description: A vector is a linear combination of a set containing this vector. (Contributed by AV, 18-Apr-2019) (Proof shortened by AV, 28-Jul-2019)

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

Proof

Step	Hyp	Ref	Expression
1		linc1.b	$⊢ B = {Base}_{M}$
2		linc1.s	$⊢ S = Scalar (M)$
3		linc1.0	$⊢ \underset{˙}{0} = 0_{S}$
4		linc1.1	$⊢ \underset{˙}{1} = 1_{S}$
5		linc1.f	$⊢ F = (x \in V ⟼ if (x = X, \underset{˙}{1}, \underset{˙}{0}))$
6		simp1	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to M \in LMod$
7	2	lmodring	$⊢ M \in LMod \to S \in Ring$
8	2	eqcomi	$⊢ Scalar (M) = S$
9	8	fveq2i	$⊢ {Base}_{Scalar (M)} = {Base}_{S}$
10	9 4	ringidcl	$⊢ S \in Ring \to \underset{˙}{1} \in {Base}_{Scalar (M)}$
11	9 3	ring0cl	$⊢ S \in Ring \to \underset{˙}{0} \in {Base}_{Scalar (M)}$
12	10 11	jca	$⊢ S \in Ring \to (\underset{˙}{1} \in {Base}_{Scalar (M)} \land \underset{˙}{0} \in {Base}_{Scalar (M)})$
13	7 12	syl	$⊢ M \in LMod \to (\underset{˙}{1} \in {Base}_{Scalar (M)} \land \underset{˙}{0} \in {Base}_{Scalar (M)})$
14	13	3ad2ant1	$⊢ (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)})$
15	14	adantr	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \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 = X, \underset{˙}{1}, \underset{˙}{0}) \in {Base}_{Scalar (M)}$
17	15 16	syl	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land x \in V) \to if (x = X, \underset{˙}{1}, \underset{˙}{0}) \in {Base}_{Scalar (M)}$
18	17 5	fmptd	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to F : V ⟶ {Base}_{Scalar (M)}$
19		fvex	$⊢ {Base}_{Scalar (M)} \in V$
20		simp2	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to V \in 𝒫 B$
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	19 20 21	sylancr	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to (F \in ({Base}_{Scalar (M)}^{V}) \leftrightarrow F : V ⟶ {Base}_{Scalar (M)})$
23	18 22	mpbird	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \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	3ad2ant2	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \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{y \in V}{\sum_{M}} (F (y) \cdot_{M} y)$
29	6 23 27 28	syl3anc	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to F linC (M) V = \underset{y \in V}{\sum_{M}} (F (y) \cdot_{M} y)$
30		eqid	$⊢ 0_{M} = 0_{M}$
31		lmodgrp	$⊢ M \in LMod \to M \in Grp$
32		grpmnd	$⊢ M \in Grp \to M \in Mnd$
33	31 32	syl	$⊢ M \in LMod \to M \in Mnd$
34	33	3ad2ant1	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to M \in Mnd$
35		simp3	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to X \in V$
36	6	adantr	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land y \in V) \to M \in LMod$
37		eqeq1	$⊢ x = y \to (x = X \leftrightarrow y = X)$
38	37	ifbid	$⊢ x = y \to if (x = X, \underset{˙}{1}, \underset{˙}{0}) = if (y = X, \underset{˙}{1}, \underset{˙}{0})$
39		simpr	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land y \in V) \to y \in V$
40		eqid	$⊢ {Base}_{S} = {Base}_{S}$
41	2 40 4	lmod1cl	$⊢ M \in LMod \to \underset{˙}{1} \in {Base}_{S}$
42	41	3ad2ant1	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to \underset{˙}{1} \in {Base}_{S}$
43	42	adantr	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land y \in V) \to \underset{˙}{1} \in {Base}_{S}$
44	2 40 3	lmod0cl	$⊢ M \in LMod \to \underset{˙}{0} \in {Base}_{S}$
45	44	3ad2ant1	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to \underset{˙}{0} \in {Base}_{S}$
46	45	adantr	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land y \in V) \to \underset{˙}{0} \in {Base}_{S}$
47	43 46	ifcld	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land y \in V) \to if (y = X, \underset{˙}{1}, \underset{˙}{0}) \in {Base}_{S}$
48	5 38 39 47	fvmptd3	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land y \in V) \to F (y) = if (y = X, \underset{˙}{1}, \underset{˙}{0})$
49	48 47	eqeltrd	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land y \in V) \to F (y) \in {Base}_{S}$
50		elelpwi	$⊢ (y \in V \land V \in 𝒫 B) \to y \in B$
51	50	expcom	$⊢ V \in 𝒫 B \to (y \in V \to y \in B)$
52	51	3ad2ant2	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to (y \in V \to y \in B)$
53	52	imp	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land y \in V) \to y \in B$
54		eqid	$⊢ \cdot_{M} = \cdot_{M}$
55	1 2 54 40	lmodvscl	$⊢ (M \in LMod \land F (y) \in {Base}_{S} \land y \in B) \to F (y) \cdot_{M} y \in B$
56	36 49 53 55	syl3anc	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land y \in V) \to F (y) \cdot_{M} y \in B$
57		eqid	$⊢ (y \in V ⟼ F (y) \cdot_{M} y) = (y \in V ⟼ F (y) \cdot_{M} y)$
58	56 57	fmptd	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to (y \in V ⟼ F (y) \cdot_{M} y) : V ⟶ B$
59		fveq2	$⊢ y = v \to F (y) = F (v)$
60		id	$⊢ y = v \to y = v$
61	59 60	oveq12d	$⊢ y = v \to F (y) \cdot_{M} y = F (v) \cdot_{M} v$
62	61	cbvmptv	$⊢ (y \in V ⟼ F (y) \cdot_{M} y) = (v \in V ⟼ F (v) \cdot_{M} v)$
63		fvexd	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to 0_{M} \in V$
64		ovexd	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land v \in V) \to F (v) \cdot_{M} v \in V$
65	62 20 63 64	mptsuppd	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to (y \in V ⟼ F (y) \cdot_{M} y) supp 0_{M} = \{v \in V \| F (v) \cdot_{M} v \neq 0_{M}\}$
66		2a1	$⊢ v = X \to (((M \in LMod \land V \in 𝒫 B \land X \in V) \land v \in V) \to (F (v) \cdot_{M} v \neq 0_{M} \to v = X))$
67		simprr	$⊢ (\neg v = X \land ((M \in LMod \land V \in 𝒫 B \land X \in V) \land v \in V)) \to v \in V$
68	4	fvexi	$⊢ \underset{˙}{1} \in V$
69	3	fvexi	$⊢ \underset{˙}{0} \in V$
70	68 69	ifex	$⊢ if (v = X, \underset{˙}{1}, \underset{˙}{0}) \in V$
71		eqeq1	$⊢ x = v \to (x = X \leftrightarrow v = X)$
72	71	ifbid	$⊢ x = v \to if (x = X, \underset{˙}{1}, \underset{˙}{0}) = if (v = X, \underset{˙}{1}, \underset{˙}{0})$
73	72 5	fvmptg	$⊢ (v \in V \land if (v = X, \underset{˙}{1}, \underset{˙}{0}) \in V) \to F (v) = if (v = X, \underset{˙}{1}, \underset{˙}{0})$
74	67 70 73	sylancl	$⊢ (\neg v = X \land ((M \in LMod \land V \in 𝒫 B \land X \in V) \land v \in V)) \to F (v) = if (v = X, \underset{˙}{1}, \underset{˙}{0})$
75		iffalse	$⊢ \neg v = X \to if (v = X, \underset{˙}{1}, \underset{˙}{0}) = \underset{˙}{0}$
76	75	adantr	$⊢ (\neg v = X \land ((M \in LMod \land V \in 𝒫 B \land X \in V) \land v \in V)) \to if (v = X, \underset{˙}{1}, \underset{˙}{0}) = \underset{˙}{0}$
77	74 76	eqtrd	$⊢ (\neg v = X \land ((M \in LMod \land V \in 𝒫 B \land X \in V) \land v \in V)) \to F (v) = \underset{˙}{0}$
78	77	oveq1d	$⊢ (\neg v = X \land ((M \in LMod \land V \in 𝒫 B \land X \in V) \land v \in V)) \to F (v) \cdot_{M} v = \underset{˙}{0} \cdot_{M} v$
79	6	adantr	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land v \in V) \to M \in LMod$
80	79	adantl	$⊢ (\neg v = X \land ((M \in LMod \land V \in 𝒫 B \land X \in V) \land v \in V)) \to M \in LMod$
81		elelpwi	$⊢ (v \in V \land V \in 𝒫 B) \to v \in B$
82	81	expcom	$⊢ V \in 𝒫 B \to (v \in V \to v \in B)$
83	82	3ad2ant2	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to (v \in V \to v \in B)$
84	83	imp	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land v \in V) \to v \in B$
85	84	adantl	$⊢ (\neg v = X \land ((M \in LMod \land V \in 𝒫 B \land X \in V) \land v \in V)) \to v \in B$
86	1 2 54 3 30	lmod0vs	$⊢ (M \in LMod \land v \in B) \to \underset{˙}{0} \cdot_{M} v = 0_{M}$
87	80 85 86	syl2anc	$⊢ (\neg v = X \land ((M \in LMod \land V \in 𝒫 B \land X \in V) \land v \in V)) \to \underset{˙}{0} \cdot_{M} v = 0_{M}$
88	78 87	eqtrd	$⊢ (\neg v = X \land ((M \in LMod \land V \in 𝒫 B \land X \in V) \land v \in V)) \to F (v) \cdot_{M} v = 0_{M}$
89	88	neeq1d	$⊢ (\neg v = X \land ((M \in LMod \land V \in 𝒫 B \land X \in V) \land v \in V)) \to (F (v) \cdot_{M} v \neq 0_{M} \leftrightarrow 0_{M} \neq 0_{M})$
90		eqneqall	$⊢ 0_{M} = 0_{M} \to (0_{M} \neq 0_{M} \to v = X)$
91	30 90	ax-mp	$⊢ 0_{M} \neq 0_{M} \to v = X$
92	89 91	syl6bi	$⊢ (\neg v = X \land ((M \in LMod \land V \in 𝒫 B \land X \in V) \land v \in V)) \to (F (v) \cdot_{M} v \neq 0_{M} \to v = X)$
93	92	ex	$⊢ \neg v = X \to (((M \in LMod \land V \in 𝒫 B \land X \in V) \land v \in V) \to (F (v) \cdot_{M} v \neq 0_{M} \to v = X))$
94	66 93	pm2.61i	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land v \in V) \to (F (v) \cdot_{M} v \neq 0_{M} \to v = X)$
95	94	ralrimiva	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to \forall v \in V (F (v) \cdot_{M} v \neq 0_{M} \to v = X)$
96		rabsssn	$⊢ \{v \in V \| F (v) \cdot_{M} v \neq 0_{M}\} \subseteq \{X\} \leftrightarrow \forall v \in V (F (v) \cdot_{M} v \neq 0_{M} \to v = X)$
97	95 96	sylibr	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to \{v \in V \| F (v) \cdot_{M} v \neq 0_{M}\} \subseteq \{X\}$
98	65 97	eqsstrd	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to (y \in V ⟼ F (y) \cdot_{M} y) supp 0_{M} \subseteq \{X\}$
99	1 30 34 20 35 58 98	gsumpt	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to \underset{y \in V}{\sum_{M}} (F (y) \cdot_{M} y) = (y \in V ⟼ F (y) \cdot_{M} y) (X)$
100		ovex	$⊢ F (X) \cdot_{M} X \in V$
101		fveq2	$⊢ y = X \to F (y) = F (X)$
102		id	$⊢ y = X \to y = X$
103	101 102	oveq12d	$⊢ y = X \to F (y) \cdot_{M} y = F (X) \cdot_{M} X$
104	103 57	fvmptg	$⊢ (X \in V \land F (X) \cdot_{M} X \in V) \to (y \in V ⟼ F (y) \cdot_{M} y) (X) = F (X) \cdot_{M} X$
105	35 100 104	sylancl	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to (y \in V ⟼ F (y) \cdot_{M} y) (X) = F (X) \cdot_{M} X$
106		iftrue	$⊢ x = X \to if (x = X, \underset{˙}{1}, \underset{˙}{0}) = \underset{˙}{1}$
107	106 5	fvmptg	$⊢ (X \in V \land \underset{˙}{1} \in V) \to F (X) = \underset{˙}{1}$
108	35 68 107	sylancl	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to F (X) = \underset{˙}{1}$
109	108	oveq1d	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to F (X) \cdot_{M} X = \underset{˙}{1} \cdot_{M} X$
110		elelpwi	$⊢ (X \in V \land V \in 𝒫 B) \to X \in B$
111	110	ancoms	$⊢ (V \in 𝒫 B \land X \in V) \to X \in B$
112	111	3adant1	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to X \in B$
113	1 2 54 4	lmodvs1	$⊢ (M \in LMod \land X \in B) \to \underset{˙}{1} \cdot_{M} X = X$
114	6 112 113	syl2anc	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to \underset{˙}{1} \cdot_{M} X = X$
115	105 109 114	3eqtrd	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to (y \in V ⟼ F (y) \cdot_{M} y) (X) = X$
116	29 99 115	3eqtrd	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to F linC (M) V = X$

Metamath Proof Explorer

Theorem linc1

Proof