Metamath Proof Explorer


Theorem 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 0 ˙ = 0 W
lspdisj2.n N = LSpan W
lspdisj2.w φ W LVec
lspdisj2.x φ X V
lspdisj2.y φ Y V
lspdisj2.q φ N X N Y
Assertion lspdisj2 φ N X N Y = 0 ˙

Proof

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