lsppratlem5

Description: Lemma for lspprat . Combine the two cases and show a contradiction to U C. ( N{ X , Y } ) under the assumptions on x and y . (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\}))$
Assertion	lsppratlem5	$⊢ φ \to N (\{X, Y\}) \subseteq U$

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	4	adantr	$⊢ (φ \land x \in N (\{Y\})) \to W \in LVec$
13	5	adantr	$⊢ (φ \land x \in N (\{Y\})) \to U \in S$
14	6	adantr	$⊢ (φ \land x \in N (\{Y\})) \to X \in V$
15	7	adantr	$⊢ (φ \land x \in N (\{Y\})) \to Y \in V$
16	8	adantr	$⊢ (φ \land x \in N (\{Y\})) \to U \subset N (\{X, Y\})$
17	10	adantr	$⊢ (φ \land x \in N (\{Y\})) \to x \in (U ∖ \{\underset{˙}{0}\})$
18	11	adantr	$⊢ (φ \land x \in N (\{Y\})) \to y \in (U ∖ N (\{x\}))$
19		simpr	$⊢ (φ \land x \in N (\{Y\})) \to x \in N (\{Y\})$
20	1 2 3 12 13 14 15 16 9 17 18 19	lsppratlem3	$⊢ (φ \land x \in N (\{Y\})) \to (X \in N (\{x, y\}) \land Y \in N (\{x, y\}))$
21	4	adantr	$⊢ (φ \land X \in N (\{x, Y\})) \to W \in LVec$
22	5	adantr	$⊢ (φ \land X \in N (\{x, Y\})) \to U \in S$
23	6	adantr	$⊢ (φ \land X \in N (\{x, Y\})) \to X \in V$
24	7	adantr	$⊢ (φ \land X \in N (\{x, Y\})) \to Y \in V$
25	8	adantr	$⊢ (φ \land X \in N (\{x, Y\})) \to U \subset N (\{X, Y\})$
26	10	adantr	$⊢ (φ \land X \in N (\{x, Y\})) \to x \in (U ∖ \{\underset{˙}{0}\})$
27	11	adantr	$⊢ (φ \land X \in N (\{x, Y\})) \to y \in (U ∖ N (\{x\}))$
28		simpr	$⊢ (φ \land X \in N (\{x, Y\})) \to X \in N (\{x, Y\})$
29	1 2 3 21 22 23 24 25 9 26 27 28	lsppratlem4	$⊢ (φ \land X \in N (\{x, Y\})) \to (X \in N (\{x, y\}) \land Y \in N (\{x, y\}))$
30	1 2 3 4 5 6 7 8 9 10 11	lsppratlem1	$⊢ φ \to (x \in N (\{Y\}) \lor X \in N (\{x, Y\}))$
31	20 29 30	mpjaodan	$⊢ φ \to (X \in N (\{x, y\}) \land Y \in N (\{x, y\}))$
32	4	adantr	$⊢ (φ \land (X \in N (\{x, y\}) \land Y \in N (\{x, y\}))) \to W \in LVec$
33	5	adantr	$⊢ (φ \land (X \in N (\{x, y\}) \land Y \in N (\{x, y\}))) \to U \in S$
34	6	adantr	$⊢ (φ \land (X \in N (\{x, y\}) \land Y \in N (\{x, y\}))) \to X \in V$
35	7	adantr	$⊢ (φ \land (X \in N (\{x, y\}) \land Y \in N (\{x, y\}))) \to Y \in V$
36	8	adantr	$⊢ (φ \land (X \in N (\{x, y\}) \land Y \in N (\{x, y\}))) \to U \subset N (\{X, Y\})$
37	10	adantr	$⊢ (φ \land (X \in N (\{x, y\}) \land Y \in N (\{x, y\}))) \to x \in (U ∖ \{\underset{˙}{0}\})$
38	11	adantr	$⊢ (φ \land (X \in N (\{x, y\}) \land Y \in N (\{x, y\}))) \to y \in (U ∖ N (\{x\}))$
39		simprl	$⊢ (φ \land (X \in N (\{x, y\}) \land Y \in N (\{x, y\}))) \to X \in N (\{x, y\})$
40		simprr	$⊢ (φ \land (X \in N (\{x, y\}) \land Y \in N (\{x, y\}))) \to Y \in N (\{x, y\})$
41	1 2 3 32 33 34 35 36 9 37 38 39 40	lsppratlem2	$⊢ (φ \land (X \in N (\{x, y\}) \land Y \in N (\{x, y\}))) \to N (\{X, Y\}) \subseteq U$
42	31 41	mpdan	$⊢ φ \to N (\{X, Y\}) \subseteq U$

Metamath Proof Explorer

Theorem lsppratlem5

Proof