lsppratlem4

Description: Lemma for lspprat . In the second case of lsppratlem1 , y e. ( N{ X , Y } ) C_ ( N{ x , Y } ) and y e/ ( N{ x } ) implies Y e. ( N{ x , y } ) and thus X e. ( N{ x , Y } ) C_ ( N{ x , y } ) as well. (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\}))$
	lsppratlem4.x3	$⊢ φ \to X \in N (\{x, Y\})$
Assertion	lsppratlem4	$⊢ φ \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		lsppratlem4.x3	$⊢ φ \to X \in N (\{x, Y\})$
13		lveclmod	$⊢ W \in LVec \to W \in LMod$
14	4 13	syl	$⊢ φ \to W \in LMod$
15	1 2	lssss	$⊢ U \in S \to U \subseteq V$
16	5 15	syl	$⊢ φ \to U \subseteq V$
17	16	ssdifssd	$⊢ φ \to U ∖ \{\underset{˙}{0}\} \subseteq V$
18	17 10	sseldd	$⊢ φ \to x \in V$
19	16	ssdifssd	$⊢ φ \to U ∖ N (\{x\}) \subseteq V$
20	19 11	sseldd	$⊢ φ \to y \in V$
21	1 2 3 14 18 20	lspprcl	$⊢ φ \to N (\{x, y\}) \in S$
22		df-pr	$⊢ \{x, Y\} = \{x\} \cup \{Y\}$
23		snsspr1	$⊢ \{x\} \subseteq \{x, y\}$
24	18 20	prssd	$⊢ φ \to \{x, y\} \subseteq V$
25	1 3	lspssid	$⊢ (W \in LMod \land \{x, y\} \subseteq V) \to \{x, y\} \subseteq N (\{x, y\})$
26	14 24 25	syl2anc	$⊢ φ \to \{x, y\} \subseteq N (\{x, y\})$
27	23 26	sstrid	$⊢ φ \to \{x\} \subseteq N (\{x, y\})$
28	18	snssd	$⊢ φ \to \{x\} \subseteq V$
29	8	pssssd	$⊢ φ \to U \subseteq N (\{X, Y\})$
30	1 2 3 14 18 7	lspprcl	$⊢ φ \to N (\{x, Y\}) \in S$
31		df-pr	$⊢ \{X, Y\} = \{X\} \cup \{Y\}$
32	12	snssd	$⊢ φ \to \{X\} \subseteq N (\{x, Y\})$
33		snsspr2	$⊢ \{Y\} \subseteq \{x, Y\}$
34	18 7	prssd	$⊢ φ \to \{x, Y\} \subseteq V$
35	1 3	lspssid	$⊢ (W \in LMod \land \{x, Y\} \subseteq V) \to \{x, Y\} \subseteq N (\{x, Y\})$
36	14 34 35	syl2anc	$⊢ φ \to \{x, Y\} \subseteq N (\{x, Y\})$
37	33 36	sstrid	$⊢ φ \to \{Y\} \subseteq N (\{x, Y\})$
38	32 37	unssd	$⊢ φ \to \{X\} \cup \{Y\} \subseteq N (\{x, Y\})$
39	31 38	eqsstrid	$⊢ φ \to \{X, Y\} \subseteq N (\{x, Y\})$
40	2 3	lspssp	$⊢ (W \in LMod \land N (\{x, Y\}) \in S \land \{X, Y\} \subseteq N (\{x, Y\})) \to N (\{X, Y\}) \subseteq N (\{x, Y\})$
41	14 30 39 40	syl3anc	$⊢ φ \to N (\{X, Y\}) \subseteq N (\{x, Y\})$
42	29 41	sstrd	$⊢ φ \to U \subseteq N (\{x, Y\})$
43	22	fveq2i	$⊢ N (\{x, Y\}) = N (\{x\} \cup \{Y\})$
44	42 43	sseqtrdi	$⊢ φ \to U \subseteq N (\{x\} \cup \{Y\})$
45	44	ssdifd	$⊢ φ \to U ∖ N (\{x\}) \subseteq N (\{x\} \cup \{Y\}) ∖ N (\{x\})$
46	45 11	sseldd	$⊢ φ \to y \in (N (\{x\} \cup \{Y\}) ∖ N (\{x\}))$
47	1 2 3	lspsolv	$⊢ (W \in LVec \land (\{x\} \subseteq V \land Y \in V \land y \in (N (\{x\} \cup \{Y\}) ∖ N (\{x\})))) \to Y \in N (\{x\} \cup \{y\})$
48	4 28 7 46 47	syl13anc	$⊢ φ \to Y \in N (\{x\} \cup \{y\})$
49		df-pr	$⊢ \{x, y\} = \{x\} \cup \{y\}$
50	49	fveq2i	$⊢ N (\{x, y\}) = N (\{x\} \cup \{y\})$
51	48 50	eleqtrrdi	$⊢ φ \to Y \in N (\{x, y\})$
52	51	snssd	$⊢ φ \to \{Y\} \subseteq N (\{x, y\})$
53	27 52	unssd	$⊢ φ \to \{x\} \cup \{Y\} \subseteq N (\{x, y\})$
54	22 53	eqsstrid	$⊢ φ \to \{x, Y\} \subseteq N (\{x, y\})$
55	2 3	lspssp	$⊢ (W \in LMod \land N (\{x, y\}) \in S \land \{x, Y\} \subseteq N (\{x, y\})) \to N (\{x, Y\}) \subseteq N (\{x, y\})$
56	14 21 54 55	syl3anc	$⊢ φ \to N (\{x, Y\}) \subseteq N (\{x, y\})$
57	56 12	sseldd	$⊢ φ \to X \in N (\{x, y\})$
58	57 51	jca	$⊢ φ \to (X \in N (\{x, y\}) \land Y \in N (\{x, y\}))$

Metamath Proof Explorer

Theorem lsppratlem4

Proof