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