lincdifsn

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

	Ref	Expression
Hypotheses	lincdifsn.b	$⊢ B = {Base}_{M}$
	lincdifsn.r	$⊢ R = Scalar (M)$
	lincdifsn.s	$⊢ S = {Base}_{R}$
	lincdifsn.t	$⊢ \underset{˙}{\cdot} = \cdot_{M}$
	lincdifsn.p	$⊢ \underset{˙}{+} = +_{M}$
	lincdifsn.0	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	lincdifsn	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \to F linC (M) V = (G linC (M) (V ∖ \{X\})) \underset{˙}{+} (F (X) \underset{˙}{\cdot} X)$

Proof

Step	Hyp	Ref	Expression
1		lincdifsn.b	$⊢ B = {Base}_{M}$
2		lincdifsn.r	$⊢ R = Scalar (M)$
3		lincdifsn.s	$⊢ S = {Base}_{R}$
4		lincdifsn.t	$⊢ \underset{˙}{\cdot} = \cdot_{M}$
5		lincdifsn.p	$⊢ \underset{˙}{+} = +_{M}$
6		lincdifsn.0	$⊢ \underset{˙}{0} = 0_{R}$
7		simp11	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \to M \in LMod$
8	2	fveq2i	$⊢ {Base}_{R} = {Base}_{Scalar (M)}$
9	3 8	eqtri	$⊢ S = {Base}_{Scalar (M)}$
10	9	oveq1i	$⊢ S^{V} = {Base}_{Scalar (M)}^{V}$
11	10	eleq2i	$⊢ F \in (S^{V}) \leftrightarrow F \in ({Base}_{Scalar (M)}^{V})$
12	11	biimpi	$⊢ F \in (S^{V}) \to F \in ({Base}_{Scalar (M)}^{V})$
13	12	adantr	$⊢ (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \to F \in ({Base}_{Scalar (M)}^{V})$
14	13	3ad2ant2	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \to F \in ({Base}_{Scalar (M)}^{V})$
15	1	pweqi	$⊢ 𝒫 B = 𝒫 {Base}_{M}$
16	15	eleq2i	$⊢ V \in 𝒫 B \leftrightarrow V \in 𝒫 {Base}_{M}$
17	16	biimpi	$⊢ V \in 𝒫 B \to V \in 𝒫 {Base}_{M}$
18	17	3ad2ant2	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to V \in 𝒫 {Base}_{M}$
19	18	3ad2ant1	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \to V \in 𝒫 {Base}_{M}$
20		lincval	$⊢ (M \in LMod \land F \in ({Base}_{Scalar (M)}^{V}) \land V \in 𝒫 {Base}_{M}) \to F linC (M) V = \underset{x \in V}{\sum_{M}} (F (x) \cdot_{M} x)$
21	7 14 19 20	syl3anc	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \to F linC (M) V = \underset{x \in V}{\sum_{M}} (F (x) \cdot_{M} x)$
22		lmodcmn	$⊢ M \in LMod \to M \in CMnd$
23	22	3ad2ant1	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to M \in CMnd$
24	23	3ad2ant1	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \to M \in CMnd$
25		simp12	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \to V \in 𝒫 B$
26	17	anim2i	$⊢ (M \in LMod \land V \in 𝒫 B) \to (M \in LMod \land V \in 𝒫 {Base}_{M})$
27	26	3adant3	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to (M \in LMod \land V \in 𝒫 {Base}_{M})$
28	27	3ad2ant1	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \to (M \in LMod \land V \in 𝒫 {Base}_{M})$
29		simp2l	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \to F \in (S^{V})$
30	6	breq2i	$⊢ {finSupp}_{\underset{˙}{0}} (F) \leftrightarrow {finSupp}_{0_{R}} (F)$
31	30	biimpi	$⊢ {finSupp}_{\underset{˙}{0}} (F) \to {finSupp}_{0_{R}} (F)$
32	31	adantl	$⊢ (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \to {finSupp}_{0_{R}} (F)$
33	32	3ad2ant2	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \to {finSupp}_{0_{R}} (F)$
34	2 3	scmfsupp	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land F \in (S^{V}) \land {finSupp}_{0_{R}} (F)) \to {finSupp}_{0_{M}} ((x \in V ⟼ F (x) \cdot_{M} x))$
35	28 29 33 34	syl3anc	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \to {finSupp}_{0_{M}} ((x \in V ⟼ F (x) \cdot_{M} x))$
36		simpl1	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F))) \to M \in LMod$
37	36	adantr	$⊢ (((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F))) \land x \in V) \to M \in LMod$
38		elmapi	$⊢ F \in (S^{V}) \to F : V ⟶ S$
39		ffvelrn	$⊢ (F : V ⟶ S \land x \in V) \to F (x) \in S$
40	39	ex	$⊢ F : V ⟶ S \to (x \in V \to F (x) \in S)$
41	40	a1d	$⊢ F : V ⟶ S \to ((M \in LMod \land V \in 𝒫 B \land X \in V) \to (x \in V \to F (x) \in S))$
42	38 41	syl	$⊢ F \in (S^{V}) \to ((M \in LMod \land V \in 𝒫 B \land X \in V) \to (x \in V \to F (x) \in S))$
43	42	adantr	$⊢ (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \to ((M \in LMod \land V \in 𝒫 B \land X \in V) \to (x \in V \to F (x) \in S))$
44	43	impcom	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F))) \to (x \in V \to F (x) \in S)$
45	44	imp	$⊢ (((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F))) \land x \in V) \to F (x) \in S$
46		elelpwi	$⊢ (x \in V \land V \in 𝒫 B) \to x \in B$
47	46	expcom	$⊢ V \in 𝒫 B \to (x \in V \to x \in B)$
48	47	3ad2ant2	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to (x \in V \to x \in B)$
49	48	adantr	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F))) \to (x \in V \to x \in B)$
50	49	imp	$⊢ (((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F))) \land x \in V) \to x \in B$
51		eqid	$⊢ \cdot_{M} = \cdot_{M}$
52	1 2 51 3	lmodvscl	$⊢ (M \in LMod \land F (x) \in S \land x \in B) \to F (x) \cdot_{M} x \in B$
53	37 45 50 52	syl3anc	$⊢ (((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F))) \land x \in V) \to F (x) \cdot_{M} x \in B$
54	53	3adantl3	$⊢ (((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \land x \in V) \to F (x) \cdot_{M} x \in B$
55		simp13	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \to X \in V$
56		ffvelrn	$⊢ (F : V ⟶ S \land X \in V) \to F (X) \in S$
57	56	expcom	$⊢ X \in V \to (F : V ⟶ S \to F (X) \in S)$
58	57	3ad2ant3	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to (F : V ⟶ S \to F (X) \in S)$
59	38 58	syl5com	$⊢ F \in (S^{V}) \to ((M \in LMod \land V \in 𝒫 B \land X \in V) \to F (X) \in S)$
60	59	adantr	$⊢ (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \to ((M \in LMod \land V \in 𝒫 B \land X \in V) \to F (X) \in S)$
61	60	impcom	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F))) \to F (X) \in S$
62		elelpwi	$⊢ (X \in V \land V \in 𝒫 B) \to X \in B$
63	62	ancoms	$⊢ (V \in 𝒫 B \land X \in V) \to X \in B$
64	63	3adant1	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to X \in B$
65	64	adantr	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F))) \to X \in B$
66	1 2 4 3	lmodvscl	$⊢ (M \in LMod \land F (X) \in S \land X \in B) \to F (X) \underset{˙}{\cdot} X \in B$
67	36 61 65 66	syl3anc	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F))) \to F (X) \underset{˙}{\cdot} X \in B$
68	67	3adant3	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \to F (X) \underset{˙}{\cdot} X \in B$
69	4	eqcomi	$⊢ \cdot_{M} = \underset{˙}{\cdot}$
70	69	a1i	$⊢ x = X \to \cdot_{M} = \underset{˙}{\cdot}$
71		fveq2	$⊢ x = X \to F (x) = F (X)$
72		id	$⊢ x = X \to x = X$
73	70 71 72	oveq123d	$⊢ x = X \to F (x) \cdot_{M} x = F (X) \underset{˙}{\cdot} X$
74	73	adantl	$⊢ (((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \land x = X) \to F (x) \cdot_{M} x = F (X) \underset{˙}{\cdot} X$
75	1 5 24 25 35 54 55 68 74	gsumdifsnd	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \to \underset{x \in V}{\sum_{M}} (F (x) \cdot_{M} x) = (\underset{x \in V ∖ \{X\}}{\sum_{M}}, (F (x) \cdot_{M} x)) \underset{˙}{+} (F (X) \underset{˙}{\cdot} X)$
76		fveq1	$⊢ G = {F ↾}_{(V ∖ \{X\})} \to G (x) = ({F ↾}_{(V ∖ \{X\})}) (x)$
77	76	3ad2ant3	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \to G (x) = ({F ↾}_{(V ∖ \{X\})}) (x)$
78		fvres	$⊢ x \in (V ∖ \{X\}) \to ({F ↾}_{(V ∖ \{X\})}) (x) = F (x)$
79	77 78	sylan9eq	$⊢ (((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \land x \in (V ∖ \{X\})) \to G (x) = F (x)$
80	79	oveq1d	$⊢ (((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \land x \in (V ∖ \{X\})) \to G (x) \cdot_{M} x = F (x) \cdot_{M} x$
81	80	mpteq2dva	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \to (x \in (V ∖ \{X\}) ⟼ G (x) \cdot_{M} x) = (x \in (V ∖ \{X\}) ⟼ F (x) \cdot_{M} x)$
82	81	eqcomd	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \to (x \in (V ∖ \{X\}) ⟼ F (x) \cdot_{M} x) = (x \in (V ∖ \{X\}) ⟼ G (x) \cdot_{M} x)$
83	82	oveq2d	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \to \underset{x \in V ∖ \{X\}}{\sum_{M}} (F (x) \cdot_{M} x) = \underset{x \in V ∖ \{X\}}{\sum_{M}} (G (x) \cdot_{M} x)$
84	83	oveq1d	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \to (\underset{x \in V ∖ \{X\}}{\sum_{M}}, (F (x) \cdot_{M} x)) \underset{˙}{+} (F (X) \underset{˙}{\cdot} X) = (\underset{x \in V ∖ \{X\}}{\sum_{M}}, (G (x) \cdot_{M} x)) \underset{˙}{+} (F (X) \underset{˙}{\cdot} X)$
85	75 84	eqtrd	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \to \underset{x \in V}{\sum_{M}} (F (x) \cdot_{M} x) = (\underset{x \in V ∖ \{X\}}{\sum_{M}}, (G (x) \cdot_{M} x)) \underset{˙}{+} (F (X) \underset{˙}{\cdot} X)$
86		eqid	$⊢ V = V$
87	86 9	feq23i	$⊢ F : V ⟶ S \leftrightarrow F : V ⟶ {Base}_{Scalar (M)}$
88	38 87	sylib	$⊢ F \in (S^{V}) \to F : V ⟶ {Base}_{Scalar (M)}$
89	88	adantr	$⊢ (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \to F : V ⟶ {Base}_{Scalar (M)}$
90	89	3ad2ant2	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \to F : V ⟶ {Base}_{Scalar (M)}$
91		difssd	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \to V ∖ \{X\} \subseteq V$
92	90 91	fssresd	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \to ({F ↾}_{(V ∖ \{X\})}) : V ∖ \{X\} ⟶ {Base}_{Scalar (M)}$
93		feq1	$⊢ G = {F ↾}_{(V ∖ \{X\})} \to (G : V ∖ \{X\} ⟶ {Base}_{Scalar (M)} \leftrightarrow ({F ↾}_{(V ∖ \{X\})}) : V ∖ \{X\} ⟶ {Base}_{Scalar (M)})$
94	93	3ad2ant3	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \to (G : V ∖ \{X\} ⟶ {Base}_{Scalar (M)} \leftrightarrow ({F ↾}_{(V ∖ \{X\})}) : V ∖ \{X\} ⟶ {Base}_{Scalar (M)})$
95	92 94	mpbird	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \to G : V ∖ \{X\} ⟶ {Base}_{Scalar (M)}$
96		fvex	$⊢ {Base}_{Scalar (M)} \in V$
97		difexg	$⊢ V \in 𝒫 B \to V ∖ \{X\} \in V$
98	97	3ad2ant2	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to V ∖ \{X\} \in V$
99	98	3ad2ant1	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \to V ∖ \{X\} \in V$
100		elmapg	$⊢ ({Base}_{Scalar (M)} \in V \land V ∖ \{X\} \in V) \to (G \in ({Base}_{Scalar (M)}^{(V ∖ \{X\})}) \leftrightarrow G : V ∖ \{X\} ⟶ {Base}_{Scalar (M)})$
101	96 99 100	sylancr	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \to (G \in ({Base}_{Scalar (M)}^{(V ∖ \{X\})}) \leftrightarrow G : V ∖ \{X\} ⟶ {Base}_{Scalar (M)})$
102	95 101	mpbird	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \to G \in ({Base}_{Scalar (M)}^{(V ∖ \{X\})})$
103		elpwi	$⊢ V \in 𝒫 B \to V \subseteq B$
104	1	sseq2i	$⊢ V \subseteq B \leftrightarrow V \subseteq {Base}_{M}$
105	104	biimpi	$⊢ V \subseteq B \to V \subseteq {Base}_{M}$
106	105	ssdifssd	$⊢ V \subseteq B \to V ∖ \{X\} \subseteq {Base}_{M}$
107	103 106	syl	$⊢ V \in 𝒫 B \to V ∖ \{X\} \subseteq {Base}_{M}$
108	107	adantl	$⊢ (M \in LMod \land V \in 𝒫 B) \to V ∖ \{X\} \subseteq {Base}_{M}$
109	97	adantl	$⊢ (M \in LMod \land V \in 𝒫 B) \to V ∖ \{X\} \in V$
110		elpwg	$⊢ V ∖ \{X\} \in V \to (V ∖ \{X\} \in 𝒫 {Base}_{M} \leftrightarrow V ∖ \{X\} \subseteq {Base}_{M})$
111	109 110	syl	$⊢ (M \in LMod \land V \in 𝒫 B) \to (V ∖ \{X\} \in 𝒫 {Base}_{M} \leftrightarrow V ∖ \{X\} \subseteq {Base}_{M})$
112	108 111	mpbird	$⊢ (M \in LMod \land V \in 𝒫 B) \to V ∖ \{X\} \in 𝒫 {Base}_{M}$
113	112	3adant3	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to V ∖ \{X\} \in 𝒫 {Base}_{M}$
114	113	3ad2ant1	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \to V ∖ \{X\} \in 𝒫 {Base}_{M}$
115		lincval	$⊢ (M \in LMod \land G \in ({Base}_{Scalar (M)}^{(V ∖ \{X\})}) \land V ∖ \{X\} \in 𝒫 {Base}_{M}) \to G linC (M) (V ∖ \{X\}) = \underset{x \in V ∖ \{X\}}{\sum_{M}} (G (x) \cdot_{M} x)$
116	7 102 114 115	syl3anc	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \to G linC (M) (V ∖ \{X\}) = \underset{x \in V ∖ \{X\}}{\sum_{M}} (G (x) \cdot_{M} x)$
117	116	eqcomd	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \to \underset{x \in V ∖ \{X\}}{\sum_{M}} (G (x) \cdot_{M} x) = G linC (M) (V ∖ \{X\})$
118	117	oveq1d	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \to (\underset{x \in V ∖ \{X\}}{\sum_{M}}, (G (x) \cdot_{M} x)) \underset{˙}{+} (F (X) \underset{˙}{\cdot} X) = (G linC (M) (V ∖ \{X\})) \underset{˙}{+} (F (X) \underset{˙}{\cdot} X)$
119	21 85 118	3eqtrd	$⊢ ((M \in LMod \land V \in 𝒫 B \land X \in V) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(V ∖ \{X\})}) \to F linC (M) V = (G linC (M) (V ∖ \{X\})) \underset{˙}{+} (F (X) \underset{˙}{\cdot} X)$

Metamath Proof Explorer

Theorem lincdifsn

Proof