Metamath Proof Explorer

Theorem hdmap1fval

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)

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 ) )
Assertion 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 ) } ) ) ) ) ) )

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 1 hdmap1ffval 
 |-  ( 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 ) } ) ) ) ) ) } ) )
16 15 fveq1d 
 |-  ( 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 ) )
17 13 16 eqtrid 
 |-  ( 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 ) )
18 fveq2 
 |-  ( w = W -> ( ( DVecH ` K ) ` w ) = ( ( DVecH ` K ) ` W ) )
19 fveq2 
 |-  ( w = W -> ( ( LCDual ` K ) ` w ) = ( ( LCDual ` K ) ` W ) )
20 fveq2 
 |-  ( w = W -> ( ( mapd ` K ) ` w ) = ( ( mapd ` K ) ` W ) )
21 20 sbceq1d 
 |-  ( 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 ) } ) ) ) ) ) ) )
22 21 sbcbidv 
 |-  ( 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 ) } ) ) ) ) ) ) )
23 22 sbcbidv 
 |-  ( 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 ) } ) ) ) ) ) ) )
24 19 23 sbceqbid 
 |-  ( 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 ) } ) ) ) ) ) ) )
25 24 sbcbidv 
 |-  ( 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 ) } ) ) ) ) ) ) )
26 25 sbcbidv 
 |-  ( 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 ) } ) ) ) ) ) ) )
27 18 26 sbceqbid 
 |-  ( 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 ) } ) ) ) ) ) ) )
28 fvex 
 |-  ( ( DVecH ` K ) ` W ) e. _V
29 fvex 
 |-  ( Base ` u ) e. _V
30 fvex 
 |-  ( LSpan ` u ) e. _V
31 2 eqeq2i 
 |-  ( u = U <-> u = ( ( DVecH ` K ) ` W ) )
32 31 biimpri 
 |-  ( u = ( ( DVecH ` K ) ` W ) -> u = U )
33 32 3ad2ant1 
 |-  ( ( u = ( ( DVecH ` K ) ` W ) /\ v = ( Base ` u ) /\ n = ( LSpan ` u ) ) -> u = U )
34 simp2 
 |-  ( ( u = ( ( DVecH ` K ) ` W ) /\ v = ( Base ` u ) /\ n = ( LSpan ` u ) ) -> v = ( Base ` u ) )
35 32 fveq2d 
 |-  ( u = ( ( DVecH ` K ) ` W ) -> ( Base ` u ) = ( Base ` U ) )
36 35 3ad2ant1 
 |-  ( ( u = ( ( DVecH ` K ) ` W ) /\ v = ( Base ` u ) /\ n = ( LSpan ` u ) ) -> ( Base ` u ) = ( Base ` U ) )
37 34 36 eqtrd 
 |-  ( ( u = ( ( DVecH ` K ) ` W ) /\ v = ( Base ` u ) /\ n = ( LSpan ` u ) ) -> v = ( Base ` U ) )
38 37 3 eqtr4di 
 |-  ( ( u = ( ( DVecH ` K ) ` W ) /\ v = ( Base ` u ) /\ n = ( LSpan ` u ) ) -> v = V )
39 simp3 
 |-  ( ( u = ( ( DVecH ` K ) ` W ) /\ v = ( Base ` u ) /\ n = ( LSpan ` u ) ) -> n = ( LSpan ` u ) )
40 33 fveq2d 
 |-  ( ( u = ( ( DVecH ` K ) ` W ) /\ v = ( Base ` u ) /\ n = ( LSpan ` u ) ) -> ( LSpan ` u ) = ( LSpan ` U ) )
41 39 40 eqtrd 
 |-  ( ( u = ( ( DVecH ` K ) ` W ) /\ v = ( Base ` u ) /\ n = ( LSpan ` u ) ) -> n = ( LSpan ` U ) )
42 41 6 eqtr4di 
 |-  ( ( u = ( ( DVecH ` K ) ` W ) /\ v = ( Base ` u ) /\ n = ( LSpan ` u ) ) -> n = N )
43 fvex 
 |-  ( ( LCDual ` K ) ` W ) e. _V
44 fvex 
 |-  ( Base ` c ) e. _V
45 fvex 
 |-  ( LSpan ` c ) e. _V
46 id 
 |-  ( c = ( ( LCDual ` K ) ` W ) -> c = ( ( LCDual ` K ) ` W ) )
47 46 7 eqtr4di 
 |-  ( c = ( ( LCDual ` K ) ` W ) -> c = C )
48 47 3ad2ant1 
 |-  ( ( c = ( ( LCDual ` K ) ` W ) /\ d = ( Base ` c ) /\ j = ( LSpan ` c ) ) -> c = C )
49 simp2 
 |-  ( ( c = ( ( LCDual ` K ) ` W ) /\ d = ( Base ` c ) /\ j = ( LSpan ` c ) ) -> d = ( Base ` c ) )
50 48 fveq2d 
 |-  ( ( c = ( ( LCDual ` K ) ` W ) /\ d = ( Base ` c ) /\ j = ( LSpan ` c ) ) -> ( Base ` c ) = ( Base ` C ) )
51 50 8 eqtr4di 
 |-  ( ( c = ( ( LCDual ` K ) ` W ) /\ d = ( Base ` c ) /\ j = ( LSpan ` c ) ) -> ( Base ` c ) = D )
52 49 51 eqtrd 
 |-  ( ( c = ( ( LCDual ` K ) ` W ) /\ d = ( Base ` c ) /\ j = ( LSpan ` c ) ) -> d = D )
53 simp3 
 |-  ( ( c = ( ( LCDual ` K ) ` W ) /\ d = ( Base ` c ) /\ j = ( LSpan ` c ) ) -> j = ( LSpan ` c ) )
54 48 fveq2d 
 |-  ( ( c = ( ( LCDual ` K ) ` W ) /\ d = ( Base ` c ) /\ j = ( LSpan ` c ) ) -> ( LSpan ` c ) = ( LSpan ` C ) )
55 54 11 eqtr4di 
 |-  ( ( c = ( ( LCDual ` K ) ` W ) /\ d = ( Base ` c ) /\ j = ( LSpan ` c ) ) -> ( LSpan ` c ) = J )
56 53 55 eqtrd 
 |-  ( ( c = ( ( LCDual ` K ) ` W ) /\ d = ( Base ` c ) /\ j = ( LSpan ` c ) ) -> j = J )
57 fvex 
 |-  ( ( mapd ` K ) ` W ) e. _V
58 id 
 |-  ( m = ( ( mapd ` K ) ` W ) -> m = ( ( mapd ` K ) ` W ) )
59 58 12 eqtr4di 
 |-  ( m = ( ( mapd ` K ) ` W ) -> m = M )
60 fveq1 
 |-  ( m = M -> ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( M ` ( n ` { ( 2nd ` x ) } ) ) )
61 60 eqeq1d 
 |-  ( m = M -> ( ( m ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) <-> ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) ) )
62 fveq1 
 |-  ( m = M -> ( m ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) = ( M ` ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) ) )
63 62 eqeq1d 
 |-  ( 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 ) } ) ) )
64 61 63 anbi12d 
 |-  ( 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 ) } ) ) ) )
65 64 riotabidv 
 |-  ( 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 ) } ) ) ) )
