lspdisj2

Description: Unequal spans are disjoint (share only the zero vector). (Contributed by NM, 22-Mar-2015)

	Ref	Expression
Hypotheses	lspdisj2.v	$⊢ V = {Base}_{W}$
	lspdisj2.o	$⊢ \underset{˙}{0} = 0_{W}$
	lspdisj2.n	$⊢ N = LSpan (W)$
	lspdisj2.w	$⊢ φ \to W \in LVec$
	lspdisj2.x	$⊢ φ \to X \in V$
	lspdisj2.y	$⊢ φ \to Y \in V$
	lspdisj2.q	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
Assertion	lspdisj2	$⊢ φ \to N (\{X\}) \cap N (\{Y\}) = \{\underset{˙}{0}\}$

Proof

Step	Hyp	Ref	Expression
1		lspdisj2.v	$⊢ V = {Base}_{W}$
2		lspdisj2.o	$⊢ \underset{˙}{0} = 0_{W}$
3		lspdisj2.n	$⊢ N = LSpan (W)$
4		lspdisj2.w	$⊢ φ \to W \in LVec$
5		lspdisj2.x	$⊢ φ \to X \in V$
6		lspdisj2.y	$⊢ φ \to Y \in V$
7		lspdisj2.q	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
8		sneq	$⊢ X = \underset{˙}{0} \to \{X\} = \{\underset{˙}{0}\}$
9	8	fveq2d	$⊢ X = \underset{˙}{0} \to N (\{X\}) = N (\{\underset{˙}{0}\})$
10		lveclmod	$⊢ W \in LVec \to W \in LMod$
11	4 10	syl	$⊢ φ \to W \in LMod$
12	2 3	lspsn0	$⊢ W \in LMod \to N (\{\underset{˙}{0}\}) = \{\underset{˙}{0}\}$
13	11 12	syl	$⊢ φ \to N (\{\underset{˙}{0}\}) = \{\underset{˙}{0}\}$
14	9 13	sylan9eqr	$⊢ (φ \land X = \underset{˙}{0}) \to N (\{X\}) = \{\underset{˙}{0}\}$
15	14	ineq1d	$⊢ (φ \land X = \underset{˙}{0}) \to N (\{X\}) \cap N (\{Y\}) = \{\underset{˙}{0}\} \cap N (\{Y\})$
16		eqid	$⊢ LSubSp (W) = LSubSp (W)$
17	1 16 3	lspsncl	$⊢ (W \in LMod \land Y \in V) \to N (\{Y\}) \in LSubSp (W)$
18	11 6 17	syl2anc	$⊢ φ \to N (\{Y\}) \in LSubSp (W)$
19	2 16	lss0ss	$⊢ (W \in LMod \land N (\{Y\}) \in LSubSp (W)) \to \{\underset{˙}{0}\} \subseteq N (\{Y\})$
20	11 18 19	syl2anc	$⊢ φ \to \{\underset{˙}{0}\} \subseteq N (\{Y\})$
21		df-ss	$⊢ \{\underset{˙}{0}\} \subseteq N (\{Y\}) \leftrightarrow \{\underset{˙}{0}\} \cap N (\{Y\}) = \{\underset{˙}{0}\}$
22	20 21	sylib	$⊢ φ \to \{\underset{˙}{0}\} \cap N (\{Y\}) = \{\underset{˙}{0}\}$
23	22	adantr	$⊢ (φ \land X = \underset{˙}{0}) \to \{\underset{˙}{0}\} \cap N (\{Y\}) = \{\underset{˙}{0}\}$
24	15 23	eqtrd	$⊢ (φ \land X = \underset{˙}{0}) \to N (\{X\}) \cap N (\{Y\}) = \{\underset{˙}{0}\}$
25	4	adantr	$⊢ (φ \land X \neq \underset{˙}{0}) \to W \in LVec$
26	18	adantr	$⊢ (φ \land X \neq \underset{˙}{0}) \to N (\{Y\}) \in LSubSp (W)$
27	5	adantr	$⊢ (φ \land X \neq \underset{˙}{0}) \to X \in V$
28	7	adantr	$⊢ (φ \land X \neq \underset{˙}{0}) \to N (\{X\}) \neq N (\{Y\})$
29	25	adantr	$⊢ ((φ \land X \neq \underset{˙}{0}) \land X \in N (\{Y\})) \to W \in LVec$
30	6	adantr	$⊢ (φ \land X \neq \underset{˙}{0}) \to Y \in V$
31	30	adantr	$⊢ ((φ \land X \neq \underset{˙}{0}) \land X \in N (\{Y\})) \to Y \in V$
32		simpr	$⊢ ((φ \land X \neq \underset{˙}{0}) \land X \in N (\{Y\})) \to X \in N (\{Y\})$
33		simplr	$⊢ ((φ \land X \neq \underset{˙}{0}) \land X \in N (\{Y\})) \to X \neq \underset{˙}{0}$
34	1 2 3 29 31 32 33	lspsneleq	$⊢ ((φ \land X \neq \underset{˙}{0}) \land X \in N (\{Y\})) \to N (\{X\}) = N (\{Y\})$
35	34	ex	$⊢ (φ \land X \neq \underset{˙}{0}) \to (X \in N (\{Y\}) \to N (\{X\}) = N (\{Y\}))$
36	35	necon3ad	$⊢ (φ \land X \neq \underset{˙}{0}) \to (N (\{X\}) \neq N (\{Y\}) \to \neg X \in N (\{Y\}))$
37	28 36	mpd	$⊢ (φ \land X \neq \underset{˙}{0}) \to \neg X \in N (\{Y\})$
38	1 2 3 16 25 26 27 37	lspdisj	$⊢ (φ \land X \neq \underset{˙}{0}) \to N (\{X\}) \cap N (\{Y\}) = \{\underset{˙}{0}\}$
39	24 38	pm2.61dane	$⊢ φ \to N (\{X\}) \cap N (\{Y\}) = \{\underset{˙}{0}\}$

Metamath Proof Explorer

Theorem lspdisj2

Proof