lbsextlem2

Description: Lemma for lbsext . Since A is a chain (actually, we only need it to be closed under binary union), the union T of the spans of each individual element of A is a subspace, and it contains all of U. A (except for our target vector x - we are trying to make x a linear combination of all the other vectors in some set from A ). (Contributed by Mario Carneiro, 25-Jun-2014)

	Ref	Expression
Hypotheses	lbsext.v	$⊢ V = {Base}_{W}$
	lbsext.j	$⊢ J = LBasis (W)$
	lbsext.n	$⊢ N = LSpan (W)$
	lbsext.w	$⊢ φ \to W \in LVec$
	lbsext.c	$⊢ φ \to C \subseteq V$
	lbsext.x	$⊢ φ \to \forall x \in C \neg x \in N (C ∖ \{x\})$
	lbsext.s	$⊢ S = \{z \in 𝒫 V \| (C \subseteq z \land \forall x \in z \neg x \in N (z ∖ \{x\}))\}$
	lbsext.p	$⊢ P = LSubSp (W)$
	lbsext.a	$⊢ φ \to A \subseteq S$
	lbsext.z	$⊢ φ \to A \neq \emptyset$
	lbsext.r	$⊢ φ \to [\subset] Or A$
	lbsext.t	$⊢ T = ⋃_{u \in A} N (u ∖ \{x\})$
Assertion	lbsextlem2	$⊢ φ \to (T \in P \land ⋃ A ∖ \{x\} \subseteq T)$

Proof

