Theorem hdmap1val

Description: Value of preliminary map from vectors to functionals in the closed kernel dual space. (Restatement of mapdhval .) TODO: change I = ( x e. _V |-> ... to ( ph -> ( I<. X , F , Y > ) = ... in e.g. mapdh8 to shorten proofs with no $d on x . (Contributed by NM, 15-May-2015)

	Ref	Expression
Hypotheses	hdmap1val.h	|- H = ( LHyp ` K )
	hdmap1fval.u	|- U = ( ( DVecH ` K ) ` W )
	hdmap1fval.v	|- V = ( Base ` U )
	hdmap1fval.s	|- .- = ( -g ` U )
	hdmap1fval.o	|- .0. = ( 0g ` U )
	hdmap1fval.n	|- N = ( LSpan ` U )
	hdmap1fval.c	|- C = ( ( LCDual ` K ) ` W )
	hdmap1fval.d	|- D = ( Base ` C )
	hdmap1fval.r	|- R = ( -g ` C )
	hdmap1fval.q	|- Q = ( 0g ` C )
	hdmap1fval.j	|- J = ( LSpan ` C )
	hdmap1fval.m	|- M = ( ( mapd ` K ) ` W )
	hdmap1fval.i	|- I = ( ( HDMap1 ` K ) ` W )
	hdmap1fval.k	|- ( ph -> ( K e. A /\ W e. H ) )
	hdmap1val.x	|- ( ph -> X e. V )
	hdmap1val.f	|- ( ph -> F e. D )
	hdmap1val.y	|- ( ph -> Y e. V )
Assertion	hdmap1val	|- ( ph -> ( I ` <. X , F , Y >. ) = if ( Y = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R h ) } ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		hdmap1val.h	|- H = ( LHyp ` K )
2		hdmap1fval.u	|- U = ( ( DVecH ` K ) ` W )
3		hdmap1fval.v	|- V = ( Base ` U )
4		hdmap1fval.s	|- .- = ( -g ` U )
5		hdmap1fval.o	|- .0. = ( 0g ` U )
6		hdmap1fval.n	|- N = ( LSpan ` U )
7		hdmap1fval.c	|- C = ( ( LCDual ` K ) ` W )
8		hdmap1fval.d	|- D = ( Base ` C )
9		hdmap1fval.r	|- R = ( -g ` C )
10		hdmap1fval.q	|- Q = ( 0g ` C )
11		hdmap1fval.j	|- J = ( LSpan ` C )
12		hdmap1fval.m	|- M = ( ( mapd ` K ) ` W )
13		hdmap1fval.i	|- I = ( ( HDMap1 ` K ) ` W )
14		hdmap1fval.k	|- ( ph -> ( K e. A /\ W e. H ) )
15		hdmap1val.x	|- ( ph -> X e. V )
16		hdmap1val.f	|- ( ph -> F e. D )
17		hdmap1val.y	|- ( ph -> Y e. V )
18		df-ot	|- <. X , F , Y >. = <. <. X , F >. , Y >.
19		opelxp	|- ( <. X , F >. e. ( V X. D ) <-> ( X e. V /\ F e. D ) )
20	15 16 19	sylanbrc	|- ( ph -> <. X , F >. e. ( V X. D ) )
21		opelxp	|- ( <. <. X , F >. , Y >. e. ( ( V X. D ) X. V ) <-> ( <. X , F >. e. ( V X. D ) /\ Y e. V ) )
22	20 17 21	sylanbrc	|- ( ph -> <. <. X , F >. , Y >. e. ( ( V X. D ) X. V ) )
23	18 22	eqeltrid	|- ( ph -> <. X , F , Y >. e. ( ( V X. D ) X. V ) )
24	1 2 3 4 5 6 7 8 9 10 11 12 13 14 23	hdmap1vallem	|- ( ph -> ( I ` <. X , F , Y >. ) = if ( ( 2nd ` <. X , F , Y >. ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` <. X , F , Y >. ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) } ) ) ) ) )
25		ot3rdg	|- ( Y e. V -> ( 2nd ` <. X , F , Y >. ) = Y )
26	17 25	syl	|- ( ph -> ( 2nd ` <. X , F , Y >. ) = Y )
27	26	eqeq1d	|- ( ph -> ( ( 2nd ` <. X , F , Y >. ) = .0. <-> Y = .0. ) )
28	26	sneqd	|- ( ph -> { ( 2nd ` <. X , F , Y >. ) } = { Y } )
29	28	fveq2d	|- ( ph -> ( N ` { ( 2nd ` <. X , F , Y >. ) } ) = ( N ` { Y } ) )
30	29	fveqeq2d	|- ( ph -> ( ( M ` ( N ` { ( 2nd ` <. X , F , Y >. ) } ) ) = ( J ` { h } ) <-> ( M ` ( N ` { Y } ) ) = ( J ` { h } ) ) )
31		ot1stg	|- ( ( X e. V /\ F e. D /\ Y e. V ) -> ( 1st ` ( 1st ` <. X , F , Y >. ) ) = X )
32	15 16 17 31	syl3anc	|- ( ph -> ( 1st ` ( 1st ` <. X , F , Y >. ) ) = X )
33	32 26	oveq12d	|- ( ph -> ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) = ( X .- Y ) )
34	33	sneqd	|- ( ph -> { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } = { ( X .- Y ) } )
35	34	fveq2d	|- ( ph -> ( N ` { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } ) = ( N ` { ( X .- Y ) } ) )
36	35	fveq2d	|- ( ph -> ( M ` ( N ` { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } ) ) = ( M ` ( N ` { ( X .- Y ) } ) ) )
37		ot2ndg	|- ( ( X e. V /\ F e. D /\ Y e. V ) -> ( 2nd ` ( 1st ` <. X , F , Y >. ) ) = F )
38	15 16 17 37	syl3anc	|- ( ph -> ( 2nd ` ( 1st ` <. X , F , Y >. ) ) = F )
39	38	oveq1d	|- ( ph -> ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) = ( F R h ) )
40	39	sneqd	|- ( ph -> { ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) } = { ( F R h ) } )
41	40	fveq2d	|- ( ph -> ( J ` { ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) } ) = ( J ` { ( F R h ) } ) )
42	36 41	eqeq12d	|- ( ph -> ( ( M ` ( N ` { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) } ) <-> ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R h ) } ) ) )
43	30 42	anbi12d	|- ( ph -> ( ( ( M ` ( N ` { ( 2nd ` <. X , F , Y >. ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) } ) ) <-> ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R h ) } ) ) ) )
44	43	riotabidv	|- ( ph -> ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` <. X , F , Y >. ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) } ) ) ) = ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R h ) } ) ) ) )
45	27 44	ifbieq2d	|- ( ph -> if ( ( 2nd ` <. X , F , Y >. ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` <. X , F , Y >. ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) } ) ) ) ) = if ( Y = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R h ) } ) ) ) ) )
46	24 45	eqtrd	|- ( ph -> ( I ` <. X , F , Y >. ) = if ( Y = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R h ) } ) ) ) ) )