66 65 ifeq2d 
 |-  ( 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 ) } ) ) ) ) )
67 66 mpteq2dv 
 |-  ( 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 ) } ) ) ) ) ) )
68 67 eleq2d 
 |-  ( 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 ) } ) ) ) ) ) ) )
69 59 68 syl 
 |-  ( 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 ) } ) ) ) ) ) ) )
70 57 69 sbcie 
 |-  ( [. ( ( 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 ) } ) ) ) ) ) )
71 simp2 
 |-  ( ( c = C /\ d = D /\ j = J ) -> d = D )
72 xpeq2 
 |-  ( d = D -> ( v X. d ) = ( v X. D ) )
73 72 xpeq1d 
 |-  ( d = D -> ( ( v X. d ) X. v ) = ( ( v X. D ) X. v ) )
74 71 73 syl 
 |-  ( ( c = C /\ d = D /\ j = J ) -> ( ( v X. d ) X. v ) = ( ( v X. D ) X. v ) )
75 simp1 
 |-  ( ( c = C /\ d = D /\ j = J ) -> c = C )
76 75 fveq2d 
 |-  ( ( c = C /\ d = D /\ j = J ) -> ( 0g ` c ) = ( 0g ` C ) )
77 76 10 eqtr4di 
 |-  ( ( c = C /\ d = D /\ j = J ) -> ( 0g ` c ) = Q )
78 simp3 
 |-  ( ( c = C /\ d = D /\ j = J ) -> j = J )
79 78 fveq1d 
 |-  ( ( c = C /\ d = D /\ j = J ) -> ( j ` { h } ) = ( J ` { h } ) )
80 79 eqeq2d 
 |-  ( ( c = C /\ d = D /\ j = J ) -> ( ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( j ` { h } ) <-> ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) ) )
81 75 fveq2d 
 |-  ( ( c = C /\ d = D /\ j = J ) -> ( -g ` c ) = ( -g ` C ) )
82 81 9 eqtr4di 
 |-  ( ( c = C /\ d = D /\ j = J ) -> ( -g ` c ) = R )
83 82 oveqd 
 |-  ( ( c = C /\ d = D /\ j = J ) -> ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) = ( ( 2nd ` ( 1st ` x ) ) R h ) )
84 83 sneqd 
 |-  ( ( c = C /\ d = D /\ j = J ) -> { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } = { ( ( 2nd ` ( 1st ` x ) ) R h ) } )
85 78 84 fveq12d 
 |-  ( ( c = C /\ d = D /\ j = J ) -> ( j ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` c ) h ) } ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) )