Step	Hyp	Ref	Expression
1		lbsext.v	$⊢ V = {Base}_{W}$
2		lbsext.j	$⊢ J = LBasis (W)$
3		lbsext.n	$⊢ N = LSpan (W)$
4		lbsext.w	$⊢ φ \to W \in LVec$
5		lbsext.c	$⊢ φ \to C \subseteq V$
6		lbsext.x	$⊢ φ \to \forall x \in C \neg x \in N (C ∖ \{x\})$
7		lbsext.s	$⊢ S = \{z \in 𝒫 V \| (C \subseteq z \land \forall x \in z \neg x \in N (z ∖ \{x\}))\}$
8		lbsext.p	$⊢ P = LSubSp (W)$
9		lbsext.a	$⊢ φ \to A \subseteq S$
10		lbsext.z	$⊢ φ \to A \neq \emptyset$
11		lbsext.r	$⊢ φ \to [\subset] Or A$
12		lbsext.t	$⊢ T = ⋃_{u \in A} N (u ∖ \{x\})$
13		eqidd	$⊢ φ \to Scalar (W) = Scalar (W)$
14		eqidd	$⊢ φ \to {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
15	1	a1i	$⊢ φ \to V = {Base}_{W}$
16		eqidd	$⊢ φ \to +_{W} = +_{W}$
17		eqidd	$⊢ φ \to \cdot_{W} = \cdot_{W}$
18	8	a1i	$⊢ φ \to P = LSubSp (W)$
19		lveclmod	$⊢ W \in LVec \to W \in LMod$
20	4 19	syl	$⊢ φ \to W \in LMod$
21	7	ssrab3	$⊢ S \subseteq 𝒫 V$
22	9 21	sstrdi	$⊢ φ \to A \subseteq 𝒫 V$
23	22	sselda	$⊢ (φ \land u \in A) \to u \in 𝒫 V$
24	23	elpwid	$⊢ (φ \land u \in A) \to u \subseteq V$
25	24	ssdifssd	$⊢ (φ \land u \in A) \to u ∖ \{x\} \subseteq V$
26	1 3	lspssv	$⊢ (W \in LMod \land u ∖ \{x\} \subseteq V) \to N (u ∖ \{x\}) \subseteq V$
27	20 25 26	syl2an2r	$⊢ (φ \land u \in A) \to N (u ∖ \{x\}) \subseteq V$
28	27	ralrimiva	$⊢ φ \to \forall u \in A N (u ∖ \{x\}) \subseteq V$
29		iunss	$⊢ ⋃_{u \in A} N (u ∖ \{x\}) \subseteq V \leftrightarrow \forall u \in A N (u ∖ \{x\}) \subseteq V$
30	28 29	sylibr	$⊢ φ \to ⋃_{u \in A} N (u ∖ \{x\}) \subseteq V$
31	12 30	eqsstrid	$⊢ φ \to T \subseteq V$
32	12	a1i	$⊢ φ \to T = ⋃_{u \in A} N (u ∖ \{x\})$
33	1 8 3	lspcl	$⊢ (W \in LMod \land u ∖ \{x\} \subseteq V) \to N (u ∖ \{x\}) \in P$
34	20 25 33	syl2an2r	$⊢ (φ \land u \in A) \to N (u ∖ \{x\}) \in P$
35	8	lssn0	$⊢ N (u ∖ \{x\}) \in P \to N (u ∖ \{x\}) \neq \emptyset$
36	34 35	syl	$⊢ (φ \land u \in A) \to N (u ∖ \{x\}) \neq \emptyset$
37	36	ralrimiva	$⊢ φ \to \forall u \in A N (u ∖ \{x\}) \neq \emptyset$
38		r19.2z	$⊢ (A \neq \emptyset \land \forall u \in A N (u ∖ \{x\}) \neq \emptyset) \to \exists u \in A N (u ∖ \{x\}) \neq \emptyset$
39	10 37 38	syl2anc	$⊢ φ \to \exists u \in A N (u ∖ \{x\}) \neq \emptyset$
40		iunn0	$⊢ \exists u \in A N (u ∖ \{x\}) \neq \emptyset \leftrightarrow ⋃_{u \in A} N (u ∖ \{x\}) \neq \emptyset$
41	39 40	sylib	$⊢ φ \to ⋃_{u \in A} N (u ∖ \{x\}) \neq \emptyset$
42	32 41	eqnetrd	$⊢ φ \to T \neq \emptyset$
43	12	eleq2i	$⊢ v \in T \leftrightarrow v \in ⋃_{u \in A} N (u ∖ \{x\})$
44		eliun	$⊢ v \in ⋃_{u \in A} N (u ∖ \{x\}) \leftrightarrow \exists u \in A v \in N (u ∖ \{x\})$
45		difeq1	$⊢ u = m \to u ∖ \{x\} = m ∖ \{x\}$
46	45	fveq2d	$⊢ u = m \to N (u ∖ \{x\}) = N (m ∖ \{x\})$
47	46	eleq2d	$⊢ u = m \to (v \in N (u ∖ \{x\}) \leftrightarrow v \in N (m ∖ \{x\}))$
48	47	cbvrexvw	$⊢ \exists u \in A v \in N (u ∖ \{x\}) \leftrightarrow \exists m \in A v \in N (m ∖ \{x\})$
49	43 44 48	3bitri	$⊢ v \in T \leftrightarrow \exists m \in A v \in N (m ∖ \{x\})$
50	12	eleq2i	$⊢ w \in T \leftrightarrow w \in ⋃_{u \in A} N (u ∖ \{x\})$
51		eliun	$⊢ w \in ⋃_{u \in A} N (u ∖ \{x\}) \leftrightarrow \exists u \in A w \in N (u ∖ \{x\})$
52		difeq1	$⊢ u = n \to u ∖ \{x\} = n ∖ \{x\}$
53	52	fveq2d	$⊢ u = n \to N (u ∖ \{x\}) = N (n ∖ \{x\})$
54	53	eleq2d	$⊢ u = n \to (w \in N (u ∖ \{x\}) \leftrightarrow w \in N (n ∖ \{x\}))$
55	54	cbvrexvw	$⊢ \exists u \in A w \in N (u ∖ \{x\}) \leftrightarrow \exists n \in A w \in N (n ∖ \{x\})$
56	50 51 55	3bitri	$⊢ w \in T \leftrightarrow \exists n \in A w \in N (n ∖ \{x\})$
57	49 56	anbi12i	$⊢ (v \in T \land w \in T) \leftrightarrow (\exists m \in A v \in N (m ∖ \{x\}) \land \exists n \in A w \in N (n ∖ \{x\}))$
58		reeanv	$⊢ \exists m \in A \exists n \in A (v \in N (m ∖ \{x\}) \land w \in N (n ∖ \{x\})) \leftrightarrow (\exists m \in A v \in N (m ∖ \{x\}) \land \exists n \in A w \in N (n ∖ \{x\}))$
59	57 58	bitr4i	$⊢ (v \in T \land w \in T) \leftrightarrow \exists m \in A \exists n \in A (v \in N (m ∖ \{x\}) \land w \in N (n ∖ \{x\}))$
60		simp1l	$⊢ ((φ \land r \in {Base}_{Scalar (W)}) \land (m \in A \land n \in A) \land (v \in N (m ∖ \{x\}) \land w \in N (n ∖ \{x\}))) \to φ$
61	60 11	syl	$⊢ ((φ \land r \in {Base}_{Scalar (W)}) \land (m \in A \land n \in A) \land (v \in N (m ∖ \{x\}) \land w \in N (n ∖ \{x\}))) \to [\subset] Or A$
62		simp2	$⊢ ((φ \land r \in {Base}_{Scalar (W)}) \land (m \in A \land n \in A) \land (v \in N (m ∖ \{x\}) \land w \in N (n ∖ \{x\}))) \to (m \in A \land n \in A)$
63		sorpssun	$⊢ ([\subset] Or A \land (m \in A \land n \in A)) \to m \cup n \in A$
64	61 62 63	syl2anc	$⊢ ((φ \land r \in {Base}_{Scalar (W)}) \land (m \in A \land n \in A) \land (v \in N (m ∖ \{x\}) \land w \in N (n ∖ \{x\}))) \to m \cup n \in A$
65	60 20	syl	$⊢ ((φ \land r \in {Base}_{Scalar (W)}) \land (m \in A \land n \in A) \land (v \in N (m ∖ \{x\}) \land w \in N (n ∖ \{x\}))) \to W \in LMod$
66		elssuni	$⊢ m \cup n \in A \to m \cup n \subseteq ⋃ A$
67	64 66	syl	$⊢ ((φ \land r \in {Base}_{Scalar (W)}) \land (m \in A \land n \in A) \land (v \in N (m ∖ \{x\}) \land w \in N (n ∖ \{x\}))) \to m \cup n \subseteq ⋃ A$
68		sspwuni	$⊢ A \subseteq 𝒫 V \leftrightarrow ⋃ A \subseteq V$
69	22 68	sylib	$⊢ φ \to ⋃ A \subseteq V$
70	60 69	syl	$⊢ ((φ \land r \in {Base}_{Scalar (W)}) \land (m \in A \land n \in A) \land (v \in N (m ∖ \{x\}) \land w \in N (n ∖ \{x\}))) \to ⋃ A \subseteq V$
71	67 70	sstrd	$⊢ ((φ \land r \in {Base}_{Scalar (W)}) \land (m \in A \land n \in A) \land (v \in N (m ∖ \{x\}) \land w \in N (n ∖ \{x\}))) \to m \cup n \subseteq V$
72	71	ssdifssd	$⊢ ((φ \land r \in {Base}_{Scalar (W)}) \land (m \in A \land n \in A) \land (v \in N (m ∖ \{x\}) \land w \in N (n ∖ \{x\}))) \to (m \cup n) ∖ \{x\} \subseteq V$
73	1 8 3	lspcl	$⊢ (W \in LMod \land (m \cup n) ∖ \{x\} \subseteq V) \to N ((m \cup n) ∖ \{x\}) \in P$
74	65 72 73	syl2anc	$⊢ ((φ \land r \in {Base}_{Scalar (W)}) \land (m \in A \land n \in A) \land (v \in N (m ∖ \{x\}) \land w \in N (n ∖ \{x\}))) \to N ((m \cup n) ∖ \{x\}) \in P$
75		simp1r	$⊢ ((φ \land r \in {Base}_{Scalar (W)}) \land (m \in A \land n \in A) \land (v \in N (m ∖ \{x\}) \land w \in N (n ∖ \{x\}))) \to r \in {Base}_{Scalar (W)}$
76		ssun1	$⊢ m \subseteq m \cup n$
77		ssdif	$⊢ m \subseteq m \cup n \to m ∖ \{x\} \subseteq (m \cup n) ∖ \{x\}$
78	76 77	mp1i	$⊢ ((φ \land r \in {Base}_{Scalar (W)}) \land (m \in A \land n \in A) \land (v \in N (m ∖ \{x\}) \land w \in N (n ∖ \{x\}))) \to m ∖ \{x\} \subseteq (m \cup n) ∖ \{x\}$
79	1 3	lspss	$⊢ (W \in LMod \land (m \cup n) ∖ \{x\} \subseteq V \land m ∖ \{x\} \subseteq (m \cup n) ∖ \{x\}) \to N (m ∖ \{x\}) \subseteq N ((m \cup n) ∖ \{x\})$
80	65 72 78 79	syl3anc	$⊢ ((φ \land r \in {Base}_{Scalar (W)}) \land (m \in A \land n \in A) \land (v \in N (m ∖ \{x\}) \land w \in N (n ∖ \{x\}))) \to N (m ∖ \{x\}) \subseteq N ((m \cup n) ∖ \{x\})$
81		simp3l	$⊢ ((φ \land r \in {Base}_{Scalar (W)}) \land (m \in A \land n \in A) \land (v \in N (m ∖ \{x\}) \land w \in N (n ∖ \{x\}))) \to v \in N (m ∖ \{x\})$
82	80 81	sseldd	$⊢ ((φ \land r \in {Base}_{Scalar (W)}) \land (m \in A \land n \in A) \land (v \in N (m ∖ \{x\}) \land w \in N (n ∖ \{x\}))) \to v \in N ((m \cup n) ∖ \{x\})$
83		ssun2	$⊢ n \subseteq m \cup n$
84		ssdif	$⊢ n \subseteq m \cup n \to n ∖ \{x\} \subseteq (m \cup n) ∖ \{x\}$
85	83 84	mp1i	$⊢ ((φ \land r \in {Base}_{Scalar (W)}) \land (m \in A \land n \in A) \land (v \in N (m ∖ \{x\}) \land w \in N (n ∖ \{x\}))) \to n ∖ \{x\} \subseteq (m \cup n) ∖ \{x\}$
86	1 3	lspss	$⊢ (W \in LMod \land (m \cup n) ∖ \{x\} \subseteq V \land n ∖ \{x\} \subseteq (m \cup n) ∖ \{x\}) \to N (n ∖ \{x\}) \subseteq N ((m \cup n) ∖ \{x\})$
87	65 72 85 86	syl3anc	$⊢ ((φ \land r \in {Base}_{Scalar (W)}) \land (m \in A \land n \in A) \land (v \in N (m ∖ \{x\}) \land w \in N (n ∖ \{x\}))) \to N (n ∖ \{x\}) \subseteq N ((m \cup n) ∖ \{x\})$
88		simp3r	$⊢ ((φ \land r \in {Base}_{Scalar (W)}) \land (m \in A \land n \in A) \land (v \in N (m ∖ \{x\}) \land w \in N (n ∖ \{x\}))) \to w \in N (n ∖ \{x\})$
89	87 88	sseldd	$⊢ ((φ \land r \in {Base}_{Scalar (W)}) \land (m \in A \land n \in A) \land (v \in N (m ∖ \{x\}) \land w \in N (n ∖ \{x\}))) \to w \in N ((m \cup n) ∖ \{x\})$
90		eqid	$⊢ Scalar (W) = Scalar (W)$
91		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
92		eqid	$⊢ +_{W} = +_{W}$
93		eqid	$⊢ \cdot_{W} = \cdot_{W}$
94	90 91 92 93 8	lsscl	$⊢ (N ((m \cup n) ∖ \{x\}) \in P \land (r \in {Base}_{Scalar (W)} \land v \in N ((m \cup n) ∖ \{x\}) \land w \in N ((m \cup n) ∖ \{x\}))) \to (r \cdot_{W} v) +_{W} w \in N ((m \cup n) ∖ \{x\})$
95	74 75 82 89 94	syl13anc	$⊢ ((φ \land r \in {Base}_{Scalar (W)}) \land (m \in A \land n \in A) \land (v \in N (m ∖ \{x\}) \land w \in N (n ∖ \{x\}))) \to (r \cdot_{W} v) +_{W} w \in N ((m \cup n) ∖ \{x\})$
96		difeq1	$⊢ u = m \cup n \to u ∖ \{x\} = (m \cup n) ∖ \{x\}$
97	96	fveq2d	$⊢ u = m \cup n \to N (u ∖ \{x\}) = N ((m \cup n) ∖ \{x\})$
98	97	eliuni	$⊢ (m \cup n \in A \land (r \cdot_{W} v) +_{W} w \in N ((m \cup n) ∖ \{x\})) \to (r \cdot_{W} v) +_{W} w \in ⋃_{u \in A} N (u ∖ \{x\})$
99	64 95 98	syl2anc	$⊢ ((φ \land r \in {Base}_{Scalar (W)}) \land (m \in A \land n \in A) \land (v \in N (m ∖ \{x\}) \land w \in N (n ∖ \{x\}))) \to (r \cdot_{W} v) +_{W} w \in ⋃_{u \in A} N (u ∖ \{x\})$
100	99 12	eleqtrrdi	$⊢ ((φ \land r \in {Base}_{Scalar (W)}) \land (m \in A \land n \in A) \land (v \in N (m ∖ \{x\}) \land w \in N (n ∖ \{x\}))) \to (r \cdot_{W} v) +_{W} w \in T$
101	100	3expia	$⊢ ((φ \land r \in {Base}_{Scalar (W)}) \land (m \in A \land n \in A)) \to ((v \in N (m ∖ \{x\}) \land w \in N (n ∖ \{x\})) \to (r \cdot_{W} v) +_{W} w \in T)$
102	101	rexlimdvva	$⊢ (φ \land r \in {Base}_{Scalar (W)}) \to (\exists m \in A \exists n \in A (v \in N (m ∖ \{x\}) \land w \in N (n ∖ \{x\})) \to (r \cdot_{W} v) +_{W} w \in T)$
103	59 102	syl5bi	$⊢ (φ \land r \in {Base}_{Scalar (W)}) \to ((v \in T \land w \in T) \to (r \cdot_{W} v) +_{W} w \in T)$
104	103	exp4b	$⊢ φ \to (r \in {Base}_{Scalar (W)} \to (v \in T \to (w \in T \to (r \cdot_{W} v) +_{W} w \in T)))$
105	104	3imp2	$⊢ (φ \land (r \in {Base}_{Scalar (W)} \land v \in T \land w \in T)) \to (r \cdot_{W} v) +_{W} w \in T$
106	13 14 15 16 17 18 31 42 105	islssd	$⊢ φ \to T \in P$
107		eldifi	$⊢ y \in (⋃ A ∖ \{x\}) \to y \in ⋃ A$
108	107	adantl	$⊢ (φ \land y \in (⋃ A ∖ \{x\})) \to y \in ⋃ A$
109		eldifn	$⊢ y \in (⋃ A ∖ \{x\}) \to \neg y \in \{x\}$
110	109	ad2antlr	$⊢ ((φ \land y \in (⋃ A ∖ \{x\})) \land u \in A) \to \neg y \in \{x\}$
111		eldif	$⊢ y \in (u ∖ \{x\}) \leftrightarrow (y \in u \land \neg y \in \{x\})$
112	1 3	lspssid	$⊢ (W \in LMod \land u ∖ \{x\} \subseteq V) \to u ∖ \{x\} \subseteq N (u ∖ \{x\})$
113	20 25 112	syl2an2r	$⊢ (φ \land u \in A) \to u ∖ \{x\} \subseteq N (u ∖ \{x\})$
114	113	adantlr	$⊢ ((φ \land y \in (⋃ A ∖ \{x\})) \land u \in A) \to u ∖ \{x\} \subseteq N (u ∖ \{x\})$
115	114	sseld	$⊢ ((φ \land y \in (⋃ A ∖ \{x\})) \land u \in A) \to (y \in (u ∖ \{x\}) \to y \in N (u ∖ \{x\}))$
116	111 115	syl5bir	$⊢ ((φ \land y \in (⋃ A ∖ \{x\})) \land u \in A) \to ((y \in u \land \neg y \in \{x\}) \to y \in N (u ∖ \{x\}))$
117	110 116	mpan2d	$⊢ ((φ \land y \in (⋃ A ∖ \{x\})) \land u \in A) \to (y \in u \to y \in N (u ∖ \{x\}))$
118	117	reximdva	$⊢ (φ \land y \in (⋃ A ∖ \{x\})) \to (\exists u \in A y \in u \to \exists u \in A y \in N (u ∖ \{x\}))$
119		eluni2	$⊢ y \in ⋃ A \leftrightarrow \exists u \in A y \in u$
120		eliun	$⊢ y \in ⋃_{u \in A} N (u ∖ \{x\}) \leftrightarrow \exists u \in A y \in N (u ∖ \{x\})$
121	118 119 120	3imtr4g	$⊢ (φ \land y \in (⋃ A ∖ \{x\})) \to (y \in ⋃ A \to y \in ⋃_{u \in A} N (u ∖ \{x\}))$
122	108 121	mpd	$⊢ (φ \land y \in (⋃ A ∖ \{x\})) \to y \in ⋃_{u \in A} N (u ∖ \{x\})$
123	122	ex	$⊢ φ \to (y \in (⋃ A ∖ \{x\}) \to y \in ⋃_{u \in A} N (u ∖ \{x\}))$
124	123	ssrdv	$⊢ φ \to ⋃ A ∖ \{x\} \subseteq ⋃_{u \in A} N (u ∖ \{x\})$
125	124 12	sseqtrrdi	$⊢ φ \to ⋃ A ∖ \{x\} \subseteq T$
126	106 125	jca	$⊢ φ \to (T \in P \land ⋃ A ∖ \{x\} \subseteq T)$

Metamath Proof Explorer

Theorem lbsextlem2

Proof