Theorem hdmapnzcl

Description: Nonzero vector closure of map from vectors to functionals with closed kernels. (Contributed by NM, 27-May-2015)

	Ref	Expression
Hypotheses	hdmapnzcl.h	|- H = ( LHyp ` K )
	hdmapnzcl.u	|- U = ( ( DVecH ` K ) ` W )
	hdmapnzcl.v	|- V = ( Base ` U )
	hdmapnzcl.o	|- .0. = ( 0g ` U )
	hdmapnzcl.c	|- C = ( ( LCDual ` K ) ` W )
	hdmapnzcl.q	|- Q = ( 0g ` C )
	hdmapnzcl.d	|- D = ( Base ` C )
	hdmapnzcl.s	|- S = ( ( HDMap ` K ) ` W )
	hdmapnzcl.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	hdmapnzcl.t	|- ( ph -> T e. ( V \ { .0. } ) )
Assertion	hdmapnzcl	|- ( ph -> ( S ` T ) e. ( D \ { Q } ) )

Proof

Step	Hyp	Ref	Expression
1		hdmapnzcl.h	|- H = ( LHyp ` K )
2		hdmapnzcl.u	|- U = ( ( DVecH ` K ) ` W )
3		hdmapnzcl.v	|- V = ( Base ` U )
4		hdmapnzcl.o	|- .0. = ( 0g ` U )
5		hdmapnzcl.c	|- C = ( ( LCDual ` K ) ` W )
6		hdmapnzcl.q	|- Q = ( 0g ` C )
7		hdmapnzcl.d	|- D = ( Base ` C )
8		hdmapnzcl.s	|- S = ( ( HDMap ` K ) ` W )
9		hdmapnzcl.k	|- ( ph -> ( K e. HL /\ W e. H ) )
10		hdmapnzcl.t	|- ( ph -> T e. ( V \ { .0. } ) )
11	10	eldifad	|- ( ph -> T e. V )
12	1 2 3 5 7 8 9 11	hdmapcl	|- ( ph -> ( S ` T ) e. D )
13		eldifsni	|- ( T e. ( V \ { .0. } ) -> T =/= .0. )
14	10 13	syl	|- ( ph -> T =/= .0. )
15	1 2 3 4 5 6 8 9 11	hdmapeq0	|- ( ph -> ( ( S ` T ) = Q <-> T = .0. ) )
16	15	necon3bid	|- ( ph -> ( ( S ` T ) =/= Q <-> T =/= .0. ) )
17	14 16	mpbird	|- ( ph -> ( S ` T ) =/= Q )
18		eldifsn	|- ( ( S ` T ) e. ( D \ { Q } ) <-> ( ( S ` T ) e. D /\ ( S ` T ) =/= Q ) )
19	12 17 18	sylanbrc	|- ( ph -> ( S ` T ) e. ( D \ { Q } ) )