86 85 eqeq2d 
 |-  ( ( 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 ) } ) ) )
87 80 86 anbi12d 
 |-  ( ( 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 ) } ) ) ) )
88 71 87 riotaeqbidv 
 |-  ( ( 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 ) } ) ) ) )
89 77 88 ifeq12d 
 |-  ( ( 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 ) } ) ) ) ) )
90 74 89 mpteq12dv 
 |-  ( ( 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 ) } ) ) ) ) ) )
91 90 eleq2d 
 |-  ( ( 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 ) } ) ) ) ) ) ) )
92 70 91 bitrid 
 |-  ( ( 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 ) } ) ) ) ) ) ) )
93 48 52 56 92 syl3anc 
 |-  ( ( 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 ) } ) ) ) ) ) ) )
94 43 44 45 93 sbc3ie 
 |-  ( [. ( ( 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 ) } ) ) ) ) ) )
95 simp2 
 |-  ( ( u = U /\ v = V /\ n = N ) -> v = V )
96 95 xpeq1d 
 |-  ( ( u = U /\ v = V /\ n = N ) -> ( v X. D ) = ( V X. D ) )
97 96 95 xpeq12d 
 |-  ( ( u = U /\ v = V /\ n = N ) -> ( ( v X. D ) X. v ) = ( ( V X. D ) X. V ) )
98 simp1 
 |-  ( ( u = U /\ v = V /\ n = N ) -> u = U )
99 98 fveq2d 
 |-  ( ( u = U /\ v = V /\ n = N ) -> ( 0g ` u ) = ( 0g ` U ) )
100 99 5 eqtr4di 
 |-  ( ( u = U /\ v = V /\ n = N ) -> ( 0g ` u ) = .0. )
101 100 eqeq2d 
 |-  ( ( u = U /\ v = V /\ n = N ) -> ( ( 2nd ` x ) = ( 0g ` u ) <-> ( 2nd ` x ) = .0. ) )
102 simp3 
 |-  ( ( u = U /\ v = V /\ n = N ) -> n = N )
103 102 fveq1d 
 |-  ( ( u = U /\ v = V /\ n = N ) -> ( n ` { ( 2nd ` x ) } ) = ( N ` { ( 2nd ` x ) } ) )
104 103 fveqeq2d 
 |-  ( ( u = U /\ v = V /\ n = N ) -> ( ( M ` ( n ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) <-> ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) ) )
105 98 fveq2d 
 |-  ( ( u = U /\ v = V /\ n = N ) -> ( -g ` u ) = ( -g ` U ) )
106 105 4 eqtr4di 
 |-  ( ( u = U /\ v = V /\ n = N ) -> ( -g ` u ) = .- )
107 106 oveqd 
 |-  ( ( u = U /\ v = V /\ n = N ) -> ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) = ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) )
108 107 sneqd 
 |-  ( ( u = U /\ v = V /\ n = N ) -> { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } = { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } )
109 102 108 fveq12d 
 |-  ( ( u = U /\ v = V /\ n = N ) -> ( n ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` u ) ( 2nd ` x ) ) } ) = ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) )
110 109 fveqeq2d 
 |-  ( ( 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 ) } ) ) )
111 104 110 anbi12d 
 |-  ( ( 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 ) } ) ) ) )
112 111 riotabidv 
 |-  ( ( 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 ) } ) ) ) )
113 101 112 ifbieq2d 
 |-  ( ( 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 ) } ) ) ) ) )
114 97 113 mpteq12dv 
 |-  ( ( 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 ) } ) ) ) ) ) )
115 114 eleq2d 
 |-  ( ( 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 ) } ) ) ) ) ) ) )
116 94 115 bitrid 
 |-  ( ( 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 ) } ) ) ) ) ) ) )
117 33 38 42 116 syl3anc 
 |-  ( ( 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 ) } ) ) ) ) ) ) )
118 28 29 30 117 sbc3ie 
 |-  ( [. ( ( 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 ) } ) ) ) ) ) )
119 27 118 bitrdi 
 |-  ( 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 ) } ) ) ) ) ) ) )
120 119 eqabcdv 
 |-  ( 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 ) } ) ) ) ) ) )
121 eqid 
 |-  ( 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 ) } ) ) ) ) ) } )
122 3 fvexi 
 |-  V e. _V
123 8 fvexi 
 |-  D e. _V
124 122 123 xpex 
 |-  ( V X. D ) e. _V
125 124 122 xpex 
 |-  ( ( V X. D ) X. V ) e. _V
126 125 mptex 
 |-  ( 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
127 120 121 126 fvmpt 
 |-  ( 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 ) } ) ) ) ) ) )
128 17 127 sylan9eq 
 |-  ( ( 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 ) } ) ) ) ) ) )
129 14 128 syl 
 |-  ( 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 ) } ) ) ) ) ) )