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