lsppratlem6

Description: Lemma for lspprat . Negating the assumption on y , we arrive close to the desired conclusion. (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\})$
	lsppratlem6.o	$⊢ \underset{˙}{0} = 0_{W}$
Assertion	lsppratlem6	$⊢ φ \to (x \in (U ∖ \{\underset{˙}{0}\}) \to U = N (\{x\}))$

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		lsppratlem6.o	$⊢ \underset{˙}{0} = 0_{W}$
10	8	adantr	$⊢ (φ \land x \in (U ∖ \{\underset{˙}{0}\})) \to U \subset N (\{X, Y\})$
11	4	adantr	$⊢ (φ \land (x \in (U ∖ \{\underset{˙}{0}\}) \land y \in (U ∖ N (\{x\})))) \to W \in LVec$
12	5	adantr	$⊢ (φ \land (x \in (U ∖ \{\underset{˙}{0}\}) \land y \in (U ∖ N (\{x\})))) \to U \in S$
13	6	adantr	$⊢ (φ \land (x \in (U ∖ \{\underset{˙}{0}\}) \land y \in (U ∖ N (\{x\})))) \to X \in V$
14	7	adantr	$⊢ (φ \land (x \in (U ∖ \{\underset{˙}{0}\}) \land y \in (U ∖ N (\{x\})))) \to Y \in V$
15	8	adantr	$⊢ (φ \land (x \in (U ∖ \{\underset{˙}{0}\}) \land y \in (U ∖ N (\{x\})))) \to U \subset N (\{X, Y\})$
16		simprl	$⊢ (φ \land (x \in (U ∖ \{\underset{˙}{0}\}) \land y \in (U ∖ N (\{x\})))) \to x \in (U ∖ \{\underset{˙}{0}\})$
17		simprr	$⊢ (φ \land (x \in (U ∖ \{\underset{˙}{0}\}) \land y \in (U ∖ N (\{x\})))) \to y \in (U ∖ N (\{x\}))$
18	1 2 3 11 12 13 14 15 9 16 17	lsppratlem5	$⊢ (φ \land (x \in (U ∖ \{\underset{˙}{0}\}) \land y \in (U ∖ N (\{x\})))) \to N (\{X, Y\}) \subseteq U$
19		ssnpss	$⊢ N (\{X, Y\}) \subseteq U \to \neg U \subset N (\{X, Y\})$
20	18 19	syl	$⊢ (φ \land (x \in (U ∖ \{\underset{˙}{0}\}) \land y \in (U ∖ N (\{x\})))) \to \neg U \subset N (\{X, Y\})$
21	20	expr	$⊢ (φ \land x \in (U ∖ \{\underset{˙}{0}\})) \to (y \in (U ∖ N (\{x\})) \to \neg U \subset N (\{X, Y\}))$
22	10 21	mt2d	$⊢ (φ \land x \in (U ∖ \{\underset{˙}{0}\})) \to \neg y \in (U ∖ N (\{x\}))$
23	22	eq0rdv	$⊢ (φ \land x \in (U ∖ \{\underset{˙}{0}\})) \to U ∖ N (\{x\}) = \emptyset$
24		ssdif0	$⊢ U \subseteq N (\{x\}) \leftrightarrow U ∖ N (\{x\}) = \emptyset$
25	23 24	sylibr	$⊢ (φ \land x \in (U ∖ \{\underset{˙}{0}\})) \to U \subseteq N (\{x\})$
26		lveclmod	$⊢ W \in LVec \to W \in LMod$
27	4 26	syl	$⊢ φ \to W \in LMod$
28	27	adantr	$⊢ (φ \land x \in (U ∖ \{\underset{˙}{0}\})) \to W \in LMod$
29	5	adantr	$⊢ (φ \land x \in (U ∖ \{\underset{˙}{0}\})) \to U \in S$
30		eldifi	$⊢ x \in (U ∖ \{\underset{˙}{0}\}) \to x \in U$
31	30	adantl	$⊢ (φ \land x \in (U ∖ \{\underset{˙}{0}\})) \to x \in U$
32	2 3 28 29 31	lspsnel5a	$⊢ (φ \land x \in (U ∖ \{\underset{˙}{0}\})) \to N (\{x\}) \subseteq U$
33	25 32	eqssd	$⊢ (φ \land x \in (U ∖ \{\underset{˙}{0}\})) \to U = N (\{x\})$
34	33	ex	$⊢ φ \to (x \in (U ∖ \{\underset{˙}{0}\}) \to U = N (\{x\}))$

Metamath Proof Explorer

Theorem lsppratlem6

Proof