lsppratlem3

Description: Lemma for lspprat . In the first case of lsppratlem1 , since x e/ ( N(/) ) , also Y e. ( N{ x } ) , and since y e. ( N{ X , Y } ) C_ ( N{ X , x } ) and y e/ ( N{ x } ) , we have X e. ( N{ x , y } ) as desired. (Contributed by NM, 29-Aug-2014)

	Ref	Expression
Hypotheses	lspprat.v	$⊢ V = {Base}_{W}$
	lspprat.s	$⊢ S = LSubSp (W)$
	lspprat.n	$⊢ N = LSpan (W)$
	lspprat.w	$⊢ φ \to W \in LVec$
	lspprat.u	$⊢ φ \to U \in S$
	lspprat.x	$⊢ φ \to X \in V$
	lspprat.y	$⊢ φ \to Y \in V$
	lspprat.p	$⊢ φ \to U \subset N (\{X, Y\})$
	lsppratlem1.o	$⊢ \underset{˙}{0} = 0_{W}$
	lsppratlem1.x2	$⊢ φ \to x \in (U ∖ \{\underset{˙}{0}\})$
	lsppratlem1.y2	$⊢ φ \to y \in (U ∖ N (\{x\}))$
	lsppratlem3.x3	$⊢ φ \to x \in N (\{Y\})$
Assertion	lsppratlem3	$⊢ φ \to (X \in N (\{x, y\}) \land Y \in N (\{x, y\}))$

Proof

