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