Theorem hdmap1eulem

Description: Lemma for hdmap1eu . TODO: combine with hdmap1eu or at least share some hypotheses. (Contributed by NM, 15-May-2015)

	Ref	Expression
Hypotheses	hdmap1eulem.h	|- H = ( LHyp ` K )
	hdmap1eulem.u	|- U = ( ( DVecH ` K ) ` W )
	hdmap1eulem.v	|- V = ( Base ` U )
	hdmap1eulem.s	|- .- = ( -g ` U )
	hdmap1eulem.o	|- .0. = ( 0g ` U )
	hdmap1eulem.n	|- N = ( LSpan ` U )
	hdmap1eulem.c	|- C = ( ( LCDual ` K ) ` W )
	hdmap1eulem.d	|- D = ( Base ` C )
	hdmap1eulem.r	|- R = ( -g ` C )
	hdmap1eulem.q	|- Q = ( 0g ` C )
	hdmap1eulem.j	|- J = ( LSpan ` C )
	hdmap1eulem.m	|- M = ( ( mapd ` K ) ` W )
	hdmap1eulem.i	|- I = ( ( HDMap1 ` K ) ` W )
	hdmap1eulem.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	hdmap1eulem.mn	|- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )
	hdmap1eulem.x	|- ( ph -> X e. ( V \ { .0. } ) )
	hdmap1eulem.f	|- ( ph -> F e. D )
	hdmap1eulem.y	|- ( ph -> T e. V )
	hdmap1eulem.l	|- L = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )
Assertion	hdmap1eulem	|- ( ph -> E! y e. D A. z e. V ( -. z e. ( ( N ` { X } ) u. ( N ` { T } ) ) -> y = ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) ) )

Proof

Step	Hyp	Ref	Expression
1		hdmap1eulem.h	|- H = ( LHyp ` K )
2		hdmap1eulem.u	|- U = ( ( DVecH ` K ) ` W )
3		hdmap1eulem.v	|- V = ( Base ` U )
4		hdmap1eulem.s	|- .- = ( -g ` U )
5		hdmap1eulem.o	|- .0. = ( 0g ` U )
6		hdmap1eulem.n	|- N = ( LSpan ` U )
7		hdmap1eulem.c	|- C = ( ( LCDual ` K ) ` W )
8		hdmap1eulem.d	|- D = ( Base ` C )
9		hdmap1eulem.r	|- R = ( -g ` C )
10		hdmap1eulem.q	|- Q = ( 0g ` C )
11		hdmap1eulem.j	|- J = ( LSpan ` C )
12		hdmap1eulem.m	|- M = ( ( mapd ` K ) ` W )
13		hdmap1eulem.i	|- I = ( ( HDMap1 ` K ) ` W )
14		hdmap1eulem.k	|- ( ph -> ( K e. HL /\ W e. H ) )
15		hdmap1eulem.mn	|- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )
16		hdmap1eulem.x	|- ( ph -> X e. ( V \ { .0. } ) )
17		hdmap1eulem.f	|- ( ph -> F e. D )
18		hdmap1eulem.y	|- ( ph -> T e. V )
19		hdmap1eulem.l	|- L = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )
20	1 2 3 4 5 6 7 8 9 10 11 12 19 14 17 15 16 18	mapdh9a	|- ( ph -> E! y e. D A. z e. V ( -. z e. ( ( N ` { X } ) u. ( N ` { T } ) ) -> y = ( L ` <. z , ( L ` <. X , F , z >. ) , T >. ) ) )
21	14	ad2antrr	|- ( ( ( ph /\ z e. V ) /\ -. z e. ( ( N ` { X } ) u. ( N ` { T } ) ) ) -> ( K e. HL /\ W e. H ) )
22	16	ad2antrr	|- ( ( ( ph /\ z e. V ) /\ -. z e. ( ( N ` { X } ) u. ( N ` { T } ) ) ) -> X e. ( V \ { .0. } ) )
23	17	ad2antrr	|- ( ( ( ph /\ z e. V ) /\ -. z e. ( ( N ` { X } ) u. ( N ` { T } ) ) ) -> F e. D )
24		simplr	|- ( ( ( ph /\ z e. V ) /\ -. z e. ( ( N ` { X } ) u. ( N ` { T } ) ) ) -> z e. V )
25	1 2 3 4 5 6 7 8 9 10 11 12 13 21 22 23 24 19	hdmap1valc	|- ( ( ( ph /\ z e. V ) /\ -. z e. ( ( N ` { X } ) u. ( N ` { T } ) ) ) -> ( I ` <. X , F , z >. ) = ( L ` <. X , F , z >. ) )
26	25	oteq2d	|- ( ( ( ph /\ z e. V ) /\ -. z e. ( ( N ` { X } ) u. ( N ` { T } ) ) ) -> <. z , ( I ` <. X , F , z >. ) , T >. = <. z , ( L ` <. X , F , z >. ) , T >. )
27	26	fveq2d	|- ( ( ( ph /\ z e. V ) /\ -. z e. ( ( N ` { X } ) u. ( N ` { T } ) ) ) -> ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) = ( I ` <. z , ( L ` <. X , F , z >. ) , T >. ) )
28		elun1	|- ( z e. ( N ` { X } ) -> z e. ( ( N ` { X } ) u. ( N ` { T } ) ) )
29	28	con3i	|- ( -. z e. ( ( N ` { X } ) u. ( N ` { T } ) ) -> -. z e. ( N ` { X } ) )
30	14	ad2antrr	|- ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X } ) ) -> ( K e. HL /\ W e. H ) )
31		eqid	|- ( LSubSp ` U ) = ( LSubSp ` U )
32	1 2 14	dvhlmod	|- ( ph -> U e. LMod )
33	32	ad2antrr	|- ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X } ) ) -> U e. LMod )
34	16	eldifad	|- ( ph -> X e. V )
35	34	ad2antrr	|- ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X } ) ) -> X e. V )
36	3 31 6	lspsncl	|- ( ( U e. LMod /\ X e. V ) -> ( N ` { X } ) e. ( LSubSp ` U ) )
37	33 35 36	syl2anc	|- ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X } ) ) -> ( N ` { X } ) e. ( LSubSp ` U ) )
38		simplr	|- ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X } ) ) -> z e. V )
39		simpr	|- ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X } ) ) -> -. z e. ( N ` { X } ) )
40	5 31 33 37 38 39	lssneln0	|- ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X } ) ) -> z e. ( V \ { .0. } ) )
41	17	ad2antrr	|- ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X } ) ) -> F e. D )
42	15	ad2antrr	|- ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X } ) ) -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )
43	16	ad2antrr	|- ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X } ) ) -> X e. ( V \ { .0. } ) )
44	3 6 33 38 35 39	lspsnne2	|- ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X } ) ) -> ( N ` { z } ) =/= ( N ` { X } ) )
45	44	necomd	|- ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X } ) ) -> ( N ` { X } ) =/= ( N ` { z } ) )
46	10 19 1 12 2 3 4 5 6 7 8 9 11 30 41 42 43 38 45	mapdhcl	|- ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X } ) ) -> ( L ` <. X , F , z >. ) e. D )
47	18	ad2antrr	|- ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X } ) ) -> T e. V )
48	1 2 3 4 5 6 7 8 9 10 11 12 13 30 40 46 47 19	hdmap1valc	|- ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X } ) ) -> ( I ` <. z , ( L ` <. X , F , z >. ) , T >. ) = ( L ` <. z , ( L ` <. X , F , z >. ) , T >. ) )
49	29 48	sylan2	|- ( ( ( ph /\ z e. V ) /\ -. z e. ( ( N ` { X } ) u. ( N ` { T } ) ) ) -> ( I ` <. z , ( L ` <. X , F , z >. ) , T >. ) = ( L ` <. z , ( L ` <. X , F , z >. ) , T >. ) )
50	27 49	eqtrd	|- ( ( ( ph /\ z e. V ) /\ -. z e. ( ( N ` { X } ) u. ( N ` { T } ) ) ) -> ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) = ( L ` <. z , ( L ` <. X , F , z >. ) , T >. ) )
51	50	eqeq2d	|- ( ( ( ph /\ z e. V ) /\ -. z e. ( ( N ` { X } ) u. ( N ` { T } ) ) ) -> ( y = ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) <-> y = ( L ` <. z , ( L ` <. X , F , z >. ) , T >. ) ) )
52	51	pm5.74da	|- ( ( ph /\ z e. V ) -> ( ( -. z e. ( ( N ` { X } ) u. ( N ` { T } ) ) -> y = ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) ) <-> ( -. z e. ( ( N ` { X } ) u. ( N ` { T } ) ) -> y = ( L ` <. z , ( L ` <. X , F , z >. ) , T >. ) ) ) )
53	52	ralbidva	|- ( ph -> ( A. z e. V ( -. z e. ( ( N ` { X } ) u. ( N ` { T } ) ) -> y = ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) ) <-> A. z e. V ( -. z e. ( ( N ` { X } ) u. ( N ` { T } ) ) -> y = ( L ` <. z , ( L ` <. X , F , z >. ) , T >. ) ) ) )
54	53	reubidv	|- ( ph -> ( E! y e. D A. z e. V ( -. z e. ( ( N ` { X } ) u. ( N ` { T } ) ) -> y = ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) ) <-> E! y e. D A. z e. V ( -. z e. ( ( N ` { X } ) u. ( N ` { T } ) ) -> y = ( L ` <. z , ( L ` <. X , F , z >. ) , T >. ) ) ) )
55	20 54	mpbird	|- ( ph -> E! y e. D A. z e. V ( -. z e. ( ( N ` { X } ) u. ( N ` { T } ) ) -> y = ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) ) )