lindsadd

Description: In a vector space, the union of an independent set and a vector not in its span is an independent set. (Contributed by Brendan Leahy, 4-Mar-2023)

		Ref	Expression
	Assertion	lindsadd	$⊢ (W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \to F \cup \{X\} \in LIndS (W)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{W} = {Base}_{W}$
2	1	linds1	$⊢ F \in LIndS (W) \to F \subseteq {Base}_{W}$
3		eldifi	$⊢ X \in ({Base}_{W} ∖ LSpan (W) (F)) \to X \in {Base}_{W}$
4	3	snssd	$⊢ X \in ({Base}_{W} ∖ LSpan (W) (F)) \to \{X\} \subseteq {Base}_{W}$
5		unss	$⊢ (F \subseteq {Base}_{W} \land \{X\} \subseteq {Base}_{W}) \leftrightarrow F \cup \{X\} \subseteq {Base}_{W}$
6	5	biimpi	$⊢ (F \subseteq {Base}_{W} \land \{X\} \subseteq {Base}_{W}) \to F \cup \{X\} \subseteq {Base}_{W}$
7	2 4 6	syl2an	$⊢ (F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \to F \cup \{X\} \subseteq {Base}_{W}$
8	7	3adant1	$⊢ (W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \to F \cup \{X\} \subseteq {Base}_{W}$
9		eldifn	$⊢ X \in ({Base}_{W} ∖ LSpan (W) (F)) \to \neg X \in LSpan (W) (F)$
10	9	3ad2ant3	$⊢ (W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \to \neg X \in LSpan (W) (F)$
11	10	adantr	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \land (x \in F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to \neg X \in LSpan (W) (F)$
12		simpll1	$⊢ (((W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \land (x \in F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \land x \in LSpan (W) ((F ∖ \{x\}) \cup \{X\})) \to W \in LVec$
13	2	ssdifssd	$⊢ F \in LIndS (W) \to F ∖ \{x\} \subseteq {Base}_{W}$
14	13	3ad2ant2	$⊢ (W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \to F ∖ \{x\} \subseteq {Base}_{W}$
15	14	ad2antrr	$⊢ (((W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \land (x \in F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \land x \in LSpan (W) ((F ∖ \{x\}) \cup \{X\})) \to F ∖ \{x\} \subseteq {Base}_{W}$
16	3	3ad2ant3	$⊢ (W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \to X \in {Base}_{W}$
17	16	ad2antrr	$⊢ (((W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \land (x \in F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \land x \in LSpan (W) ((F ∖ \{x\}) \cup \{X\})) \to X \in {Base}_{W}$
18		simpr	$⊢ (((W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \land (x \in F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \land x \in LSpan (W) ((F ∖ \{x\}) \cup \{X\})) \to x \in LSpan (W) ((F ∖ \{x\}) \cup \{X\})$
19		lveclmod	$⊢ W \in LVec \to W \in LMod$
20	19	ad2antrr	$⊢ ((W \in LVec \land F \in LIndS (W)) \land (x \in F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to W \in LMod$
21		eqid	$⊢ Scalar (W) = Scalar (W)$
22	21	lmodring	$⊢ W \in LMod \to Scalar (W) \in Ring$
23	19 22	syl	$⊢ W \in LVec \to Scalar (W) \in Ring$
24		eqid	$⊢ 0_{Scalar (W)} = 0_{Scalar (W)}$
25		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
26	24 25	ringelnzr	$⊢ (Scalar (W) \in Ring \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\})) \to Scalar (W) \in NzRing$
27	23 26	sylan	$⊢ (W \in LVec \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\})) \to Scalar (W) \in NzRing$
28	27	ad2ant2rl	$⊢ ((W \in LVec \land F \in LIndS (W)) \land (x \in F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to Scalar (W) \in NzRing$
29		simplr	$⊢ ((W \in LVec \land F \in LIndS (W)) \land (x \in F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to F \in LIndS (W)$
30		simprl	$⊢ ((W \in LVec \land F \in LIndS (W)) \land (x \in F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to x \in F$
31		eqid	$⊢ LSpan (W) = LSpan (W)$
32	31 21	lindsind2	$⊢ ((W \in LMod \land Scalar (W) \in NzRing) \land F \in LIndS (W) \land x \in F) \to \neg x \in LSpan (W) (F ∖ \{x\})$
33	20 28 29 30 32	syl211anc	$⊢ ((W \in LVec \land F \in LIndS (W)) \land (x \in F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to \neg x \in LSpan (W) (F ∖ \{x\})$
34	33	3adantl3	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \land (x \in F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to \neg x \in LSpan (W) (F ∖ \{x\})$
35	34	adantr	$⊢ (((W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \land (x \in F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \land x \in LSpan (W) ((F ∖ \{x\}) \cup \{X\})) \to \neg x \in LSpan (W) (F ∖ \{x\})$
36	18 35	eldifd	$⊢ (((W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \land (x \in F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \land x \in LSpan (W) ((F ∖ \{x\}) \cup \{X\})) \to x \in (LSpan (W) ((F ∖ \{x\}) \cup \{X\}) ∖ LSpan (W) (F ∖ \{x\}))$
37		eqid	$⊢ LSubSp (W) = LSubSp (W)$
38	1 37 31	lspsolv	$⊢ (W \in LVec \land (F ∖ \{x\} \subseteq {Base}_{W} \land X \in {Base}_{W} \land x \in (LSpan (W) ((F ∖ \{x\}) \cup \{X\}) ∖ LSpan (W) (F ∖ \{x\})))) \to X \in LSpan (W) ((F ∖ \{x\}) \cup \{x\})$
39	12 15 17 36 38	syl13anc	$⊢ (((W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \land (x \in F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \land x \in LSpan (W) ((F ∖ \{x\}) \cup \{X\})) \to X \in LSpan (W) ((F ∖ \{x\}) \cup \{x\})$
40	39	ex	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \land (x \in F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to (x \in LSpan (W) ((F ∖ \{x\}) \cup \{X\}) \to X \in LSpan (W) ((F ∖ \{x\}) \cup \{x\}))$
41		eldif	$⊢ X \in ({Base}_{W} ∖ LSpan (W) (F)) \leftrightarrow (X \in {Base}_{W} \land \neg X \in LSpan (W) (F))$
42		snssi	$⊢ X \in F \to \{X\} \subseteq F$
43	1 31	lspss	$⊢ (W \in LMod \land F \subseteq {Base}_{W} \land \{X\} \subseteq F) \to LSpan (W) (\{X\}) \subseteq LSpan (W) (F)$
44	19 2 42 43	syl3an	$⊢ (W \in LVec \land F \in LIndS (W) \land X \in F) \to LSpan (W) (\{X\}) \subseteq LSpan (W) (F)$
45	44	ad4ant124	$⊢ (((W \in LVec \land F \in LIndS (W)) \land X \in {Base}_{W}) \land X \in F) \to LSpan (W) (\{X\}) \subseteq LSpan (W) (F)$
46	1 31	lspsnid	$⊢ (W \in LMod \land X \in {Base}_{W}) \to X \in LSpan (W) (\{X\})$
47	19 46	sylan	$⊢ (W \in LVec \land X \in {Base}_{W}) \to X \in LSpan (W) (\{X\})$
48	47	ad4ant13	$⊢ (((W \in LVec \land F \in LIndS (W)) \land X \in {Base}_{W}) \land X \in F) \to X \in LSpan (W) (\{X\})$
49	45 48	sseldd	$⊢ (((W \in LVec \land F \in LIndS (W)) \land X \in {Base}_{W}) \land X \in F) \to X \in LSpan (W) (F)$
50	49	ex	$⊢ ((W \in LVec \land F \in LIndS (W)) \land X \in {Base}_{W}) \to (X \in F \to X \in LSpan (W) (F))$
51	50	con3d	$⊢ ((W \in LVec \land F \in LIndS (W)) \land X \in {Base}_{W}) \to (\neg X \in LSpan (W) (F) \to \neg X \in F)$
52	51	expimpd	$⊢ (W \in LVec \land F \in LIndS (W)) \to ((X \in {Base}_{W} \land \neg X \in LSpan (W) (F)) \to \neg X \in F)$
53	52	3impia	$⊢ (W \in LVec \land F \in LIndS (W) \land (X \in {Base}_{W} \land \neg X \in LSpan (W) (F))) \to \neg X \in F$
54	41 53	syl3an3b	$⊢ (W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \to \neg X \in F$
55		eleq1	$⊢ X = x \to (X \in F \leftrightarrow x \in F)$
56	55	notbid	$⊢ X = x \to (\neg X \in F \leftrightarrow \neg x \in F)$
57	54 56	syl5ibcom	$⊢ (W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \to (X = x \to \neg x \in F)$
58	57	necon2ad	$⊢ (W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \to (x \in F \to X \neq x)$
59	58	imp	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \land x \in F) \to X \neq x$
60		disjsn2	$⊢ X \neq x \to \{X\} \cap \{x\} = \emptyset$
61	59 60	syl	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \land x \in F) \to \{X\} \cap \{x\} = \emptyset$
62		disj3	$⊢ \{X\} \cap \{x\} = \emptyset \leftrightarrow \{X\} = \{X\} ∖ \{x\}$
63	61 62	sylib	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \land x \in F) \to \{X\} = \{X\} ∖ \{x\}$
64	63	uneq2d	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \land x \in F) \to (F ∖ \{x\}) \cup \{X\} = (F ∖ \{x\}) \cup (\{X\} ∖ \{x\})$
65		difundir	$⊢ (F \cup \{X\}) ∖ \{x\} = (F ∖ \{x\}) \cup (\{X\} ∖ \{x\})$
66	64 65	eqtr4di	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \land x \in F) \to (F ∖ \{x\}) \cup \{X\} = (F \cup \{X\}) ∖ \{x\}$
67	66	fveq2d	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \land x \in F) \to LSpan (W) ((F ∖ \{x\}) \cup \{X\}) = LSpan (W) ((F \cup \{X\}) ∖ \{x\})$
68	67	eleq2d	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \land x \in F) \to (x \in LSpan (W) ((F ∖ \{x\}) \cup \{X\}) \leftrightarrow x \in LSpan (W) ((F \cup \{X\}) ∖ \{x\}))$
69	68	adantrr	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \land (x \in F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to (x \in LSpan (W) ((F ∖ \{x\}) \cup \{X\}) \leftrightarrow x \in LSpan (W) ((F \cup \{X\}) ∖ \{x\}))$
70		simpl	$⊢ (W \in LVec \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\})) \to W \in LVec$
71		eldifsn	$⊢ k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \leftrightarrow (k \in {Base}_{Scalar (W)} \land k \neq 0_{Scalar (W)})$
72	71	bilani	$⊢ (W \in LVec \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\})) \to (k \in {Base}_{Scalar (W)} \land k \neq 0_{Scalar (W)})$
73	2	sselda	$⊢ (F \in LIndS (W) \land x \in F) \to x \in {Base}_{W}$
74		eqid	$⊢ \cdot_{W} = \cdot_{W}$
75	1 21 74 25 24 31	lspsnvs	$⊢ (W \in LVec \land (k \in {Base}_{Scalar (W)} \land k \neq 0_{Scalar (W)}) \land x \in {Base}_{W}) \to LSpan (W) (\{k \cdot_{W} x\}) = LSpan (W) (\{x\})$
76	70 72 73 75	syl2an3an	$⊢ ((W \in LVec \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\})) \land (F \in LIndS (W) \land x \in F)) \to LSpan (W) (\{k \cdot_{W} x\}) = LSpan (W) (\{x\})$
77	76	an42s	$⊢ ((W \in LVec \land F \in LIndS (W)) \land (x \in F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to LSpan (W) (\{k \cdot_{W} x\}) = LSpan (W) (\{x\})$
78	77	sseq1d	$⊢ ((W \in LVec \land F \in LIndS (W)) \land (x \in F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to (LSpan (W) (\{k \cdot_{W} x\}) \subseteq LSpan (W) ((F \cup \{X\}) ∖ \{x\}) \leftrightarrow LSpan (W) (\{x\}) \subseteq LSpan (W) ((F \cup \{X\}) ∖ \{x\}))$
79	78	3adantl3	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in {Base}_{W}) \land (x \in F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to (LSpan (W) (\{k \cdot_{W} x\}) \subseteq LSpan (W) ((F \cup \{X\}) ∖ \{x\}) \leftrightarrow LSpan (W) (\{x\}) \subseteq LSpan (W) ((F \cup \{X\}) ∖ \{x\}))$
80		eldifi	$⊢ k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \to k \in {Base}_{Scalar (W)}$
81	19	3ad2ant1	$⊢ (W \in LVec \land F \in LIndS (W) \land X \in {Base}_{W}) \to W \in LMod$
82	81	adantr	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in {Base}_{W}) \land (x \in F \land k \in {Base}_{Scalar (W)})) \to W \in LMod$
83		snssi	$⊢ X \in {Base}_{W} \to \{X\} \subseteq {Base}_{W}$
84	2 83 6	syl2an	$⊢ (F \in LIndS (W) \land X \in {Base}_{W}) \to F \cup \{X\} \subseteq {Base}_{W}$
85	84	ssdifssd	$⊢ (F \in LIndS (W) \land X \in {Base}_{W}) \to (F \cup \{X\}) ∖ \{x\} \subseteq {Base}_{W}$
86	1 37 31	lspcl	$⊢ (W \in LMod \land (F \cup \{X\}) ∖ \{x\} \subseteq {Base}_{W}) \to LSpan (W) ((F \cup \{X\}) ∖ \{x\}) \in LSubSp (W)$
87	19 85 86	syl2an	$⊢ (W \in LVec \land (F \in LIndS (W) \land X \in {Base}_{W})) \to LSpan (W) ((F \cup \{X\}) ∖ \{x\}) \in LSubSp (W)$
88	87	3impb	$⊢ (W \in LVec \land F \in LIndS (W) \land X \in {Base}_{W}) \to LSpan (W) ((F \cup \{X\}) ∖ \{x\}) \in LSubSp (W)$
89	88	adantr	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in {Base}_{W}) \land (x \in F \land k \in {Base}_{Scalar (W)})) \to LSpan (W) ((F \cup \{X\}) ∖ \{x\}) \in LSubSp (W)$
90	19	anim1i	$⊢ (W \in LVec \land k \in {Base}_{Scalar (W)}) \to (W \in LMod \land k \in {Base}_{Scalar (W)})$
91	1 21 74 25	lmodvscl	$⊢ (W \in LMod \land k \in {Base}_{Scalar (W)} \land x \in {Base}_{W}) \to k \cdot_{W} x \in {Base}_{W}$
92	91	3expa	$⊢ ((W \in LMod \land k \in {Base}_{Scalar (W)}) \land x \in {Base}_{W}) \to k \cdot_{W} x \in {Base}_{W}$
93	90 73 92	syl2an	$⊢ ((W \in LVec \land k \in {Base}_{Scalar (W)}) \land (F \in LIndS (W) \land x \in F)) \to k \cdot_{W} x \in {Base}_{W}$
94	93	an42s	$⊢ ((W \in LVec \land F \in LIndS (W)) \land (x \in F \land k \in {Base}_{Scalar (W)})) \to k \cdot_{W} x \in {Base}_{W}$
95	94	3adantl3	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in {Base}_{W}) \land (x \in F \land k \in {Base}_{Scalar (W)})) \to k \cdot_{W} x \in {Base}_{W}$
96	1 37 31 82 89 95	ellspsn5b	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in {Base}_{W}) \land (x \in F \land k \in {Base}_{Scalar (W)})) \to (k \cdot_{W} x \in LSpan (W) ((F \cup \{X\}) ∖ \{x\}) \leftrightarrow LSpan (W) (\{k \cdot_{W} x\}) \subseteq LSpan (W) ((F \cup \{X\}) ∖ \{x\}))$
97	80 96	sylanr2	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in {Base}_{W}) \land (x \in F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to (k \cdot_{W} x \in LSpan (W) ((F \cup \{X\}) ∖ \{x\}) \leftrightarrow LSpan (W) (\{k \cdot_{W} x\}) \subseteq LSpan (W) ((F \cup \{X\}) ∖ \{x\}))$
98	81	adantr	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in {Base}_{W}) \land x \in F) \to W \in LMod$
99	88	adantr	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in {Base}_{W}) \land x \in F) \to LSpan (W) ((F \cup \{X\}) ∖ \{x\}) \in LSubSp (W)$
100	73	3ad2antl2	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in {Base}_{W}) \land x \in F) \to x \in {Base}_{W}$
101	1 37 31 98 99 100	ellspsn5b	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in {Base}_{W}) \land x \in F) \to (x \in LSpan (W) ((F \cup \{X\}) ∖ \{x\}) \leftrightarrow LSpan (W) (\{x\}) \subseteq LSpan (W) ((F \cup \{X\}) ∖ \{x\}))$
102	101	adantrr	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in {Base}_{W}) \land (x \in F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to (x \in LSpan (W) ((F \cup \{X\}) ∖ \{x\}) \leftrightarrow LSpan (W) (\{x\}) \subseteq LSpan (W) ((F \cup \{X\}) ∖ \{x\}))$
103	79 97 102	3bitr4rd	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in {Base}_{W}) \land (x \in F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to (x \in LSpan (W) ((F \cup \{X\}) ∖ \{x\}) \leftrightarrow k \cdot_{W} x \in LSpan (W) ((F \cup \{X\}) ∖ \{x\}))$
104	3 103	syl3anl3	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \land (x \in F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to (x \in LSpan (W) ((F \cup \{X\}) ∖ \{x\}) \leftrightarrow k \cdot_{W} x \in LSpan (W) ((F \cup \{X\}) ∖ \{x\}))$
105	69 104	bitrd	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \land (x \in F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to (x \in LSpan (W) ((F ∖ \{x\}) \cup \{X\}) \leftrightarrow k \cdot_{W} x \in LSpan (W) ((F \cup \{X\}) ∖ \{x\}))$
106		difsnid	$⊢ x \in F \to (F ∖ \{x\}) \cup \{x\} = F$
107	106	fveq2d	$⊢ x \in F \to LSpan (W) ((F ∖ \{x\}) \cup \{x\}) = LSpan (W) (F)$
108	107	eleq2d	$⊢ x \in F \to (X \in LSpan (W) ((F ∖ \{x\}) \cup \{x\}) \leftrightarrow X \in LSpan (W) (F))$
109	108	ad2antrl	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \land (x \in F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to (X \in LSpan (W) ((F ∖ \{x\}) \cup \{x\}) \leftrightarrow X \in LSpan (W) (F))$
110	40 105 109	3imtr3d	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \land (x \in F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to (k \cdot_{W} x \in LSpan (W) ((F \cup \{X\}) ∖ \{x\}) \to X \in LSpan (W) (F))$
111	11 110	mtod	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \land (x \in F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to \neg k \cdot_{W} x \in LSpan (W) ((F \cup \{X\}) ∖ \{x\})$
112	111	ralrimivva	$⊢ (W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \to \forall x \in F \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} x \in LSpan (W) ((F \cup \{X\}) ∖ \{x\})$
113	10	adantr	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\})) \to \neg X \in LSpan (W) (F)$
114		difsn	$⊢ \neg X \in F \to F ∖ \{X\} = F$
115	54 114	syl	$⊢ (W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \to F ∖ \{X\} = F$
116	115	fveq2d	$⊢ (W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \to LSpan (W) (F ∖ \{X\}) = LSpan (W) (F)$
117	116	eleq2d	$⊢ (W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \to (k \cdot_{W} X \in LSpan (W) (F ∖ \{X\}) \leftrightarrow k \cdot_{W} X \in LSpan (W) (F))$
118	117	adantr	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\})) \to (k \cdot_{W} X \in LSpan (W) (F ∖ \{X\}) \leftrightarrow k \cdot_{W} X \in LSpan (W) (F))$
119	1 21 74 25 24 31	lspsnvs	$⊢ (W \in LVec \land (k \in {Base}_{Scalar (W)} \land k \neq 0_{Scalar (W)}) \land X \in {Base}_{W}) \to LSpan (W) (\{k \cdot_{W} X\}) = LSpan (W) (\{X\})$
120	119	3expa	$⊢ ((W \in LVec \land (k \in {Base}_{Scalar (W)} \land k \neq 0_{Scalar (W)})) \land X \in {Base}_{W}) \to LSpan (W) (\{k \cdot_{W} X\}) = LSpan (W) (\{X\})$
121	120	an32s	$⊢ ((W \in LVec \land X \in {Base}_{W}) \land (k \in {Base}_{Scalar (W)} \land k \neq 0_{Scalar (W)})) \to LSpan (W) (\{k \cdot_{W} X\}) = LSpan (W) (\{X\})$
122	71 121	sylan2b	$⊢ ((W \in LVec \land X \in {Base}_{W}) \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\})) \to LSpan (W) (\{k \cdot_{W} X\}) = LSpan (W) (\{X\})$
123	122	sseq1d	$⊢ ((W \in LVec \land X \in {Base}_{W}) \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\})) \to (LSpan (W) (\{k \cdot_{W} X\}) \subseteq LSpan (W) (F) \leftrightarrow LSpan (W) (\{X\}) \subseteq LSpan (W) (F))$
124	123	3adantl2	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in {Base}_{W}) \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\})) \to (LSpan (W) (\{k \cdot_{W} X\}) \subseteq LSpan (W) (F) \leftrightarrow LSpan (W) (\{X\}) \subseteq LSpan (W) (F))$
125	81	adantr	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in {Base}_{W}) \land k \in {Base}_{Scalar (W)}) \to W \in LMod$
126	1 37 31	lspcl	$⊢ (W \in LMod \land F \subseteq {Base}_{W}) \to LSpan (W) (F) \in LSubSp (W)$
127	19 2 126	syl2an	$⊢ (W \in LVec \land F \in LIndS (W)) \to LSpan (W) (F) \in LSubSp (W)$
128	127	3adant3	$⊢ (W \in LVec \land F \in LIndS (W) \land X \in {Base}_{W}) \to LSpan (W) (F) \in LSubSp (W)$
129	128	adantr	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in {Base}_{W}) \land k \in {Base}_{Scalar (W)}) \to LSpan (W) (F) \in LSubSp (W)$
130	1 21 74 25	lmodvscl	$⊢ (W \in LMod \land k \in {Base}_{Scalar (W)} \land X \in {Base}_{W}) \to k \cdot_{W} X \in {Base}_{W}$
131	130	3expa	$⊢ ((W \in LMod \land k \in {Base}_{Scalar (W)}) \land X \in {Base}_{W}) \to k \cdot_{W} X \in {Base}_{W}$
132	131	an32s	$⊢ ((W \in LMod \land X \in {Base}_{W}) \land k \in {Base}_{Scalar (W)}) \to k \cdot_{W} X \in {Base}_{W}$
133	19 132	sylanl1	$⊢ ((W \in LVec \land X \in {Base}_{W}) \land k \in {Base}_{Scalar (W)}) \to k \cdot_{W} X \in {Base}_{W}$
134	133	3adantl2	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in {Base}_{W}) \land k \in {Base}_{Scalar (W)}) \to k \cdot_{W} X \in {Base}_{W}$
135	1 37 31 125 129 134	ellspsn5b	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in {Base}_{W}) \land k \in {Base}_{Scalar (W)}) \to (k \cdot_{W} X \in LSpan (W) (F) \leftrightarrow LSpan (W) (\{k \cdot_{W} X\}) \subseteq LSpan (W) (F))$
136	80 135	sylan2	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in {Base}_{W}) \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\})) \to (k \cdot_{W} X \in LSpan (W) (F) \leftrightarrow LSpan (W) (\{k \cdot_{W} X\}) \subseteq LSpan (W) (F))$
137		simp3	$⊢ (W \in LVec \land F \in LIndS (W) \land X \in {Base}_{W}) \to X \in {Base}_{W}$
138	1 37 31 81 128 137	ellspsn5b	$⊢ (W \in LVec \land F \in LIndS (W) \land X \in {Base}_{W}) \to (X \in LSpan (W) (F) \leftrightarrow LSpan (W) (\{X\}) \subseteq LSpan (W) (F))$
139	138	adantr	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in {Base}_{W}) \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\})) \to (X \in LSpan (W) (F) \leftrightarrow LSpan (W) (\{X\}) \subseteq LSpan (W) (F))$
140	124 136 139	3bitr4d	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in {Base}_{W}) \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\})) \to (k \cdot_{W} X \in LSpan (W) (F) \leftrightarrow X \in LSpan (W) (F))$
141	3 140	syl3anl3	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\})) \to (k \cdot_{W} X \in LSpan (W) (F) \leftrightarrow X \in LSpan (W) (F))$
142	118 141	bitrd	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\})) \to (k \cdot_{W} X \in LSpan (W) (F ∖ \{X\}) \leftrightarrow X \in LSpan (W) (F))$
143	113 142	mtbird	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\})) \to \neg k \cdot_{W} X \in LSpan (W) (F ∖ \{X\})$
144	143	ralrimiva	$⊢ (W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \to \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} X \in LSpan (W) (F ∖ \{X\})$
145		oveq2	$⊢ x = X \to k \cdot_{W} x = k \cdot_{W} X$
146		sneq	$⊢ x = X \to \{x\} = \{X\}$
147	146	difeq2d	$⊢ x = X \to (F \cup \{X\}) ∖ \{x\} = (F \cup \{X\}) ∖ \{X\}$
148		difun2	$⊢ (F \cup \{X\}) ∖ \{X\} = F ∖ \{X\}$
149	147 148	eqtrdi	$⊢ x = X \to (F \cup \{X\}) ∖ \{x\} = F ∖ \{X\}$
150	149	fveq2d	$⊢ x = X \to LSpan (W) ((F \cup \{X\}) ∖ \{x\}) = LSpan (W) (F ∖ \{X\})$
151	145 150	eleq12d	$⊢ x = X \to (k \cdot_{W} x \in LSpan (W) ((F \cup \{X\}) ∖ \{x\}) \leftrightarrow k \cdot_{W} X \in LSpan (W) (F ∖ \{X\}))$
152	151	notbid	$⊢ x = X \to (\neg k \cdot_{W} x \in LSpan (W) ((F \cup \{X\}) ∖ \{x\}) \leftrightarrow \neg k \cdot_{W} X \in LSpan (W) (F ∖ \{X\}))$
153	152	ralbidv	$⊢ x = X \to (\forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} x \in LSpan (W) ((F \cup \{X\}) ∖ \{x\}) \leftrightarrow \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} X \in LSpan (W) (F ∖ \{X\}))$
154	153	ralsng	$⊢ X \in ({Base}_{W} ∖ LSpan (W) (F)) \to (\forall x \in \{X\} \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} x \in LSpan (W) ((F \cup \{X\}) ∖ \{x\}) \leftrightarrow \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} X \in LSpan (W) (F ∖ \{X\}))$
155	154	3ad2ant3	$⊢ (W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \to (\forall x \in \{X\} \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} x \in LSpan (W) ((F \cup \{X\}) ∖ \{x\}) \leftrightarrow \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} X \in LSpan (W) (F ∖ \{X\}))$
156	144 155	mpbird	$⊢ (W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \to \forall x \in \{X\} \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} x \in LSpan (W) ((F \cup \{X\}) ∖ \{x\})$
157		ralunb	$⊢ \forall x \in (F \cup \{X\}) \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} x \in LSpan (W) ((F \cup \{X\}) ∖ \{x\}) \leftrightarrow (\forall x \in F \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} x \in LSpan (W) ((F \cup \{X\}) ∖ \{x\}) \land \forall x \in \{X\} \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} x \in LSpan (W) ((F \cup \{X\}) ∖ \{x\}))$
158	112 156 157	sylanbrc	$⊢ (W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \to \forall x \in (F \cup \{X\}) \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} x \in LSpan (W) ((F \cup \{X\}) ∖ \{x\})$
159	1 74 31 21 25 24	islinds2	$⊢ W \in LVec \to (F \cup \{X\} \in LIndS (W) \leftrightarrow (F \cup \{X\} \subseteq {Base}_{W} \land \forall x \in (F \cup \{X\}) \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} x \in LSpan (W) ((F \cup \{X\}) ∖ \{x\})))$
160	159	3ad2ant1	$⊢ (W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \to (F \cup \{X\} \in LIndS (W) \leftrightarrow (F \cup \{X\} \subseteq {Base}_{W} \land \forall x \in (F \cup \{X\}) \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} x \in LSpan (W) ((F \cup \{X\}) ∖ \{x\})))$
161	8 158 160	mpbir2and	$⊢ (W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \to F \cup \{X\} \in LIndS (W)$

Metamath Proof Explorer

Theorem lindsadd

Proof