Metamath Proof Explorer


Theorem lspsncv0

Description: The span of a singleton covers the zero subspace, using Definition 3.2.18 of PtakPulmannova p. 68 for "covers".) (Contributed by NM, 12-Aug-2014) (Revised by AV, 13-Jul-2022)

Ref Expression
Hypotheses lspsncv0.v
|- V = ( Base ` W )
lspsncv0.z
|- .0. = ( 0g ` W )
lspsncv0.s
|- S = ( LSubSp ` W )
lspsncv0.n
|- N = ( LSpan ` W )
lspsncv0.w
|- ( ph -> W e. LVec )
lspsncv0.x
|- ( ph -> X e. V )
Assertion lspsncv0
|- ( ph -> -. E. y e. S ( { .0. } C. y /\ y C. ( N ` { X } ) ) )

Proof

Step Hyp Ref Expression
1 lspsncv0.v
 |-  V = ( Base ` W )
2 lspsncv0.z
 |-  .0. = ( 0g ` W )
3 lspsncv0.s
 |-  S = ( LSubSp ` W )
4 lspsncv0.n
 |-  N = ( LSpan ` W )
5 lspsncv0.w
 |-  ( ph -> W e. LVec )
6 lspsncv0.x
 |-  ( ph -> X e. V )
7 df-pss
 |-  ( { .0. } C. y <-> ( { .0. } C_ y /\ { .0. } =/= y ) )
8 simpr
 |-  ( ( { .0. } C_ y /\ { .0. } =/= y ) -> { .0. } =/= y )
9 nesym
 |-  ( { .0. } =/= y <-> -. y = { .0. } )
10 8 9 sylib
 |-  ( ( { .0. } C_ y /\ { .0. } =/= y ) -> -. y = { .0. } )
11 7 10 sylbi
 |-  ( { .0. } C. y -> -. y = { .0. } )
12 5 ad2antrr
 |-  ( ( ( ph /\ y e. S ) /\ y C_ ( N ` { X } ) ) -> W e. LVec )
13 simplr
 |-  ( ( ( ph /\ y e. S ) /\ y C_ ( N ` { X } ) ) -> y e. S )
14 6 ad2antrr
 |-  ( ( ( ph /\ y e. S ) /\ y C_ ( N ` { X } ) ) -> X e. V )
15 simpr
 |-  ( ( ( ph /\ y e. S ) /\ y C_ ( N ` { X } ) ) -> y C_ ( N ` { X } ) )
16 1 2 3 4 lspsnat
 |-  ( ( ( W e. LVec /\ y e. S /\ X e. V ) /\ y C_ ( N ` { X } ) ) -> ( y = ( N ` { X } ) \/ y = { .0. } ) )
17 12 13 14 15 16 syl31anc
 |-  ( ( ( ph /\ y e. S ) /\ y C_ ( N ` { X } ) ) -> ( y = ( N ` { X } ) \/ y = { .0. } ) )
18 17 orcomd
 |-  ( ( ( ph /\ y e. S ) /\ y C_ ( N ` { X } ) ) -> ( y = { .0. } \/ y = ( N ` { X } ) ) )
19 18 ord
 |-  ( ( ( ph /\ y e. S ) /\ y C_ ( N ` { X } ) ) -> ( -. y = { .0. } -> y = ( N ` { X } ) ) )
20 19 ex
 |-  ( ( ph /\ y e. S ) -> ( y C_ ( N ` { X } ) -> ( -. y = { .0. } -> y = ( N ` { X } ) ) ) )
21 20 com23
 |-  ( ( ph /\ y e. S ) -> ( -. y = { .0. } -> ( y C_ ( N ` { X } ) -> y = ( N ` { X } ) ) ) )
22 npss
 |-  ( -. y C. ( N ` { X } ) <-> ( y C_ ( N ` { X } ) -> y = ( N ` { X } ) ) )
23 21 22 syl6ibr
 |-  ( ( ph /\ y e. S ) -> ( -. y = { .0. } -> -. y C. ( N ` { X } ) ) )
24 11 23 syl5
 |-  ( ( ph /\ y e. S ) -> ( { .0. } C. y -> -. y C. ( N ` { X } ) ) )
25 24 ralrimiva
 |-  ( ph -> A. y e. S ( { .0. } C. y -> -. y C. ( N ` { X } ) ) )
26 ralinexa
 |-  ( A. y e. S ( { .0. } C. y -> -. y C. ( N ` { X } ) ) <-> -. E. y e. S ( { .0. } C. y /\ y C. ( N ` { X } ) ) )
27 25 26 sylib
 |-  ( ph -> -. E. y e. S ( { .0. } C. y /\ y C. ( N ` { X } ) ) )