Metamath Proof Explorer


Theorem lspprat

Description: A proper subspace of the span of a pair of vectors is the span of a singleton (an atom) or the zero subspace (if z is zero). Proof suggested by Mario Carneiro, 28-Aug-2014. (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 φ W LVec
lspprat.u φ U S
lspprat.x φ X V
lspprat.y φ Y V
lspprat.p φ U N X Y
Assertion lspprat φ z V U = N z

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 φ W LVec
5 lspprat.u φ U S
6 lspprat.x φ X V
7 lspprat.y φ Y V
8 lspprat.p φ U N X Y
9 ssdif0 U 0 W U 0 W =
10 lveclmod W LVec W LMod
11 4 10 syl φ W LMod
12 eqid 0 W = 0 W
13 1 12 lmod0vcl W LMod 0 W V
14 11 13 syl φ 0 W V
15 14 adantr φ U 0 W 0 W V
16 simpr φ U 0 W U 0 W
17 12 2 lss0ss W LMod U S 0 W U
18 11 5 17 syl2anc φ 0 W U
19 18 adantr φ U 0 W 0 W U
20 16 19 eqssd φ U 0 W U = 0 W
21 12 3 lspsn0 W LMod N 0 W = 0 W
22 11 21 syl φ N 0 W = 0 W
23 22 adantr φ U 0 W N 0 W = 0 W
24 20 23 eqtr4d φ U 0 W U = N 0 W
25 sneq z = 0 W z = 0 W
26 25 fveq2d z = 0 W N z = N 0 W
27 26 rspceeqv 0 W V U = N 0 W z V U = N z
28 15 24 27 syl2anc φ U 0 W z V U = N z
29 28 ex φ U 0 W z V U = N z
30 9 29 syl5bir φ U 0 W = z V U = N z
31 1 2 lssss U S U V
32 5 31 syl φ U V
33 32 ssdifssd φ U 0 W V
34 33 sseld φ z U 0 W z V
35 1 2 3 4 5 6 7 8 12 lsppratlem6 φ z U 0 W U = N z
36 34 35 jcad φ z U 0 W z V U = N z
37 36 eximdv φ z z U 0 W z z V U = N z
38 n0 U 0 W z z U 0 W
39 df-rex z V U = N z z z V U = N z
40 37 38 39 3imtr4g φ U 0 W z V U = N z
41 30 40 pm2.61dne φ z V U = N z