lspdisj

Description: The span of a vector not in a subspace is disjoint with the subspace. (Contributed by NM, 6-Apr-2015)

	Ref	Expression
Hypotheses	lspdisj.v	$⊢ V = {Base}_{W}$
	lspdisj.o	$⊢ \underset{˙}{0} = 0_{W}$
	lspdisj.n	$⊢ N = LSpan (W)$
	lspdisj.s	$⊢ S = LSubSp (W)$
	lspdisj.w	$⊢ φ \to W \in LVec$
	lspdisj.u	$⊢ φ \to U \in S$
	lspdisj.x	$⊢ φ \to X \in V$
	lspdisj.e	$⊢ φ \to \neg X \in U$
Assertion	lspdisj	$⊢ φ \to N (\{X\}) \cap U = \{\underset{˙}{0}\}$

Proof

Step	Hyp	Ref	Expression
1		lspdisj.v	$⊢ V = {Base}_{W}$
2		lspdisj.o	$⊢ \underset{˙}{0} = 0_{W}$
3		lspdisj.n	$⊢ N = LSpan (W)$
4		lspdisj.s	$⊢ S = LSubSp (W)$
5		lspdisj.w	$⊢ φ \to W \in LVec$
6		lspdisj.u	$⊢ φ \to U \in S$
7		lspdisj.x	$⊢ φ \to X \in V$
8		lspdisj.e	$⊢ φ \to \neg X \in U$
9		lveclmod	$⊢ W \in LVec \to W \in LMod$
10	5 9	syl	$⊢ φ \to W \in LMod$
11		eqid	$⊢ Scalar (W) = Scalar (W)$
12		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
13		eqid	$⊢ \cdot_{W} = \cdot_{W}$
14	11 12 1 13 3	ellspsn	$⊢ (W \in LMod \land X \in V) \to (v \in N (\{X\}) \leftrightarrow \exists k \in {Base}_{Scalar (W)} v = k \cdot_{W} X)$
15	10 7 14	syl2anc	$⊢ φ \to (v \in N (\{X\}) \leftrightarrow \exists k \in {Base}_{Scalar (W)} v = k \cdot_{W} X)$
16	15	biimpa	$⊢ (φ \land v \in N (\{X\})) \to \exists k \in {Base}_{Scalar (W)} v = k \cdot_{W} X$
17	16	adantrr	$⊢ (φ \land (v \in N (\{X\}) \land v \in U)) \to \exists k \in {Base}_{Scalar (W)} v = k \cdot_{W} X$
18		simprr	$⊢ ((φ \land v \in U) \land (k \in {Base}_{Scalar (W)} \land v = k \cdot_{W} X)) \to v = k \cdot_{W} X$
19	8	ad2antrr	$⊢ ((φ \land v \in U) \land (k \in {Base}_{Scalar (W)} \land v = k \cdot_{W} X)) \to \neg X \in U$
20		simplr	$⊢ ((φ \land v \in U) \land (k \in {Base}_{Scalar (W)} \land v = k \cdot_{W} X)) \to v \in U$
21	18 20	eqeltrrd	$⊢ ((φ \land v \in U) \land (k \in {Base}_{Scalar (W)} \land v = k \cdot_{W} X)) \to k \cdot_{W} X \in U$
22		eqid	$⊢ 0_{Scalar (W)} = 0_{Scalar (W)}$
23	5	ad2antrr	$⊢ ((φ \land v \in U) \land (k \in {Base}_{Scalar (W)} \land v = k \cdot_{W} X)) \to W \in LVec$
24	6	ad2antrr	$⊢ ((φ \land v \in U) \land (k \in {Base}_{Scalar (W)} \land v = k \cdot_{W} X)) \to U \in S$
25	7	ad2antrr	$⊢ ((φ \land v \in U) \land (k \in {Base}_{Scalar (W)} \land v = k \cdot_{W} X)) \to X \in V$
26		simprl	$⊢ ((φ \land v \in U) \land (k \in {Base}_{Scalar (W)} \land v = k \cdot_{W} X)) \to k \in {Base}_{Scalar (W)}$
27	1 13 11 12 22 4 23 24 25 26	lssvs0or	$⊢ ((φ \land v \in U) \land (k \in {Base}_{Scalar (W)} \land v = k \cdot_{W} X)) \to (k \cdot_{W} X \in U \leftrightarrow (k = 0_{Scalar (W)} \lor X \in U))$
28	21 27	mpbid	$⊢ ((φ \land v \in U) \land (k \in {Base}_{Scalar (W)} \land v = k \cdot_{W} X)) \to (k = 0_{Scalar (W)} \lor X \in U)$
29	28	orcomd	$⊢ ((φ \land v \in U) \land (k \in {Base}_{Scalar (W)} \land v = k \cdot_{W} X)) \to (X \in U \lor k = 0_{Scalar (W)})$
30	29	ord	$⊢ ((φ \land v \in U) \land (k \in {Base}_{Scalar (W)} \land v = k \cdot_{W} X)) \to (\neg X \in U \to k = 0_{Scalar (W)})$
31	19 30	mpd	$⊢ ((φ \land v \in U) \land (k \in {Base}_{Scalar (W)} \land v = k \cdot_{W} X)) \to k = 0_{Scalar (W)}$
32	31	oveq1d	$⊢ ((φ \land v \in U) \land (k \in {Base}_{Scalar (W)} \land v = k \cdot_{W} X)) \to k \cdot_{W} X = 0_{Scalar (W)} \cdot_{W} X$
33	10	ad2antrr	$⊢ ((φ \land v \in U) \land (k \in {Base}_{Scalar (W)} \land v = k \cdot_{W} X)) \to W \in LMod$
34	1 11 13 22 2	lmod0vs	$⊢ (W \in LMod \land X \in V) \to 0_{Scalar (W)} \cdot_{W} X = \underset{˙}{0}$
35	33 25 34	syl2anc	$⊢ ((φ \land v \in U) \land (k \in {Base}_{Scalar (W)} \land v = k \cdot_{W} X)) \to 0_{Scalar (W)} \cdot_{W} X = \underset{˙}{0}$
36	18 32 35	3eqtrd	$⊢ ((φ \land v \in U) \land (k \in {Base}_{Scalar (W)} \land v = k \cdot_{W} X)) \to v = \underset{˙}{0}$
37	36	exp32	$⊢ (φ \land v \in U) \to (k \in {Base}_{Scalar (W)} \to (v = k \cdot_{W} X \to v = \underset{˙}{0}))$
38	37	adantrl	$⊢ (φ \land (v \in N (\{X\}) \land v \in U)) \to (k \in {Base}_{Scalar (W)} \to (v = k \cdot_{W} X \to v = \underset{˙}{0}))$
39	38	rexlimdv	$⊢ (φ \land (v \in N (\{X\}) \land v \in U)) \to (\exists k \in {Base}_{Scalar (W)} v = k \cdot_{W} X \to v = \underset{˙}{0})$
40	17 39	mpd	$⊢ (φ \land (v \in N (\{X\}) \land v \in U)) \to v = \underset{˙}{0}$
41	40	ex	$⊢ φ \to ((v \in N (\{X\}) \land v \in U) \to v = \underset{˙}{0})$
42		elin	$⊢ v \in (N (\{X\}) \cap U) \leftrightarrow (v \in N (\{X\}) \land v \in U)$
43		velsn	$⊢ v \in \{\underset{˙}{0}\} \leftrightarrow v = \underset{˙}{0}$
44	41 42 43	3imtr4g	$⊢ φ \to (v \in (N (\{X\}) \cap U) \to v \in \{\underset{˙}{0}\})$
45	44	ssrdv	$⊢ φ \to N (\{X\}) \cap U \subseteq \{\underset{˙}{0}\}$
46	1 4 3	lspsncl	$⊢ (W \in LMod \land X \in V) \to N (\{X\}) \in S$
47	10 7 46	syl2anc	$⊢ φ \to N (\{X\}) \in S$
48	2 4	lss0ss	$⊢ (W \in LMod \land N (\{X\}) \in S) \to \{\underset{˙}{0}\} \subseteq N (\{X\})$
49	10 47 48	syl2anc	$⊢ φ \to \{\underset{˙}{0}\} \subseteq N (\{X\})$
50	2 4	lss0ss	$⊢ (W \in LMod \land U \in S) \to \{\underset{˙}{0}\} \subseteq U$
51	10 6 50	syl2anc	$⊢ φ \to \{\underset{˙}{0}\} \subseteq U$
52	49 51	ssind	$⊢ φ \to \{\underset{˙}{0}\} \subseteq N (\{X\}) \cap U$
53	45 52	eqssd	$⊢ φ \to N (\{X\}) \cap U = \{\underset{˙}{0}\}$

Metamath Proof Explorer

Theorem lspdisj

Proof