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	31	grpmndd	$⊢ M \in LMod \to M \in Mnd$
33	32	3ad2ant1	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to M \in Mnd$
34		simp3	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to X \in V$
35	6	adantr	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land y \in V) \to M \in LMod$
36		eqeq1	$⊢ x = y \to (x = X \leftrightarrow y = X)$
37	36	ifbid	$⊢ x = y \to if (x = X, \underset{˙}{1}, \underset{˙}{0}) = if (y = X, \underset{˙}{1}, \underset{˙}{0})$
38		simpr	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land y \in V) \to y \in V$
39		eqid	$⊢ {Base}_{S} = {Base}_{S}$
40	2 39 4	lmod1cl	$⊢ M \in LMod \to \underset{˙}{1} \in {Base}_{S}$
41	40	3ad2ant1	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to \underset{˙}{1} \in {Base}_{S}$
42	41	adantr	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land y \in V) \to \underset{˙}{1} \in {Base}_{S}$
43	2 39 3	lmod0cl	$⊢ M \in LMod \to \underset{˙}{0} \in {Base}_{S}$
44	43	3ad2ant1	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to \underset{˙}{0} \in {Base}_{S}$
45	44	adantr	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land y \in V) \to \underset{˙}{0} \in {Base}_{S}$
46	42 45	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}$
47	5 37 38 46	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})$
48	47 46	eqeltrd	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land y \in V) \to F (y) \in {Base}_{S}$
49		elelpwi	$⊢ (y \in V \land V \in 𝒫 B) \to y \in B$
50	49	expcom	$⊢ V \in 𝒫 B \to (y \in V \to y \in B)$
51	50	3ad2ant2	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to (y \in V \to y \in B)$
52	51	imp	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land y \in V) \to y \in B$
53		eqid	$⊢ \cdot_{M} = \cdot_{M}$
54	1 2 53 39	lmodvscl	$⊢ (M \in LMod \land F (y) \in {Base}_{S} \land y \in B) \to F (y) \cdot_{M} y \in B$
55	35 48 52 54	syl3anc	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land y \in V) \to F (y) \cdot_{M} y \in B$
56		eqid	$⊢ (y \in V ⟼ F (y) \cdot_{M} y) = (y \in V ⟼ F (y) \cdot_{M} y)$
57	55 56	fmptd	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to (y \in V ⟼ F (y) \cdot_{M} y) : V ⟶ B$
58		fveq2	$⊢ y = v \to F (y) = F (v)$
59		id	$⊢ y = v \to y = v$
60	58 59	oveq12d	$⊢ y = v \to F (y) \cdot_{M} y = F (v) \cdot_{M} v$
61	60	cbvmptv	$⊢ (y \in V ⟼ F (y) \cdot_{M} y) = (v \in V ⟼ F (v) \cdot_{M} v)$
62		fvexd	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to 0_{M} \in V$
63		ovexd	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land v \in V) \to F (v) \cdot_{M} v \in V$
64	61 20 62 63	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}\}$
65		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))$
66		simprr	$⊢ (\neg v = X \land ((M \in LMod \land V \in 𝒫 B \land X \in V) \land v \in V)) \to v \in V$
67	4	fvexi	$⊢ \underset{˙}{1} \in V$
68	3	fvexi	$⊢ \underset{˙}{0} \in V$
69	67 68	ifex	$⊢ if (v = X, \underset{˙}{1}, \underset{˙}{0}) \in V$
70		eqeq1	$⊢ x = v \to (x = X \leftrightarrow v = X)$
71	70	ifbid	$⊢ x = v \to if (x = X, \underset{˙}{1}, \underset{˙}{0}) = if (v = X, \underset{˙}{1}, \underset{˙}{0})$
72	71 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})$
73	66 69 72	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})$
74		iffalse	$⊢ \neg v = X \to if (v = X, \underset{˙}{1}, \underset{˙}{0}) = \underset{˙}{0}$
75	74	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}$
76	73 75	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}$
77	76	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$
78	6	adantr	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land v \in V) \to M \in LMod$
79	78	adantl	$⊢ (\neg v = X \land ((M \in LMod \land V \in 𝒫 B \land X \in V) \land v \in V)) \to M \in LMod$
80		elelpwi	$⊢ (v \in V \land V \in 𝒫 B) \to v \in B$
81	80	expcom	$⊢ V \in 𝒫 B \to (v \in V \to v \in B)$
82	81	3ad2ant2	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to (v \in V \to v \in B)$
83	82	imp	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land v \in V) \to v \in B$
84	83	adantl	$⊢ (\neg v = X \land ((M \in LMod \land V \in 𝒫 B \land X \in V) \land v \in V)) \to v \in B$
85	1 2 53 3 30	lmod0vs	$⊢ (M \in LMod \land v \in B) \to \underset{˙}{0} \cdot_{M} v = 0_{M}$
86	79 84 85	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}$
87	77 86	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}$
88	87	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})$
89		eqneqall	$⊢ 0_{M} = 0_{M} \to (0_{M} \neq 0_{M} \to v = X)$
90	30 89	ax-mp	$⊢ 0_{M} \neq 0_{M} \to v = X$
91	88 90	biimtrdi	$⊢ (\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)$
92	91	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))$
93	65 92	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)$
94	93	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)$
95		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)$
96	94 95	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\}$
97	64 96	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\}$
98	1 30 33 20 34 57 97	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)$
99		ovex	$⊢ F (X) \cdot_{M} X \in V$
100		fveq2	$⊢ y = X \to F (y) = F (X)$
101		id	$⊢ y = X \to y = X$
102	100 101	oveq12d	$⊢ y = X \to F (y) \cdot_{M} y = F (X) \cdot_{M} X$
103	102 56	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$
104	34 99 103	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$
105		iftrue	$⊢ x = X \to if (x = X, \underset{˙}{1}, \underset{˙}{0}) = \underset{˙}{1}$
106	105 5	fvmptg	$⊢ (X \in V \land \underset{˙}{1} \in V) \to F (X) = \underset{˙}{1}$
107	34 67 106	sylancl	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to F (X) = \underset{˙}{1}$
108	107	oveq1d	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to F (X) \cdot_{M} X = \underset{˙}{1} \cdot_{M} X$
109		elelpwi	$⊢ (X \in V \land V \in 𝒫 B) \to X \in B$
110	109	ancoms	$⊢ (V \in 𝒫 B \land X \in V) \to X \in B$
111	110	3adant1	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to X \in B$
112	1 2 53 4	lmodvs1	$⊢ (M \in LMod \land X \in B) \to \underset{˙}{1} \cdot_{M} X = X$
113	6 111 112	syl2anc	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to \underset{˙}{1} \cdot_{M} X = X$
114	104 108 113	3eqtrd	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to (y \in V ⟼ F (y) \cdot_{M} y) (X) = X$
115	29 98 114	3eqtrd	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to F linC (M) V = X$

Metamath Proof Explorer

Theorem linc1

Proof