lbsdiflsp0

Description: The linear spans of two disjunct independent sets only have a trivial intersection. This can be seen as the opposite direction of lindsun . (Contributed by Thierry Arnoux, 17-May-2023)

	Ref	Expression
Hypotheses	lbsdiflsp0.j	$⊢ J = LBasis (W)$
	lbsdiflsp0.n	$⊢ N = LSpan (W)$
	lbsdiflsp0.1	$⊢ \underset{˙}{0} = 0_{W}$
Assertion	lbsdiflsp0	$⊢ (W \in LVec \land B \in J \land V \subseteq B) \to N (B ∖ V) \cap N (V) = \{\underset{˙}{0}\}$

Proof

Step	Hyp	Ref	Expression
1		lbsdiflsp0.j	$⊢ J = LBasis (W)$
2		lbsdiflsp0.n	$⊢ N = LSpan (W)$
3		lbsdiflsp0.1	$⊢ \underset{˙}{0} = 0_{W}$
4		simp-4r	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)$
5		fveq2	$⊢ u = v \to a (u) = a (v)$
6		id	$⊢ u = v \to u = v$
7	5 6	oveq12d	$⊢ u = v \to a (u) \cdot_{W} u = a (v) \cdot_{W} v$
8	7	cbvmptv	$⊢ (u \in V ⟼ a (u) \cdot_{W} u) = (v \in V ⟼ a (v) \cdot_{W} v)$
9	8	oveq2i	$⊢ \underset{u \in V}{\sum_{W}} (a (u) \cdot_{W} u) = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)$
10	4 9	eqtr4di	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to x = \underset{u \in V}{\sum_{W}} (a (u) \cdot_{W} u)$
11		simp-4r	$⊢ ((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \to {finSupp}_{0_{Scalar (W)}} (a)$
12		simpr	$⊢ ((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \to {finSupp}_{0_{Scalar (W)}} (b)$
13		simp-8l	$⊢ ((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \to W \in LVec$
14		simplr	$⊢ ((W \in LVec \land B \in J) \land V \subseteq B) \to B \in J$
15	14	ad6antr	$⊢ ((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \to B \in J$
16		simpr	$⊢ ((W \in LVec \land B \in J) \land V \subseteq B) \to V \subseteq B$
17	16	ad6antr	$⊢ ((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \to V \subseteq B$
18		simp-5r	$⊢ ((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \to a \in ({Base}_{Scalar (W)}^{V})$
19		fvexd	$⊢ ((W \in LVec \land B \in J) \land V \subseteq B) \to {Base}_{Scalar (W)} \in V$
20	14 16	ssexd	$⊢ ((W \in LVec \land B \in J) \land V \subseteq B) \to V \in V$
21	19 20	elmapd	$⊢ ((W \in LVec \land B \in J) \land V \subseteq B) \to (a \in ({Base}_{Scalar (W)}^{V}) \leftrightarrow a : V ⟶ {Base}_{Scalar (W)})$
22	21	biimpa	$⊢ (((W \in LVec \land B \in J) \land V \subseteq B) \land a \in ({Base}_{Scalar (W)}^{V})) \to a : V ⟶ {Base}_{Scalar (W)}$
23	13 15 17 18 22	syl1111anc	$⊢ ((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \to a : V ⟶ {Base}_{Scalar (W)}$
24		simplr	$⊢ ((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \to b \in ({Base}_{Scalar (W)}^{(B ∖ V)})$
25		lveclmod	$⊢ W \in LVec \to W \in LMod$
26	25	ad2antrr	$⊢ ((W \in LVec \land B \in J) \land V \subseteq B) \to W \in LMod$
27		eqid	$⊢ {Base}_{W} = {Base}_{W}$
28	27 1	lbsss	$⊢ B \in J \to B \subseteq {Base}_{W}$
29	28	ad2antlr	$⊢ ((W \in LVec \land B \in J) \land V \subseteq B) \to B \subseteq {Base}_{W}$
30	29	ssdifssd	$⊢ ((W \in LVec \land B \in J) \land V \subseteq B) \to B ∖ V \subseteq {Base}_{W}$
31	3 27 2	0ellsp	$⊢ (W \in LMod \land B ∖ V \subseteq {Base}_{W}) \to \underset{˙}{0} \in N (B ∖ V)$
32	26 30 31	syl2anc	$⊢ ((W \in LVec \land B \in J) \land V \subseteq B) \to \underset{˙}{0} \in N (B ∖ V)$
33	32	elfvexd	$⊢ ((W \in LVec \land B \in J) \land V \subseteq B) \to B ∖ V \in V$
34	19 33	elmapd	$⊢ ((W \in LVec \land B \in J) \land V \subseteq B) \to (b \in ({Base}_{Scalar (W)}^{(B ∖ V)}) \leftrightarrow b : B ∖ V ⟶ {Base}_{Scalar (W)})$
35	34	biimpa	$⊢ (((W \in LVec \land B \in J) \land V \subseteq B) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \to b : B ∖ V ⟶ {Base}_{Scalar (W)}$
36	13 15 17 24 35	syl1111anc	$⊢ ((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \to b : B ∖ V ⟶ {Base}_{Scalar (W)}$
37		disjdif	$⊢ V \cap (B ∖ V) = \emptyset$
38	37	a1i	$⊢ ((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \to V \cap (B ∖ V) = \emptyset$
39	23 36 38	fun2d	$⊢ ((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \to (a \cup b) : V \cup (B ∖ V) ⟶ {Base}_{Scalar (W)}$
40		undif	$⊢ V \subseteq B \leftrightarrow V \cup (B ∖ V) = B$
41	17 40	sylib	$⊢ ((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \to V \cup (B ∖ V) = B$
42	41	feq2d	$⊢ ((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \to ((a \cup b) : V \cup (B ∖ V) ⟶ {Base}_{Scalar (W)} \leftrightarrow (a \cup b) : B ⟶ {Base}_{Scalar (W)})$
43	39 42	mpbid	$⊢ ((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \to (a \cup b) : B ⟶ {Base}_{Scalar (W)}$
44	43	ffund	$⊢ ((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \to Fun (a \cup b)$
45	44	fsuppunbi	$⊢ ((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \to ({finSupp}_{0_{Scalar (W)}} ((a \cup b)) \leftrightarrow ({finSupp}_{0_{Scalar (W)}} (a) \land {finSupp}_{0_{Scalar (W)}} (b)))$
46	11 12 45	mpbir2and	$⊢ ((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \to {finSupp}_{0_{Scalar (W)}} ((a \cup b))$
47	46	adantr	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to {finSupp}_{0_{Scalar (W)}} ((a \cup b))$
48		eqid	$⊢ +_{W} = +_{W}$
49		lmodcmn	$⊢ W \in LMod \to W \in CMnd$
50	25 49	syl	$⊢ W \in LVec \to W \in CMnd$
51	50	ad9antr	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to W \in CMnd$
52	14	ad7antr	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to B \in J$
53	26	ad8antr	$⊢ ((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in B) \to W \in LMod$
54		elmapfn	$⊢ a \in ({Base}_{Scalar (W)}^{V}) \to a Fn V$
55	54	ad6antlr	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to a Fn V$
56	55	adantr	$⊢ ((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in V) \to a Fn V$
57		elmapfn	$⊢ b \in ({Base}_{Scalar (W)}^{(B ∖ V)}) \to b Fn (B ∖ V)$
58	57	ad3antlr	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to b Fn (B ∖ V)$
59	58	adantr	$⊢ ((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in V) \to b Fn (B ∖ V)$
60	37	a1i	$⊢ ((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in V) \to V \cap (B ∖ V) = \emptyset$
61		simpr	$⊢ ((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in V) \to u \in V$
62		fvun1	$⊢ (a Fn V \land b Fn (B ∖ V) \land (V \cap (B ∖ V) = \emptyset \land u \in V)) \to (a \cup b) (u) = a (u)$
63	56 59 60 61 62	syl112anc	$⊢ ((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in V) \to (a \cup b) (u) = a (u)$
64	63	adantlr	$⊢ (((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in B) \land u \in V) \to (a \cup b) (u) = a (u)$
65	23	ad3antrrr	$⊢ (((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in B) \land u \in V) \to a : V ⟶ {Base}_{Scalar (W)}$
66		simpr	$⊢ (((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in B) \land u \in V) \to u \in V$
67	65 66	ffvelrnd	$⊢ (((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in B) \land u \in V) \to a (u) \in {Base}_{Scalar (W)}$
68	64 67	eqeltrd	$⊢ (((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in B) \land u \in V) \to (a \cup b) (u) \in {Base}_{Scalar (W)}$
69	55	adantr	$⊢ ((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in (B ∖ V)) \to a Fn V$
70	58	adantr	$⊢ ((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in (B ∖ V)) \to b Fn (B ∖ V)$
71	37	a1i	$⊢ ((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in (B ∖ V)) \to V \cap (B ∖ V) = \emptyset$
72		simpr	$⊢ ((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in (B ∖ V)) \to u \in (B ∖ V)$
73		fvun2	$⊢ (a Fn V \land b Fn (B ∖ V) \land (V \cap (B ∖ V) = \emptyset \land u \in (B ∖ V))) \to (a \cup b) (u) = b (u)$
74	69 70 71 72 73	syl112anc	$⊢ ((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in (B ∖ V)) \to (a \cup b) (u) = b (u)$
75	74	adantlr	$⊢ (((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in B) \land u \in (B ∖ V)) \to (a \cup b) (u) = b (u)$
76	36	ad3antrrr	$⊢ (((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in B) \land u \in (B ∖ V)) \to b : B ∖ V ⟶ {Base}_{Scalar (W)}$
77		simpr	$⊢ (((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in B) \land u \in (B ∖ V)) \to u \in (B ∖ V)$
78	76 77	ffvelrnd	$⊢ (((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in B) \land u \in (B ∖ V)) \to b (u) \in {Base}_{Scalar (W)}$
79	75 78	eqeltrd	$⊢ (((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in B) \land u \in (B ∖ V)) \to (a \cup b) (u) \in {Base}_{Scalar (W)}$
80		simpr	$⊢ ((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in B) \to u \in B$
81	40	biimpi	$⊢ V \subseteq B \to V \cup (B ∖ V) = B$
82	81	ad8antlr	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to V \cup (B ∖ V) = B$
83	82	eqcomd	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to B = V \cup (B ∖ V)$
84	83	adantr	$⊢ ((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in B) \to B = V \cup (B ∖ V)$
85	80 84	eleqtrd	$⊢ ((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in B) \to u \in (V \cup (B ∖ V))$
86		elun	$⊢ u \in (V \cup (B ∖ V)) \leftrightarrow (u \in V \lor u \in (B ∖ V))$
87	85 86	sylib	$⊢ ((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in B) \to (u \in V \lor u \in (B ∖ V))$
88	68 79 87	mpjaodan	$⊢ ((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in B) \to (a \cup b) (u) \in {Base}_{Scalar (W)}$
89	29	ad8antr	$⊢ ((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in B) \to B \subseteq {Base}_{W}$
90	89 80	sseldd	$⊢ ((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in B) \to u \in {Base}_{W}$
91		eqid	$⊢ Scalar (W) = Scalar (W)$
92		eqid	$⊢ \cdot_{W} = \cdot_{W}$
93		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
94	27 91 92 93	lmodvscl	$⊢ (W \in LMod \land (a \cup b) (u) \in {Base}_{Scalar (W)} \land u \in {Base}_{W}) \to (a \cup b) (u) \cdot_{W} u \in {Base}_{W}$
95	53 88 90 94	syl3anc	$⊢ ((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in B) \to (a \cup b) (u) \cdot_{W} u \in {Base}_{W}$
96		simp-9l	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to W \in LVec$
97	96 25	syl	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to W \in LMod$
98		eqidd	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to Scalar (W) = Scalar (W)$
99		eqid	$⊢ 0_{Scalar (W)} = 0_{Scalar (W)}$
100	43	adantr	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to (a \cup b) : B ⟶ {Base}_{Scalar (W)}$
101	100	feqmptd	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to a \cup b = (u \in B ⟼ (a \cup b) (u))$
102	101 47	eqbrtrrd	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to {finSupp}_{0_{Scalar (W)}} ((u \in B ⟼ (a \cup b) (u)))$
103	52 97 98 27 88 90 3 99 92 102	mptscmfsupp0	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to {finSupp}_{\underset{˙}{0}} ((u \in B ⟼ (a \cup b) (u) \cdot_{W} u))$
104	37	a1i	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to V \cap (B ∖ V) = \emptyset$
105	27 3 48 51 52 95 103 104 83	gsumsplit2	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to \underset{u \in B}{\sum_{W}} ((a \cup b) (u) \cdot_{W} u) = (\underset{u \in V}{\sum_{W}}, ((a \cup b) (u) \cdot_{W} u)) +_{W} (\underset{u \in B ∖ V}{\sum_{W}}, ((a \cup b) (u) \cdot_{W} u))$
106	63	oveq1d	$⊢ ((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in V) \to (a \cup b) (u) \cdot_{W} u = a (u) \cdot_{W} u$
107	106	mpteq2dva	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to (u \in V ⟼ (a \cup b) (u) \cdot_{W} u) = (u \in V ⟼ a (u) \cdot_{W} u)$
108	107	oveq2d	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to \underset{u \in V}{\sum_{W}} ((a \cup b) (u) \cdot_{W} u) = \underset{u \in V}{\sum_{W}} (a (u) \cdot_{W} u)$
109	74	oveq1d	$⊢ ((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in (B ∖ V)) \to (a \cup b) (u) \cdot_{W} u = b (u) \cdot_{W} u$
110	109	mpteq2dva	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to (u \in (B ∖ V) ⟼ (a \cup b) (u) \cdot_{W} u) = (u \in (B ∖ V) ⟼ b (u) \cdot_{W} u)$
111	110	oveq2d	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to \underset{u \in B ∖ V}{\sum_{W}} ((a \cup b) (u) \cdot_{W} u) = \underset{u \in B ∖ V}{\sum_{W}} (b (u) \cdot_{W} u)$
112	108 111	oveq12d	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to (\underset{u \in V}{\sum_{W}}, ((a \cup b) (u) \cdot_{W} u)) +_{W} (\underset{u \in B ∖ V}{\sum_{W}}, ((a \cup b) (u) \cdot_{W} u)) = (\underset{u \in V}{\sum_{W}}, (a (u) \cdot_{W} u)) +_{W} (\underset{u \in B ∖ V}{\sum_{W}}, (b (u) \cdot_{W} u))$
113		simpr	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)$
114		fveq2	$⊢ u = v \to b (u) = b (v)$
115	114 6	oveq12d	$⊢ u = v \to b (u) \cdot_{W} u = b (v) \cdot_{W} v$
116	115	cbvmptv	$⊢ (u \in (B ∖ V) ⟼ b (u) \cdot_{W} u) = (v \in (B ∖ V) ⟼ b (v) \cdot_{W} v)$
117	116	oveq2i	$⊢ \underset{u \in B ∖ V}{\sum_{W}} (b (u) \cdot_{W} u) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)$
118	113 117	eqtr4di	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to {inv}_{g} (W) (x) = \underset{u \in B ∖ V}{\sum_{W}} (b (u) \cdot_{W} u)$
119	10 118	oveq12d	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to x +_{W} {inv}_{g} (W) (x) = (\underset{u \in V}{\sum_{W}}, (a (u) \cdot_{W} u)) +_{W} (\underset{u \in B ∖ V}{\sum_{W}}, (b (u) \cdot_{W} u))$
120		lmodgrp	$⊢ W \in LMod \to W \in Grp$
121	96 25 120	3syl	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to W \in Grp$
122	16 29	sstrd	$⊢ ((W \in LVec \land B \in J) \land V \subseteq B) \to V \subseteq {Base}_{W}$
123	27 2	lspssv	$⊢ (W \in LMod \land V \subseteq {Base}_{W}) \to N (V) \subseteq {Base}_{W}$
124	26 122 123	syl2anc	$⊢ ((W \in LVec \land B \in J) \land V \subseteq B) \to N (V) \subseteq {Base}_{W}$
125	124	ad7antr	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to N (V) \subseteq {Base}_{W}$
126		simpr	$⊢ (((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \to x \in (N (B ∖ V) \cap N (V))$
127	126	elin2d	$⊢ (((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \to x \in N (V)$
128	127	ad6antr	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to x \in N (V)$
129	125 128	sseldd	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to x \in {Base}_{W}$
130		eqid	$⊢ {inv}_{g} (W) = {inv}_{g} (W)$
131	27 48 3 130	grprinv	$⊢ (W \in Grp \land x \in {Base}_{W}) \to x +_{W} {inv}_{g} (W) (x) = \underset{˙}{0}$
132	121 129 131	syl2anc	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to x +_{W} {inv}_{g} (W) (x) = \underset{˙}{0}$
133	112 119 132	3eqtr2d	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to (\underset{u \in V}{\sum_{W}}, ((a \cup b) (u) \cdot_{W} u)) +_{W} (\underset{u \in B ∖ V}{\sum_{W}}, ((a \cup b) (u) \cdot_{W} u)) = \underset{˙}{0}$
134	105 133	eqtrd	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to \underset{u \in B}{\sum_{W}} ((a \cup b) (u) \cdot_{W} u) = \underset{˙}{0}$
135		breq1	$⊢ c = a \cup b \to ({finSupp}_{0_{Scalar (W)}} (c) \leftrightarrow {finSupp}_{0_{Scalar (W)}} ((a \cup b)))$
136		fveq1	$⊢ c = a \cup b \to c (u) = (a \cup b) (u)$
137	136	oveq1d	$⊢ c = a \cup b \to c (u) \cdot_{W} u = (a \cup b) (u) \cdot_{W} u$
138	137	mpteq2dv	$⊢ c = a \cup b \to (u \in B ⟼ c (u) \cdot_{W} u) = (u \in B ⟼ (a \cup b) (u) \cdot_{W} u)$
139	138	oveq2d	$⊢ c = a \cup b \to \underset{u \in B}{\sum_{W}} (c (u) \cdot_{W} u) = \underset{u \in B}{\sum_{W}} ((a \cup b) (u) \cdot_{W} u)$
140	139	eqeq1d	$⊢ c = a \cup b \to (\underset{u \in B}{\sum_{W}} (c (u) \cdot_{W} u) = \underset{˙}{0} \leftrightarrow \underset{u \in B}{\sum_{W}} ((a \cup b) (u) \cdot_{W} u) = \underset{˙}{0})$
141	135 140	anbi12d	$⊢ c = a \cup b \to (({finSupp}_{0_{Scalar (W)}} (c) \land \underset{u \in B}{\sum_{W}} (c (u) \cdot_{W} u) = \underset{˙}{0}) \leftrightarrow ({finSupp}_{0_{Scalar (W)}} ((a \cup b)) \land \underset{u \in B}{\sum_{W}} ((a \cup b) (u) \cdot_{W} u) = \underset{˙}{0}))$
142		eqeq1	$⊢ c = a \cup b \to (c = B \times \{0_{Scalar (W)}\} \leftrightarrow a \cup b = B \times \{0_{Scalar (W)}\})$
143	141 142	imbi12d	$⊢ c = a \cup b \to ((({finSupp}_{0_{Scalar (W)}} (c) \land \underset{u \in B}{\sum_{W}} (c (u) \cdot_{W} u) = \underset{˙}{0}) \to c = B \times \{0_{Scalar (W)}\}) \leftrightarrow (({finSupp}_{0_{Scalar (W)}} ((a \cup b)) \land \underset{u \in B}{\sum_{W}} ((a \cup b) (u) \cdot_{W} u) = \underset{˙}{0}) \to a \cup b = B \times \{0_{Scalar (W)}\}))$
144	1	lbslinds	$⊢ J \subseteq LIndS (W)$
145	144 14	sselid	$⊢ ((W \in LVec \land B \in J) \land V \subseteq B) \to B \in LIndS (W)$
146	27 93 91 92 3 99	islinds5	$⊢ (W \in LMod \land B \subseteq {Base}_{W}) \to (B \in LIndS (W) \leftrightarrow \forall c \in ({Base}_{Scalar (W)}^{B}) (({finSupp}_{0_{Scalar (W)}} (c) \land \underset{u \in B}{\sum_{W}} (c (u) \cdot_{W} u) = \underset{˙}{0}) \to c = B \times \{0_{Scalar (W)}\}))$
147	146	biimpa	$⊢ ((W \in LMod \land B \subseteq {Base}_{W}) \land B \in LIndS (W)) \to \forall c \in ({Base}_{Scalar (W)}^{B}) (({finSupp}_{0_{Scalar (W)}} (c) \land \underset{u \in B}{\sum_{W}} (c (u) \cdot_{W} u) = \underset{˙}{0}) \to c = B \times \{0_{Scalar (W)}\})$
148	26 29 145 147	syl21anc	$⊢ ((W \in LVec \land B \in J) \land V \subseteq B) \to \forall c \in ({Base}_{Scalar (W)}^{B}) (({finSupp}_{0_{Scalar (W)}} (c) \land \underset{u \in B}{\sum_{W}} (c (u) \cdot_{W} u) = \underset{˙}{0}) \to c = B \times \{0_{Scalar (W)}\})$
149	148	ad7antr	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to \forall c \in ({Base}_{Scalar (W)}^{B}) (({finSupp}_{0_{Scalar (W)}} (c) \land \underset{u \in B}{\sum_{W}} (c (u) \cdot_{W} u) = \underset{˙}{0}) \to c = B \times \{0_{Scalar (W)}\})$
150		fvexd	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to {Base}_{Scalar (W)} \in V$
151	150 52	elmapd	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to (a \cup b \in ({Base}_{Scalar (W)}^{B}) \leftrightarrow (a \cup b) : B ⟶ {Base}_{Scalar (W)})$
152	100 151	mpbird	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to a \cup b \in ({Base}_{Scalar (W)}^{B})$
153	143 149 152	rspcdva	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to (({finSupp}_{0_{Scalar (W)}} ((a \cup b)) \land \underset{u \in B}{\sum_{W}} ((a \cup b) (u) \cdot_{W} u) = \underset{˙}{0}) \to a \cup b = B \times \{0_{Scalar (W)}\})$
154	47 134 153	mp2and	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to a \cup b = B \times \{0_{Scalar (W)}\}$
155	154	reseq1d	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to {(a \cup b) ↾}_{V} = {(B \times \{0_{Scalar (W)}\}) ↾}_{V}$
156		fnunres1	$⊢ (a Fn V \land b Fn (B ∖ V) \land V \cap (B ∖ V) = \emptyset) \to {(a \cup b) ↾}_{V} = a$
157	55 58 104 156	syl3anc	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to {(a \cup b) ↾}_{V} = a$
158		xpssres	$⊢ V \subseteq B \to {(B \times \{0_{Scalar (W)}\}) ↾}_{V} = V \times \{0_{Scalar (W)}\}$
159	158	ad8antlr	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to {(B \times \{0_{Scalar (W)}\}) ↾}_{V} = V \times \{0_{Scalar (W)}\}$
160	155 157 159	3eqtr3d	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to a = V \times \{0_{Scalar (W)}\}$
161	160	adantr	$⊢ ((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in V) \to a = V \times \{0_{Scalar (W)}\}$
162	161	fveq1d	$⊢ ((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in V) \to a (u) = (V \times \{0_{Scalar (W)}\}) (u)$
163		fvex	$⊢ 0_{Scalar (W)} \in V$
164	163	fvconst2	$⊢ u \in V \to (V \times \{0_{Scalar (W)}\}) (u) = 0_{Scalar (W)}$
165	61 164	syl	$⊢ ((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in V) \to (V \times \{0_{Scalar (W)}\}) (u) = 0_{Scalar (W)}$
166	162 165	eqtrd	$⊢ ((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in V) \to a (u) = 0_{Scalar (W)}$
167	166	oveq1d	$⊢ ((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in V) \to a (u) \cdot_{W} u = 0_{Scalar (W)} \cdot_{W} u$
168	122	ad8antr	$⊢ ((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in V) \to V \subseteq {Base}_{W}$
169	168 61	sseldd	$⊢ ((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in V) \to u \in {Base}_{W}$
170	27 91 92 99 3	lmod0vs	$⊢ (W \in LMod \land u \in {Base}_{W}) \to 0_{Scalar (W)} \cdot_{W} u = \underset{˙}{0}$
171	97 169 170	syl2an2r	$⊢ ((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in V) \to 0_{Scalar (W)} \cdot_{W} u = \underset{˙}{0}$
172	167 171	eqtrd	$⊢ ((((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \land u \in V) \to a (u) \cdot_{W} u = \underset{˙}{0}$
173	172	mpteq2dva	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to (u \in V ⟼ a (u) \cdot_{W} u) = (u \in V ⟼ \underset{˙}{0})$
174	173	oveq2d	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to \underset{u \in V}{\sum_{W}} (a (u) \cdot_{W} u) = \underset{u \in V}{\sum_{W}} \underset{˙}{0}$
175		cmnmnd	$⊢ W \in CMnd \to W \in Mnd$
176	51 175	syl	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to W \in Mnd$
177	128	elfvexd	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to V \in V$
178	3	gsumz	$⊢ (W \in Mnd \land V \in V) \to \underset{u \in V}{\sum_{W}} \underset{˙}{0} = \underset{˙}{0}$
179	176 177 178	syl2anc	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to \underset{u \in V}{\sum_{W}} \underset{˙}{0} = \underset{˙}{0}$
180	10 174 179	3eqtrd	$⊢ (((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land {finSupp}_{0_{Scalar (W)}} (b)) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)) \to x = \underset{˙}{0}$
181	180	anasss	$⊢ ((((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \land b \in ({Base}_{Scalar (W)}^{(B ∖ V)})) \land ({finSupp}_{0_{Scalar (W)}} (b) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v))) \to x = \underset{˙}{0}$
182		eqid	$⊢ LSubSp (W) = LSubSp (W)$
183	27 182 2	lspcl	$⊢ (W \in LMod \land B ∖ V \subseteq {Base}_{W}) \to N (B ∖ V) \in LSubSp (W)$
184	26 30 183	syl2anc	$⊢ ((W \in LVec \land B \in J) \land V \subseteq B) \to N (B ∖ V) \in LSubSp (W)$
185	184	adantr	$⊢ (((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \to N (B ∖ V) \in LSubSp (W)$
186	182	lsssubg	$⊢ (W \in LMod \land N (B ∖ V) \in LSubSp (W)) \to N (B ∖ V) \in SubGrp (W)$
187	26 185 186	syl2an2r	$⊢ (((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \to N (B ∖ V) \in SubGrp (W)$
188	126	elin1d	$⊢ (((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \to x \in N (B ∖ V)$
189	130	subginvcl	$⊢ (N (B ∖ V) \in SubGrp (W) \land x \in N (B ∖ V)) \to {inv}_{g} (W) (x) \in N (B ∖ V)$
190	187 188 189	syl2anc	$⊢ (((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \to {inv}_{g} (W) (x) \in N (B ∖ V)$
191	2 27 93 91 99 92 26 30	ellspds	$⊢ ((W \in LVec \land B \in J) \land V \subseteq B) \to ({inv}_{g} (W) (x) \in N (B ∖ V) \leftrightarrow \exists b \in ({Base}_{Scalar (W)}^{(B ∖ V)}) ({finSupp}_{0_{Scalar (W)}} (b) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v)))$
192	191	biimpa	$⊢ (((W \in LVec \land B \in J) \land V \subseteq B) \land {inv}_{g} (W) (x) \in N (B ∖ V)) \to \exists b \in ({Base}_{Scalar (W)}^{(B ∖ V)}) ({finSupp}_{0_{Scalar (W)}} (b) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v))$
193	190 192	syldan	$⊢ (((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \to \exists b \in ({Base}_{Scalar (W)}^{(B ∖ V)}) ({finSupp}_{0_{Scalar (W)}} (b) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v))$
194	193	ad3antrrr	$⊢ ((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \to \exists b \in ({Base}_{Scalar (W)}^{(B ∖ V)}) ({finSupp}_{0_{Scalar (W)}} (b) \land {inv}_{g} (W) (x) = \underset{v \in B ∖ V}{\sum_{W}} (b (v) \cdot_{W} v))$
195	181 194	r19.29a	$⊢ ((((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land {finSupp}_{0_{Scalar (W)}} (a)) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)) \to x = \underset{˙}{0}$
196	195	anasss	$⊢ (((((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \land a \in ({Base}_{Scalar (W)}^{V})) \land ({finSupp}_{0_{Scalar (W)}} (a) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v))) \to x = \underset{˙}{0}$
197	2 27 93 91 99 92 26 122	ellspds	$⊢ ((W \in LVec \land B \in J) \land V \subseteq B) \to (x \in N (V) \leftrightarrow \exists a \in ({Base}_{Scalar (W)}^{V}) ({finSupp}_{0_{Scalar (W)}} (a) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v)))$
198	197	biimpa	$⊢ (((W \in LVec \land B \in J) \land V \subseteq B) \land x \in N (V)) \to \exists a \in ({Base}_{Scalar (W)}^{V}) ({finSupp}_{0_{Scalar (W)}} (a) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v))$
199	127 198	syldan	$⊢ (((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \to \exists a \in ({Base}_{Scalar (W)}^{V}) ({finSupp}_{0_{Scalar (W)}} (a) \land x = \underset{v \in V}{\sum_{W}} (a (v) \cdot_{W} v))$
200	196 199	r19.29a	$⊢ (((W \in LVec \land B \in J) \land V \subseteq B) \land x \in (N (B ∖ V) \cap N (V))) \to x = \underset{˙}{0}$
201	3 27 2	0ellsp	$⊢ (W \in LMod \land V \subseteq {Base}_{W}) \to \underset{˙}{0} \in N (V)$
202	26 122 201	syl2anc	$⊢ ((W \in LVec \land B \in J) \land V \subseteq B) \to \underset{˙}{0} \in N (V)$
203	32 202	elind	$⊢ ((W \in LVec \land B \in J) \land V \subseteq B) \to \underset{˙}{0} \in (N (B ∖ V) \cap N (V))$
204	200 203	eqsnd	$⊢ ((W \in LVec \land B \in J) \land V \subseteq B) \to N (B ∖ V) \cap N (V) = \{\underset{˙}{0}\}$
205	204	3impa	$⊢ (W \in LVec \land B \in J \land V \subseteq B) \to N (B ∖ V) \cap N (V) = \{\underset{˙}{0}\}$

Metamath Proof Explorer

Theorem lbsdiflsp0

Proof