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.t 
 ( ph > T e. ( ( V X. D ) X. V ) ) 
16 
1 2 3 4 5 6 7 8 9 10 11 12 13 14

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 ) } ) ) ) ) ) ) 
17 
16

fveq1d 
 ( ph > ( I ` T ) = ( ( 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 ) } ) ) ) ) ) ` T ) ) 
18 
10

fvexi 
 Q e. _V 
19 

riotaex 
 ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` T ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` T ) ) . ( 2nd ` T ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` T ) ) R h ) } ) ) ) e. _V 
20 
18 19

ifex 
 if ( ( 2nd ` T ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` T ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` T ) ) . ( 2nd ` T ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` T ) ) R h ) } ) ) ) ) e. _V 
21 

fveqeq2 
 ( x = T > ( ( 2nd ` x ) = .0. <> ( 2nd ` T ) = .0. ) ) 
22 

fveq2 
 ( x = T > ( 2nd ` x ) = ( 2nd ` T ) ) 
23 
22

sneqd 
 ( x = T > { ( 2nd ` x ) } = { ( 2nd ` T ) } ) 
24 
23

fveq2d 
 ( x = T > ( N ` { ( 2nd ` x ) } ) = ( N ` { ( 2nd ` T ) } ) ) 
25 
24

fveqeq2d 
 ( x = T > ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) <> ( M ` ( N ` { ( 2nd ` T ) } ) ) = ( J ` { h } ) ) ) 
26 

2fveq3 
 ( x = T > ( 1st ` ( 1st ` x ) ) = ( 1st ` ( 1st ` T ) ) ) 
27 
26 22

oveq12d 
 ( x = T > ( ( 1st ` ( 1st ` x ) ) . ( 2nd ` x ) ) = ( ( 1st ` ( 1st ` T ) ) . ( 2nd ` T ) ) ) 
28 
27

sneqd 
 ( x = T > { ( ( 1st ` ( 1st ` x ) ) . ( 2nd ` x ) ) } = { ( ( 1st ` ( 1st ` T ) ) . ( 2nd ` T ) ) } ) 
29 
28

fveq2d 
 ( x = T > ( N ` { ( ( 1st ` ( 1st ` x ) ) . ( 2nd ` x ) ) } ) = ( N ` { ( ( 1st ` ( 1st ` T ) ) . ( 2nd ` T ) ) } ) ) 
30 
29

fveq2d 
 ( x = T > ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) . ( 2nd ` x ) ) } ) ) = ( M ` ( N ` { ( ( 1st ` ( 1st ` T ) ) . ( 2nd ` T ) ) } ) ) ) 
31 

2fveq3 
 ( x = T > ( 2nd ` ( 1st ` x ) ) = ( 2nd ` ( 1st ` T ) ) ) 
32 
31

oveq1d 
 ( x = T > ( ( 2nd ` ( 1st ` x ) ) R h ) = ( ( 2nd ` ( 1st ` T ) ) R h ) ) 
33 
32

sneqd 
 ( x = T > { ( ( 2nd ` ( 1st ` x ) ) R h ) } = { ( ( 2nd ` ( 1st ` T ) ) R h ) } ) 
34 
33

fveq2d 
 ( x = T > ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) = ( J ` { ( ( 2nd ` ( 1st ` T ) ) R h ) } ) ) 
35 
30 34

eqeq12d 
 ( x = T > ( ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) . ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) <> ( M ` ( N ` { ( ( 1st ` ( 1st ` T ) ) . ( 2nd ` T ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` T ) ) R h ) } ) ) ) 
36 
25 35

anbi12d 
 ( x = T > ( ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) . ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) <> ( ( M ` ( N ` { ( 2nd ` T ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` T ) ) . ( 2nd ` T ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` T ) ) R h ) } ) ) ) ) 
37 
36

riotabidv 
 ( x = T > ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) . ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) = ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` T ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` T ) ) . ( 2nd ` T ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` T ) ) R h ) } ) ) ) ) 
38 
21 37

ifbieq2d 
 ( x = T > 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 ) } ) ) ) ) = if ( ( 2nd ` T ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` T ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` T ) ) . ( 2nd ` T ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` T ) ) R h ) } ) ) ) ) ) 
39 

eqid 
 ( 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 ) } ) ) ) ) ) = ( 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 ) } ) ) ) ) ) 
40 
38 39

fvmptg 
 ( ( T e. ( ( V X. D ) X. V ) /\ if ( ( 2nd ` T ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` T ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` T ) ) . ( 2nd ` T ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` T ) ) R h ) } ) ) ) ) e. _V ) > ( ( 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 ) } ) ) ) ) ) ` T ) = if ( ( 2nd ` T ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` T ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` T ) ) . ( 2nd ` T ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` T ) ) R h ) } ) ) ) ) ) 
41 
15 20 40

sylancl 
 ( ph > ( ( 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 ) } ) ) ) ) ) ` T ) = if ( ( 2nd ` T ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` T ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` T ) ) . ( 2nd ` T ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` T ) ) R h ) } ) ) ) ) ) 
42 
17 41

eqtrd 
 ( ph > ( I ` T ) = if ( ( 2nd ` T ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` T ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` T ) ) . ( 2nd ` T ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` T ) ) R h ) } ) ) ) ) ) 