Theorem hdmap1fval 37086

Description: Preliminary map from vectors to functionals in the closed kernel dual space. TODO: change span J to the convention L for this section. (Contributed by NM, 15-May-2015.)

Hypotheses

Ref	Expression
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 ) )

Assertion

Ref	Expression
hdmap1fval	|- ( ph -> I = ( x e. ( ( V X. D ) X. 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 ) } ) ) ) ) ) )

Distinct variable groups:   x, h, C   D, h, x   h, J, x   h, M, x   h, N, x   U, h, x   h, V, x

Allowed substitution hints:   ph( x, h)   A( x, h)   Q( x, h)   R( x, h)   H( x, h)   I( x, h)   K( x, h)   .- ( x, h)   W( x, h)   .0. ( x, h)

Proof of Theorem hdmap1fval

Dummy variables w a c d j m n u v are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		hdmap1fval.k	. 2 |- ( ph -> ( K e. A /\ W e. H ) )
2		hdmap1fval.i	. . . 4 |- I = ( (HDMap1 ` K ) ` W )
3		hdmap1val.h	. . . . . 6 |- H = ( LHyp ` K )
4	3	hdmap1ffval 37085	. . . . 5 |- ( K e. A -> (HDMap1 ` K ) = ( w e. H |-> { a | [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( (LCDual ` K ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( (mapd ` K ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) } ) )
5	4	fveq1d 6193	. . . 4 |- ( K e. A -> ( (HDMap1 ` K ) ` W ) = ( ( w e. H |-> { a | [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( (LCDual ` K ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( (mapd ` K ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) } ) ` W ) )
6	2, 5	syl5eq 2668	. . 3 |- ( K e. A -> I = ( ( w e. H |-> { a | [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( (LCDual ` K ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( (mapd ` K ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) } ) ` W ) )
7		fveq2 6191	. . . . . . 7 |- ( w = W -> ( ( DVecH ` K ) ` w ) = ( ( DVecH ` K ) ` W ) )
8		fveq2 6191	. . . . . . . . . 10 |- ( w = W -> ( (LCDual ` K ) ` w ) = ( (LCDual ` K ) ` W ) )
9		fveq2 6191	. . . . . . . . . . . . 13 |- ( w = W -> ( (mapd ` K ) ` w ) = ( (mapd ` K ) ` W ) )
10	9	sbceq1d 3440	. . . . . . . . . . . 12 |- ( w = W -> ( [. ( (mapd ` K ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) <-> [. ( (mapd ` K ) ` W ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) ) )
11	10	sbcbidv 3490	. . . . . . . . . . 11 |- ( w = W -> ( [. ( LSpan ` c ) / j ]. [. ( (mapd ` K ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) <-> [. ( LSpan ` c ) / j ]. [. ( (mapd ` K ) ` W ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) ) )
12	11	sbcbidv 3490	. . . . . . . . . 10 |- ( w = W -> ( [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( (mapd ` K ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) <-> [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( (mapd ` K ) ` W ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) ) )
13	8, 12	sbceqbid 3442	. . . . . . . . 9 |- ( w = W -> ( [. ( (LCDual ` K ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( (mapd ` K ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) <-> [. ( (LCDual ` K ) ` W ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( (mapd ` K ) ` W ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) ) )
14	13	sbcbidv 3490	. . . . . . . 8 |- ( w = W -> ( [. ( LSpan ` u ) / n ]. [. ( (LCDual ` K ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( (mapd ` K ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) <-> [. ( LSpan ` u ) / n ]. [. ( (LCDual ` K ) ` W ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( (mapd ` K ) ` W ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) ) )
15	14	sbcbidv 3490	. . . . . . 7 |- ( w = W -> ( [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( (LCDual ` K ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( (mapd ` K ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) <-> [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( (LCDual ` K ) ` W ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( (mapd ` K ) ` W ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) ) )
16	7, 15	sbceqbid 3442	. . . . . 6 |- ( w = W -> ( [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( (LCDual ` K ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( (mapd ` K ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) <-> [. ( ( DVecH ` K ) ` W ) / u ]. [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( (LCDual ` K ) ` W ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( (mapd ` K ) ` W ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) ) )
17		fvex 6201	. . . . . . 7 |- ( ( DVecH ` K ) ` W ) e. _V
18		fvex 6201	. . . . . . 7 |- ( Base ` u ) e. _V
19		fvex 6201	. . . . . . 7 |- ( LSpan ` u ) e. _V
20		hdmap1fval.u	. . . . . . . . . . 11 |- U = ( ( DVecH ` K ) ` W )
21	20	eqeq2i 2634	. . . . . . . . . 10 |- ( u = U <-> u = ( ( DVecH ` K ) ` W ) )
22	21	biimpri 218	. . . . . . . . 9 |- ( u = ( ( DVecH ` K ) ` W ) -> u = U )
23	22	3ad2ant1 1082	. . . . . . . 8 |- ( ( u = ( ( DVecH ` K ) ` W ) /\ v = ( Base ` u ) /\ n = ( LSpan ` u ) ) -> u = U )
24		simp2 1062	. . . . . . . . . 10 |- ( ( u = ( ( DVecH ` K ) ` W ) /\ v = ( Base ` u ) /\ n = ( LSpan ` u ) ) -> v = ( Base ` u ) )
25	22	fveq2d 6195	. . . . . . . . . . 11 |- ( u = ( ( DVecH ` K ) ` W ) -> ( Base ` u ) = ( Base ` U ) )
26	25	3ad2ant1 1082	. . . . . . . . . 10 |- ( ( u = ( ( DVecH ` K ) ` W ) /\ v = ( Base ` u ) /\ n = ( LSpan ` u ) ) -> ( Base ` u ) = ( Base ` U ) )
27	24, 26	eqtrd 2656	. . . . . . . . 9 |- ( ( u = ( ( DVecH ` K ) ` W ) /\ v = ( Base ` u ) /\ n = ( LSpan ` u ) ) -> v = ( Base ` U ) )
28		hdmap1fval.v	. . . . . . . . 9 |- V = ( Base ` U )
29	27, 28	syl6eqr 2674	. . . . . . . 8 |- ( ( u = ( ( DVecH ` K ) ` W ) /\ v = ( Base ` u ) /\ n = ( LSpan ` u ) ) -> v = V )
30		simp3 1063	. . . . . . . . . 10 |- ( ( u = ( ( DVecH ` K ) ` W ) /\ v = ( Base ` u ) /\ n = ( LSpan ` u ) ) -> n = ( LSpan ` u ) )
31	23	fveq2d 6195	. . . . . . . . . 10 |- ( ( u = ( ( DVecH ` K ) ` W ) /\ v = ( Base ` u ) /\ n = ( LSpan ` u ) ) -> ( LSpan ` u ) = ( LSpan ` U ) )
32	30, 31	eqtrd 2656	. . . . . . . . 9 |- ( ( u = ( ( DVecH ` K ) ` W ) /\ v = ( Base ` u ) /\ n = ( LSpan ` u ) ) -> n = ( LSpan ` U ) )
33		hdmap1fval.n	. . . . . . . . 9 |- N = ( LSpan ` U )
34	32, 33	syl6eqr 2674	. . . . . . . 8 |- ( ( u = ( ( DVecH ` K ) ` W ) /\ v = ( Base ` u ) /\ n = ( LSpan ` u ) ) -> n = N )
35		fvex 6201	. . . . . . . . . 10 |- ( (LCDual ` K ) ` W ) e. _V
36		fvex 6201	. . . . . . . . . 10 |- ( Base ` c ) e. _V
37		fvex 6201	. . . . . . . . . 10 |- ( LSpan ` c ) e. _V
38		id 22	. . . . . . . . . . . . 13 |- ( c = ( (LCDual ` K ) ` W ) -> c = ( (LCDual ` K ) ` W ) )
39		hdmap1fval.c	. . . . . . . . . . . . 13 |- C = ( (LCDual ` K ) ` W )
40	38, 39	syl6eqr 2674	. . . . . . . . . . . 12 |- ( c = ( (LCDual ` K ) ` W ) -> c = C )
41	40	3ad2ant1 1082	. . . . . . . . . . 11 |- ( ( c = ( (LCDual ` K ) ` W ) /\ d = ( Base ` c ) /\ j = ( LSpan ` c ) ) -> c = C )
42		simp2 1062	. . . . . . . . . . . 12 |- ( ( c = ( (LCDual ` K ) ` W ) /\ d = ( Base ` c ) /\ j = ( LSpan ` c ) ) -> d = ( Base ` c ) )
43	41	fveq2d 6195	. . . . . . . . . . . . 13 |- ( ( c = ( (LCDual ` K ) ` W ) /\ d = ( Base ` c ) /\ j = ( LSpan ` c ) ) -> ( Base ` c ) = ( Base ` C ) )
44		hdmap1fval.d	. . . . . . . . . . . . 13 |- D = ( Base ` C )
45	43, 44	syl6eqr 2674	. . . . . . . . . . . 12 |- ( ( c = ( (LCDual ` K ) ` W ) /\ d = ( Base ` c ) /\ j = ( LSpan ` c ) ) -> ( Base ` c ) = D )
46	42, 45	eqtrd 2656	. . . . . . . . . . 11 |- ( ( c = ( (LCDual ` K ) ` W ) /\ d = ( Base ` c ) /\ j = ( LSpan ` c ) ) -> d = D )
47		simp3 1063	. . . . . . . . . . . 12 |- ( ( c = ( (LCDual ` K ) ` W ) /\ d = ( Base ` c ) /\ j = ( LSpan ` c ) ) -> j = ( LSpan ` c ) )
48	41	fveq2d 6195	. . . . . . . . . . . . 13 |- ( ( c = ( (LCDual ` K ) ` W ) /\ d = ( Base ` c ) /\ j = ( LSpan ` c ) ) -> ( LSpan ` c ) = ( LSpan ` C ) )
49		hdmap1fval.j	. . . . . . . . . . . . 13 |- J = ( LSpan ` C )
50	48, 49	syl6eqr 2674	. . . . . . . . . . . 12 |- ( ( c = ( (LCDual ` K ) ` W ) /\ d = ( Base ` c ) /\ j = ( LSpan ` c ) ) -> ( LSpan ` c ) = J )
51	47, 50	eqtrd 2656	. . . . . . . . . . 11 |- ( ( c = ( (LCDual ` K ) ` W ) /\ d = ( Base ` c ) /\ j = ( LSpan ` c ) ) -> j = J )
52		fvex 6201	. . . . . . . . . . . . 13 |- ( (mapd ` K ) ` W ) e. _V
53		id 22	. . . . . . . . . . . . . . 15 |- ( m = ( (mapd ` K ) ` W ) -> m = ( (mapd ` K ) ` W ) )
54		hdmap1fval.m	. . . . . . . . . . . . . . 15 |- M = ( (mapd ` K ) ` W )
55	53, 54	syl6eqr 2674	. . . . . . . . . . . . . 14 |- ( m = ( (mapd ` K ) ` W ) -> m = M )
56		fveq1 6190	. . . . . . . . . . . . . . . . . . . 20 |- ( m = M -> ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( M ` ( n ` { ( 2nd ` x ) } ) ) )
57	56	eqeq1d 2624	. . . . . . . . . . . . . . . . . . 19 |- ( m = M -> ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) <-> ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) ) )
58		fveq1 6190	. . . . . . . . . . . . . . . . . . . 20 |- ( m = M -> ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( M ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) )
59	58	eqeq1d 2624	. . . . . . . . . . . . . . . . . . 19 |- ( m = M -> ( ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) <-> ( M ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) )
60	57, 59	anbi12d 747	. . . . . . . . . . . . . . . . . 18 |- ( m = M -> ( ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) <-> ( ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( M ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) )
61	60	riotabidv 6613	. . . . . . . . . . . . . . . . 17 |- ( m = M -> ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) = ( iota_ h e. d ( ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( M ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) )
62	61	ifeq2d 4105	. . . . . . . . . . . . . . . 16 |- ( m = M -> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) = if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( M ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) )
63	62	mpteq2dv 4745	. . . . . . . . . . . . . . 15 |- ( m = M -> ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) = ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( M ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) )
64	63	eleq2d 2687	. . . . . . . . . . . . . 14 |- ( m = M -> ( a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) <-> a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( M ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) ) )
65	55, 64	syl 17	. . . . . . . . . . . . 13 |- ( m = ( (mapd ` K ) ` W ) -> ( a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) <-> a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( M ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) ) )
66	52, 65	sbcie 3470	. . . . . . . . . . . 12 |- ( [. ( (mapd ` K ) ` W ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) <-> a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( M ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) )
67		simp2 1062	. . . . . . . . . . . . . . 15 |- ( ( c = C /\ d = D /\ j = J ) -> d = D )
68		xpeq2 5129	. . . . . . . . . . . . . . . 16 |- ( d = D -> ( v X. d ) = ( v X. D ) )
69	68	xpeq1d 5138	. . . . . . . . . . . . . . 15 |- ( d = D -> ( ( v X. d ) X. v ) = ( ( v X. D ) X. v ) )
70	67, 69	syl 17	. . . . . . . . . . . . . 14 |- ( ( c = C /\ d = D /\ j = J ) -> ( ( v X. d ) X. v ) = ( ( v X. D ) X. v ) )
71		simp1 1061	. . . . . . . . . . . . . . . . 17 |- ( ( c = C /\ d = D /\ j = J ) -> c = C )
72	71	fveq2d 6195	. . . . . . . . . . . . . . . 16 |- ( ( c = C /\ d = D /\ j = J ) -> ( 0g ` c ) = ( 0g ` C ) )
73		hdmap1fval.q	. . . . . . . . . . . . . . . 16 |- Q = ( 0g ` C )
74	72, 73	syl6eqr 2674	. . . . . . . . . . . . . . 15 |- ( ( c = C /\ d = D /\ j = J ) -> ( 0g ` c ) = Q )
75		simp3 1063	. . . . . . . . . . . . . . . . . . 19 |- ( ( c = C /\ d = D /\ j = J ) -> j = J )
76	75	fveq1d 6193	. . . . . . . . . . . . . . . . . 18 |- ( ( c = C /\ d = D /\ j = J ) -> ( j ` { h } ) = ( J ` { h } ) )
77	76	eqeq2d 2632	. . . . . . . . . . . . . . . . 17 |- ( ( c = C /\ d = D /\ j = J ) -> ( ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) <-> ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) ) )
78	71	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( c = C /\ d = D /\ j = J ) -> ( -g ` c ) = ( -g ` C ) )
79		hdmap1fval.r	. . . . . . . . . . . . . . . . . . . . . 22 |- R = ( -g ` C )
80	78, 79	syl6eqr 2674	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( c = C /\ d = D /\ j = J ) -> ( -g ` c ) = R )
81	80	oveqd 6667	. . . . . . . . . . . . . . . . . . . 20 |- ( ( c = C /\ d = D /\ j = J ) -> ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) = ( ( 2nd ` ( 1st ` x ) ) R h ) )
82	81	sneqd 4189	. . . . . . . . . . . . . . . . . . 19 |- ( ( c = C /\ d = D /\ j = J ) -> { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } = { ( ( 2nd ` ( 1st ` x ) ) R h ) } )
83	75, 82	fveq12d 6197	. . . . . . . . . . . . . . . . . 18 |- ( ( c = C /\ d = D /\ j = J ) -> ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) )
84	83	eqeq2d 2632	. . . . . . . . . . . . . . . . 17 |- ( ( c = C /\ d = D /\ j = J ) -> ( ( M ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) <-> ( M ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) )
85	77, 84	anbi12d 747	. . . . . . . . . . . . . . . 16 |- ( ( c = C /\ d = D /\ j = J ) -> ( ( ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( M ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) <-> ( ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) )
86	67, 85	riotaeqbidv 6614	. . . . . . . . . . . . . . 15 |- ( ( c = C /\ d = D /\ j = J ) -> ( iota_ h e. d ( ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( M ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) = ( iota_ h e. D ( ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) )
87	74, 86	ifeq12d 4106	. . . . . . . . . . . . . 14 |- ( ( c = C /\ d = D /\ j = J ) -> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( M ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) = if ( ( 2nd ` x ) = ( 0g ` u ) , Q , ( iota_ h e. D ( ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )
88	70, 87	mpteq12dv 4733	. . . . . . . . . . . . 13 |- ( ( c = C /\ d = D /\ j = J ) -> ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( M ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) = ( x e. ( ( v X. D ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , Q , ( iota_ h e. D ( ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) ) )
89	88	eleq2d 2687	. . . . . . . . . . . 12 |- ( ( c = C /\ d = D /\ j = J ) -> ( a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( M ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) <-> a e. ( x e. ( ( v X. D ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , Q , ( iota_ h e. D ( ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) ) ) )
90	66, 89	syl5bb 272	. . . . . . . . . . 11 |- ( ( c = C /\ d = D /\ j = J ) -> ( [. ( (mapd ` K ) ` W ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) <-> a e. ( x e. ( ( v X. D ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , Q , ( iota_ h e. D ( ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) ) ) )
91	41, 46, 51, 90	syl3anc 1326	. . . . . . . . . 10 |- ( ( c = ( (LCDual ` K ) ` W ) /\ d = ( Base ` c ) /\ j = ( LSpan ` c ) ) -> ( [. ( (mapd ` K ) ` W ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) <-> a e. ( x e. ( ( v X. D ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , Q , ( iota_ h e. D ( ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) ) ) )
92	35, 36, 37, 91	sbc3ie 3507	. . . . . . . . 9 |- ( [. ( (LCDual ` K ) ` W ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( (mapd ` K ) ` W ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) <-> a e. ( x e. ( ( v X. D ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , Q , ( iota_ h e. D ( ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) ) )
93		simp2 1062	. . . . . . . . . . . . 13 |- ( ( u = U /\ v = V /\ n = N ) -> v = V )
94	93	xpeq1d 5138	. . . . . . . . . . . 12 |- ( ( u = U /\ v = V /\ n = N ) -> ( v X. D ) = ( V X. D ) )
95	94, 93	xpeq12d 5140	. . . . . . . . . . 11 |- ( ( u = U /\ v = V /\ n = N ) -> ( ( v X. D ) X. v ) = ( ( V X. D ) X. V ) )
96		simp1 1061	. . . . . . . . . . . . . . 15 |- ( ( u = U /\ v = V /\ n = N ) -> u = U )
97	96	fveq2d 6195	. . . . . . . . . . . . . 14 |- ( ( u = U /\ v = V /\ n = N ) -> ( 0g ` u ) = ( 0g ` U ) )
98		hdmap1fval.o	. . . . . . . . . . . . . 14 |- .0. = ( 0g ` U )
99	97, 98	syl6eqr 2674	. . . . . . . . . . . . 13 |- ( ( u = U /\ v = V /\ n = N ) -> ( 0g ` u ) = .0. )
100	99	eqeq2d 2632	. . . . . . . . . . . 12 |- ( ( u = U /\ v = V /\ n = N ) -> ( ( 2nd ` x ) = ( 0g ` u ) <-> ( 2nd ` x ) = .0. ) )
101		simp3 1063	. . . . . . . . . . . . . . . . 17 |- ( ( u = U /\ v = V /\ n = N ) -> n = N )
102	101	fveq1d 6193	. . . . . . . . . . . . . . . 16 |- ( ( u = U /\ v = V /\ n = N ) -> ( n ` { ( 2nd ` x ) } ) = ( N ` { ( 2nd ` x ) } ) )
103	102	fveq2d 6195	. . . . . . . . . . . . . . 15 |- ( ( u = U /\ v = V /\ n = N ) -> ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( M ` ( N ` { ( 2nd ` x ) } ) ) )
104	103	eqeq1d 2624	. . . . . . . . . . . . . 14 |- ( ( u = U /\ v = V /\ n = N ) -> ( ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) <-> ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) ) )
105	96	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20 |- ( ( u = U /\ v = V /\ n = N ) -> ( -g ` u ) = ( -g ` U ) )
106		hdmap1fval.s	. . . . . . . . . . . . . . . . . . . 20 |- .- = ( -g ` U )
107	105, 106	syl6eqr 2674	. . . . . . . . . . . . . . . . . . 19 |- ( ( u = U /\ v = V /\ n = N ) -> ( -g ` u ) = .- )
108	107	oveqd 6667	. . . . . . . . . . . . . . . . . 18 |- ( ( u = U /\ v = V /\ n = N ) -> ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) = ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) )
109	108	sneqd 4189	. . . . . . . . . . . . . . . . 17 |- ( ( u = U /\ v = V /\ n = N ) -> { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } = { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } )
110	101, 109	fveq12d 6197	. . . . . . . . . . . . . . . 16 |- ( ( u = U /\ v = V /\ n = N ) -> ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) = ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) )
111	110	fveq2d 6195	. . . . . . . . . . . . . . 15 |- ( ( u = U /\ v = V /\ n = N ) -> ( M ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) )
112	111	eqeq1d 2624	. . . . . . . . . . . . . 14 |- ( ( u = U /\ v = V /\ n = N ) -> ( ( M ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) <-> ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) )
113	104, 112	anbi12d 747	. . . . . . . . . . . . 13 |- ( ( u = U /\ v = V /\ n = N ) -> ( ( ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) <-> ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) )
114	113	riotabidv 6613	. . . . . . . . . . . 12 |- ( ( u = U /\ v = V /\ n = N ) -> ( iota_ h e. D ( ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) = ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) )
115	100, 114	ifbieq2d 4111	. . . . . . . . . . 11 |- ( ( u = U /\ v = V /\ n = N ) -> if ( ( 2nd ` x ) = ( 0g ` u ) , Q , ( iota_ h e. D ( ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) = 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 ) } ) ) ) ) )
116	95, 115	mpteq12dv 4733	. . . . . . . . . 10 |- ( ( u = U /\ v = V /\ n = N ) -> ( x e. ( ( v X. D ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , Q , ( iota_ h e. D ( ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) ) = ( x e. ( ( V X. D ) X. 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 ) } ) ) ) ) ) )
117	116	eleq2d 2687	. . . . . . . . 9 |- ( ( u = U /\ v = V /\ n = N ) -> ( a e. ( x e. ( ( v X. D ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , Q , ( iota_ h e. D ( ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) ) <-> a e. ( x e. ( ( V X. D ) X. 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 ) } ) ) ) ) ) ) )
118	92, 117	syl5bb 272	. . . . . . . 8 |- ( ( u = U /\ v = V /\ n = N ) -> ( [. ( (LCDual ` K ) ` W ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( (mapd ` K ) ` W ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) <-> a e. ( x e. ( ( V X. D ) X. 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 ) } ) ) ) ) ) ) )
119	23, 29, 34, 118	syl3anc 1326	. . . . . . 7 |- ( ( u = ( ( DVecH ` K ) ` W ) /\ v = ( Base ` u ) /\ n = ( LSpan ` u ) ) -> ( [. ( (LCDual ` K ) ` W ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( (mapd ` K ) ` W ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) <-> a e. ( x e. ( ( V X. D ) X. 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 ) } ) ) ) ) ) ) )
120	17, 18, 19, 119	sbc3ie 3507	. . . . . 6 |- ( [. ( ( DVecH ` K ) ` W ) / u ]. [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( (LCDual ` K ) ` W ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( (mapd ` K ) ` W ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) <-> a e. ( x e. ( ( V X. D ) X. 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 ) } ) ) ) ) ) )
121	16, 120	syl6bb 276	. . . . 5 |- ( w = W -> ( [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( (LCDual ` K ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( (mapd ` K ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) <-> a e. ( x e. ( ( V X. D ) X. 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 ) } ) ) ) ) ) ) )
122	121	abbi1dv 2743	. . . 4 |- ( w = W -> { a | [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( (LCDual ` K ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( (mapd ` K ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) } = ( x e. ( ( V X. D ) X. 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 ) } ) ) ) ) ) )
123		eqid 2622	. . . 4 |- ( w e. H |-> { a | [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( (LCDual ` K ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( (mapd ` K ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) } ) = ( w e. H |-> { a | [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( (LCDual ` K ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( (mapd ` K ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) } )
124		fvex 6201	. . . . . . . 8 |- ( Base ` U ) e. _V
125	28, 124	eqeltri 2697	. . . . . . 7 |- V e. _V
126		fvex 6201	. . . . . . . 8 |- ( Base ` C ) e. _V
127	44, 126	eqeltri 2697	. . . . . . 7 |- D e. _V
128	125, 127	xpex 6962	. . . . . 6 |- ( V X. D ) e. _V
129	128, 125	xpex 6962	. . . . 5 |- ( ( V X. D ) X. V ) e. _V
130	129	mptex 6486	. . . 4 |- ( x e. ( ( V X. D ) X. 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 ) } ) ) ) ) ) e. _V
131	122, 123, 130	fvmpt 6282	. . 3 |- ( W e. H -> ( ( w e. H |-> { a | [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( LSpan ` u ) / n ]. [. ( (LCDual ` K ) ` w ) / c ]. [. ( Base ` c ) / d ]. [. ( LSpan ` c ) / j ]. [. ( (mapd ` K ) ` w ) / m ]. a e. ( x e. ( ( v X. d ) X. v ) |-> if ( ( 2nd ` x ) = ( 0g ` u ) , ( 0g ` c ) , ( iota_ h e. d ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) /\ ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) ) ) ) ) } ) ` W ) = ( x e. ( ( V X. D ) X. 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 ) } ) ) ) ) ) )
132	6, 131	sylan9eq 2676	. 2 |- ( ( K e. A /\ W e. H ) -> I = ( x e. ( ( V X. D ) X. 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 ) } ) ) ) ) ) )
133	1, 132	syl 17	1 |- ( ph -> I = ( x e. ( ( V X. D ) X. 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 ) } ) ) ) ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   {cab 2608   _Vcvv 3200   [.wsbc 3435   ifcif 4086   {csn 4177   |-> cmpt 4729   X. cxp 5112   ` cfv 5888   iota_crio 6610  (class class class)co 6650   1stc1st 7166   2ndc2nd 7167   Basecbs 15857   0gc0g 16100   -gcsg 17424   LSpanclspn 18971   LHypclh 35270   DVecHcdvh 36367  LCDualclcd 36875  mapdcmpd 36913  HDMap1chdma1 37081

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-hdmap1 37083

This theorem is referenced by:  hdmap1vallem  37087