Step	Hyp	Ref	Expression
1		lspprat.v	$⊢ V = {Base}_{W}$
2		lspprat.s	$⊢ S = LSubSp (W)$
3		lspprat.n	$⊢ N = LSpan (W)$
4		lspprat.w	$⊢ φ \to W \in LVec$
5		lspprat.u	$⊢ φ \to U \in S$
6		lspprat.x	$⊢ φ \to X \in V$
7		lspprat.y	$⊢ φ \to Y \in V$
8		lspprat.p	$⊢ φ \to U \subset N (\{X, Y\})$
9		lsppratlem1.o	$⊢ \underset{˙}{0} = 0_{W}$
10		lsppratlem1.x2	$⊢ φ \to x \in (U ∖ \{\underset{˙}{0}\})$
11		lsppratlem1.y2	$⊢ φ \to y \in (U ∖ N (\{x\}))$
12		lsppratlem3.x3	$⊢ φ \to x \in N (\{Y\})$
13		lveclmod	$⊢ W \in LVec \to W \in LMod$
14	4 13	syl	$⊢ φ \to W \in LMod$
15	7	snssd	$⊢ φ \to \{Y\} \subseteq V$
16	1 3	lspssv	$⊢ (W \in LMod \land \{Y\} \subseteq V) \to N (\{Y\}) \subseteq V$
17	14 15 16	syl2anc	$⊢ φ \to N (\{Y\}) \subseteq V$
18	17 12	sseldd	$⊢ φ \to x \in V$
19	18	snssd	$⊢ φ \to \{x\} \subseteq V$
20	8	pssssd	$⊢ φ \to U \subseteq N (\{X, Y\})$
21	6	snssd	$⊢ φ \to \{X\} \subseteq V$
22	19 21	unssd	$⊢ φ \to \{x\} \cup \{X\} \subseteq V$
23	1 2 3	lspcl	$⊢ (W \in LMod \land \{x\} \cup \{X\} \subseteq V) \to N (\{x\} \cup \{X\}) \in S$
24	14 22 23	syl2anc	$⊢ φ \to N (\{x\} \cup \{X\}) \in S$
25		df-pr	$⊢ \{X, Y\} = \{X\} \cup \{Y\}$
26	1 3	lspssid	$⊢ (W \in LMod \land \{x\} \cup \{X\} \subseteq V) \to \{x\} \cup \{X\} \subseteq N (\{x\} \cup \{X\})$
27	14 22 26	syl2anc	$⊢ φ \to \{x\} \cup \{X\} \subseteq N (\{x\} \cup \{X\})$
28	27	unssbd	$⊢ φ \to \{X\} \subseteq N (\{x\} \cup \{X\})$
29		ssun1	$⊢ \{x\} \subseteq \{x\} \cup \{X\}$
30	29	a1i	$⊢ φ \to \{x\} \subseteq \{x\} \cup \{X\}$
31	1 3	lspss	$⊢ (W \in LMod \land \{x\} \cup \{X\} \subseteq V \land \{x\} \subseteq \{x\} \cup \{X\}) \to N (\{x\}) \subseteq N (\{x\} \cup \{X\})$
32	14 22 30 31	syl3anc	$⊢ φ \to N (\{x\}) \subseteq N (\{x\} \cup \{X\})$
33		0ss	$⊢ \emptyset \subseteq V$
34	33	a1i	$⊢ φ \to \emptyset \subseteq V$
35		uncom	$⊢ \emptyset \cup \{Y\} = \{Y\} \cup \emptyset$
36		un0	$⊢ \{Y\} \cup \emptyset = \{Y\}$
37	35 36	eqtri	$⊢ \emptyset \cup \{Y\} = \{Y\}$
38	37	fveq2i	$⊢ N (\emptyset \cup \{Y\}) = N (\{Y\})$
39	12 38	eleqtrrdi	$⊢ φ \to x \in N (\emptyset \cup \{Y\})$
40	10	eldifbd	$⊢ φ \to \neg x \in \{\underset{˙}{0}\}$
41	9 3	lsp0	$⊢ W \in LMod \to N (\emptyset) = \{\underset{˙}{0}\}$
42	14 41	syl	$⊢ φ \to N (\emptyset) = \{\underset{˙}{0}\}$
43	40 42	neleqtrrd	$⊢ φ \to \neg x \in N (\emptyset)$
44	39 43	eldifd	$⊢ φ \to x \in (N (\emptyset \cup \{Y\}) ∖ N (\emptyset))$
45	1 2 3	lspsolv	$⊢ (W \in LVec \land (\emptyset \subseteq V \land Y \in V \land x \in (N (\emptyset \cup \{Y\}) ∖ N (\emptyset)))) \to Y \in N (\emptyset \cup \{x\})$
46	4 34 7 44 45	syl13anc	$⊢ φ \to Y \in N (\emptyset \cup \{x\})$
47		uncom	$⊢ \emptyset \cup \{x\} = \{x\} \cup \emptyset$
48		un0	$⊢ \{x\} \cup \emptyset = \{x\}$
49	47 48	eqtri	$⊢ \emptyset \cup \{x\} = \{x\}$
50	49	fveq2i	$⊢ N (\emptyset \cup \{x\}) = N (\{x\})$
51	46 50	eleqtrdi	$⊢ φ \to Y \in N (\{x\})$
52	32 51	sseldd	$⊢ φ \to Y \in N (\{x\} \cup \{X\})$
53	52	snssd	$⊢ φ \to \{Y\} \subseteq N (\{x\} \cup \{X\})$
54	28 53	unssd	$⊢ φ \to \{X\} \cup \{Y\} \subseteq N (\{x\} \cup \{X\})$
55	25 54	eqsstrid	$⊢ φ \to \{X, Y\} \subseteq N (\{x\} \cup \{X\})$
56	2 3	lspssp	$⊢ (W \in LMod \land N (\{x\} \cup \{X\}) \in S \land \{X, Y\} \subseteq N (\{x\} \cup \{X\})) \to N (\{X, Y\}) \subseteq N (\{x\} \cup \{X\})$
57	14 24 55 56	syl3anc	$⊢ φ \to N (\{X, Y\}) \subseteq N (\{x\} \cup \{X\})$
58	20 57	sstrd	$⊢ φ \to U \subseteq N (\{x\} \cup \{X\})$
59	58	ssdifd	$⊢ φ \to U ∖ N (\{x\}) \subseteq N (\{x\} \cup \{X\}) ∖ N (\{x\})$
60	59 11	sseldd	$⊢ φ \to y \in (N (\{x\} \cup \{X\}) ∖ N (\{x\}))$
61	1 2 3	lspsolv	$⊢ (W \in LVec \land (\{x\} \subseteq V \land X \in V \land y \in (N (\{x\} \cup \{X\}) ∖ N (\{x\})))) \to X \in N (\{x\} \cup \{y\})$
62	4 19 6 60 61	syl13anc	$⊢ φ \to X \in N (\{x\} \cup \{y\})$
63		df-pr	$⊢ \{x, y\} = \{x\} \cup \{y\}$
64	63	fveq2i	$⊢ N (\{x, y\}) = N (\{x\} \cup \{y\})$
65	62 64	eleqtrrdi	$⊢ φ \to X \in N (\{x, y\})$
66	1 2	lssss	$⊢ U \in S \to U \subseteq V$
67	5 66	syl	$⊢ φ \to U \subseteq V$
68	67	ssdifssd	$⊢ φ \to U ∖ N (\{x\}) \subseteq V$
69	68 11	sseldd	$⊢ φ \to y \in V$
70	18 69	prssd	$⊢ φ \to \{x, y\} \subseteq V$
71		snsspr1	$⊢ \{x\} \subseteq \{x, y\}$
72	71	a1i	$⊢ φ \to \{x\} \subseteq \{x, y\}$
73	1 3	lspss	$⊢ (W \in LMod \land \{x, y\} \subseteq V \land \{x\} \subseteq \{x, y\}) \to N (\{x\}) \subseteq N (\{x, y\})$
74	14 70 72 73	syl3anc	$⊢ φ \to N (\{x\}) \subseteq N (\{x, y\})$
75	74 51	sseldd	$⊢ φ \to Y \in N (\{x, y\})$
76	65 75	jca	$⊢ φ \to (X \in N (\{x, y\}) \land Y \in N (\{x, y\}))$

Metamath Proof Explorer

Theorem lsppratlem3

Proof