This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrrdi 
 |-  ( ( 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 } ) ) )