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	biimpi	$⊢ k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \to (k \in {Base}_{Scalar (W)} \land k \neq 0_{Scalar (W)})$
73	72	adantl	$⊢ (W \in LVec \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\})) \to (k \in {Base}_{Scalar (W)} \land k \neq 0_{Scalar (W)})$
74	2	sselda	$⊢ (F \in LIndS (W) \land x \in F) \to x \in {Base}_{W}$
75		eqid	$⊢ \cdot_{W} = \cdot_{W}$
76	1 21 75 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\})$
77	70 73 74 76	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\})$
78	77	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\})$
79	78	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\}))$
80	79	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\}))$
81		eldifi	$⊢ k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \to k \in {Base}_{Scalar (W)}$
82	19	3ad2ant1	$⊢ (W \in LVec \land F \in LIndS (W) \land X \in {Base}_{W}) \to W \in LMod$
83	82	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$
84		snssi	$⊢ X \in {Base}_{W} \to \{X\} \subseteq {Base}_{W}$
85	2 84 6	syl2an	$⊢ (F \in LIndS (W) \land X \in {Base}_{W}) \to F \cup \{X\} \subseteq {Base}_{W}$
86	85	ssdifssd	$⊢ (F \in LIndS (W) \land X \in {Base}_{W}) \to (F \cup \{X\}) ∖ \{x\} \subseteq {Base}_{W}$
87	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)$
88	19 86 87	syl2an	$⊢ (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	3impb	$⊢ (W \in LVec \land F \in LIndS (W) \land X \in {Base}_{W}) \to LSpan (W) ((F \cup \{X\}) ∖ \{x\}) \in LSubSp (W)$
90	89	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)$
91	19	anim1i	$⊢ (W \in LVec \land k \in {Base}_{Scalar (W)}) \to (W \in LMod \land k \in {Base}_{Scalar (W)})$
92	1 21 75 25	lmodvscl	$⊢ (W \in LMod \land k \in {Base}_{Scalar (W)} \land x \in {Base}_{W}) \to k \cdot_{W} x \in {Base}_{W}$
93	92	3expa	$⊢ ((W \in LMod \land k \in {Base}_{Scalar (W)}) \land x \in {Base}_{W}) \to k \cdot_{W} x \in {Base}_{W}$
94	91 74 93	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}$
95	94	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}$
96	95	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}$
97	1 37 31 83 90 96	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\}))$
98	81 97	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\}))$
99	82	adantr	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in {Base}_{W}) \land x \in F) \to W \in LMod$
100	89	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)$
101	74	3ad2antl2	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in {Base}_{W}) \land x \in F) \to x \in {Base}_{W}$
102	1 37 31 99 100 101	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\}))$
103	102	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\}))$
104	80 98 103	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\}))$
105	3 104	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\}))$
106	69 105	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\}))$
107		difsnid	$⊢ x \in F \to (F ∖ \{x\}) \cup \{x\} = F$
108	107	fveq2d	$⊢ x \in F \to LSpan (W) ((F ∖ \{x\}) \cup \{x\}) = LSpan (W) (F)$
109	108	eleq2d	$⊢ x \in F \to (X \in LSpan (W) ((F ∖ \{x\}) \cup \{x\}) \leftrightarrow X \in LSpan (W) (F))$
110	109	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))$
111	40 106 110	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))$
112	11 111	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\})$
113	112	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\})$
114	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)$
115		difsn	$⊢ \neg X \in F \to F ∖ \{X\} = F$
116	54 115	syl	$⊢ (W \in LVec \land F \in LIndS (W) \land X \in ({Base}_{W} ∖ LSpan (W) (F))) \to F ∖ \{X\} = F$
117	116	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)$
118	117	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))$
119	118	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))$
120	1 21 75 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\})$
121	120	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\})$
122	121	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\})$
123	71 122	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\})$
124	123	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))$
125	124	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))$
126	82	adantr	$⊢ ((W \in LVec \land F \in LIndS (W) \land X \in {Base}_{W}) \land k \in {Base}_{Scalar (W)}) \to W \in LMod$
127	1 37 31	lspcl	$⊢ (W \in LMod \land F \subseteq {Base}_{W}) \to LSpan (W) (F) \in LSubSp (W)$
128	19 2 127	syl2an	$⊢ (W \in LVec \land F \in LIndS (W)) \to LSpan (W) (F) \in LSubSp (W)$
129	128	3adant3	$⊢ (W \in LVec \land F \in LIndS (W) \land X \in {Base}_{W}) \to LSpan (W) (F) \in LSubSp (W)$
130	129	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)$
131	1 21 75 25	lmodvscl	$⊢ (W \in LMod \land k \in {Base}_{Scalar (W)} \land X \in {Base}_{W}) \to k \cdot_{W} X \in {Base}_{W}$
132	131	3expa	$⊢ ((W \in LMod \land k \in {Base}_{Scalar (W)}) \land X \in {Base}_{W}) \to k \cdot_{W} X \in {Base}_{W}$
133	132	an32s	$⊢ ((W \in LMod \land X \in {Base}_{W}) \land k \in {Base}_{Scalar (W)}) \to k \cdot_{W} X \in {Base}_{W}$
134	19 133	sylanl1	$⊢ ((W \in LVec \land X \in {Base}_{W}) \land k \in {Base}_{Scalar (W)}) \to k \cdot_{W} X \in {Base}_{W}$
135	134	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}$
136	1 37 31 126 130 135	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))$
137	81 136	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))$
138		simp3	$⊢ (W \in LVec \land F \in LIndS (W) \land X \in {Base}_{W}) \to X \in {Base}_{W}$
139	1 37 31 82 129 138	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))$
140	139	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))$
141	125 137 140	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))$
142	3 141	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))$
143	119 142	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))$
144	114 143	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\})$
145	144	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\})$
146		oveq2	$⊢ x = X \to k \cdot_{W} x = k \cdot_{W} X$
147		sneq	$⊢ x = X \to \{x\} = \{X\}$
148	147	difeq2d	$⊢ x = X \to (F \cup \{X\}) ∖ \{x\} = (F \cup \{X\}) ∖ \{X\}$
149		difun2	$⊢ (F \cup \{X\}) ∖ \{X\} = F ∖ \{X\}$
150	148 149	eqtrdi	$⊢ x = X \to (F \cup \{X\}) ∖ \{x\} = F ∖ \{X\}$
151	150	fveq2d	$⊢ x = X \to LSpan (W) ((F \cup \{X\}) ∖ \{x\}) = LSpan (W) (F ∖ \{X\})$
152	146 151	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\}))$
153	152	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\}))$
154	153	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\}))$
155	154	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\}))$
156	155	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\}))$
157	145 156	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\})$
158		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\}))$
159	113 157 158	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\})$
160	1 75 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\})))$
161	160	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\})))$
162	8 159 161	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