Theorem hdmaprnlem15N

Description: Lemma for hdmaprnN . Eliminate u . (Contributed by NM, 30-May-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hdmaprnlem15.h	|- H = ( LHyp ` K )
	hdmaprnlem15.u	|- U = ( ( DVecH ` K ) ` W )
	hdmaprnlem15.v	|- V = ( Base ` U )
	hdmaprnlem15.n	|- N = ( LSpan ` U )
	hdmaprnlem15.c	|- C = ( ( LCDual ` K ) ` W )
	hdmaprnlem15.d	|- D = ( Base ` C )
	hdmaprnlem15.q	|- .0. = ( 0g ` C )
	hdmaprnlem15.l	|- L = ( LSpan ` C )
	hdmaprnlem15.m	|- M = ( ( mapd ` K ) ` W )
	hdmaprnlem15.s	|- S = ( ( HDMap ` K ) ` W )
	hdmaprnlem15.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	hdmaprnlem15.se	|- ( ph -> s e. ( D \ { .0. } ) )
	hdmaprnlem15.ve	|- ( ph -> v e. V )
	hdmaprnlem15.e	|- ( ph -> ( M ` ( N ` { v } ) ) = ( L ` { s } ) )
Assertion	hdmaprnlem15N	|- ( ph -> s e. ran S )

Proof

Step	Hyp	Ref	Expression
1		hdmaprnlem15.h	|- H = ( LHyp ` K )
2		hdmaprnlem15.u	|- U = ( ( DVecH ` K ) ` W )
3		hdmaprnlem15.v	|- V = ( Base ` U )
4		hdmaprnlem15.n	|- N = ( LSpan ` U )
5		hdmaprnlem15.c	|- C = ( ( LCDual ` K ) ` W )
6		hdmaprnlem15.d	|- D = ( Base ` C )
7		hdmaprnlem15.q	|- .0. = ( 0g ` C )
8		hdmaprnlem15.l	|- L = ( LSpan ` C )
9		hdmaprnlem15.m	|- M = ( ( mapd ` K ) ` W )
10		hdmaprnlem15.s	|- S = ( ( HDMap ` K ) ` W )
11		hdmaprnlem15.k	|- ( ph -> ( K e. HL /\ W e. H ) )
12		hdmaprnlem15.se	|- ( ph -> s e. ( D \ { .0. } ) )
13		hdmaprnlem15.ve	|- ( ph -> v e. V )
14		hdmaprnlem15.e	|- ( ph -> ( M ` ( N ` { v } ) ) = ( L ` { s } ) )
15	1 2 3 4 11 13	dvh2dim	|- ( ph -> E. t e. V -. t e. ( N ` { v } ) )
16	11	3ad2ant1	|- ( ( ph /\ t e. V /\ -. t e. ( N ` { v } ) ) -> ( K e. HL /\ W e. H ) )
17	12	3ad2ant1	|- ( ( ph /\ t e. V /\ -. t e. ( N ` { v } ) ) -> s e. ( D \ { .0. } ) )
18	13	3ad2ant1	|- ( ( ph /\ t e. V /\ -. t e. ( N ` { v } ) ) -> v e. V )
19	14	3ad2ant1	|- ( ( ph /\ t e. V /\ -. t e. ( N ` { v } ) ) -> ( M ` ( N ` { v } ) ) = ( L ` { s } ) )
20		simp2	|- ( ( ph /\ t e. V /\ -. t e. ( N ` { v } ) ) -> t e. V )
21		simp3	|- ( ( ph /\ t e. V /\ -. t e. ( N ` { v } ) ) -> -. t e. ( N ` { v } ) )
22		eqid	|- ( 0g ` U ) = ( 0g ` U )
23		eqid	|- ( +g ` C ) = ( +g ` C )
24		eqid	|- ( +g ` U ) = ( +g ` U )
25	1 2 3 4 5 8 9 10 16 17 18 19 20 21 6 7 22 23 24	hdmaprnlem11N	|- ( ( ph /\ t e. V /\ -. t e. ( N ` { v } ) ) -> s e. ran S )
26	25	rexlimdv3a	|- ( ph -> ( E. t e. V -. t e. ( N ` { v } ) -> s e. ran S ) )
27	15 26	mpd	|- ( ph -> s e. ran S )