Step 
Hyp 
Ref 
Expression 
1 

hdmap1val.h 
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) 
2 

hdmap1fval.u 
⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) 
3 

hdmap1fval.v 
⊢ 𝑉 = ( Base ‘ 𝑈 ) 
4 

hdmap1fval.s 
⊢ − = ( _{g} ‘ 𝑈 ) 
5 

hdmap1fval.o 
⊢ 0 = ( 0_{g} ‘ 𝑈 ) 
6 

hdmap1fval.n 
⊢ 𝑁 = ( LSpan ‘ 𝑈 ) 
7 

hdmap1fval.c 
⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) 
8 

hdmap1fval.d 
⊢ 𝐷 = ( Base ‘ 𝐶 ) 
9 

hdmap1fval.r 
⊢ 𝑅 = ( _{g} ‘ 𝐶 ) 
10 

hdmap1fval.q 
⊢ 𝑄 = ( 0_{g} ‘ 𝐶 ) 
11 

hdmap1fval.j 
⊢ 𝐽 = ( LSpan ‘ 𝐶 ) 
12 

hdmap1fval.m 
⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) 
13 

hdmap1fval.i 
⊢ 𝐼 = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) 
14 

hdmap1fval.k 
⊢ ( 𝜑 → ( 𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻 ) ) 
15 

hdmap1val.t 
⊢ ( 𝜑 → 𝑇 ∈ ( ( 𝑉 × 𝐷 ) × 𝑉 ) ) 
16 
1 2 3 4 5 6 7 8 9 10 11 12 13 14

hdmap1fval 
⊢ ( 𝜑 → 𝐼 = ( 𝑥 ∈ ( ( 𝑉 × 𝐷 ) × 𝑉 ) ↦ if ( ( 2^{nd} ‘ 𝑥 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^{nd} ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) − ( 2^{nd} ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) ) ) 
17 
16

fveq1d 
⊢ ( 𝜑 → ( 𝐼 ‘ 𝑇 ) = ( ( 𝑥 ∈ ( ( 𝑉 × 𝐷 ) × 𝑉 ) ↦ if ( ( 2^{nd} ‘ 𝑥 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^{nd} ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) − ( 2^{nd} ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) ) ‘ 𝑇 ) ) 
18 
10

fvexi 
⊢ 𝑄 ∈ V 
19 

riotaex 
⊢ ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^{nd} ‘ 𝑇 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑇 ) ) − ( 2^{nd} ‘ 𝑇 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑇 ) ) 𝑅 ℎ ) } ) ) ) ∈ V 
20 
18 19

ifex 
⊢ if ( ( 2^{nd} ‘ 𝑇 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^{nd} ‘ 𝑇 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑇 ) ) − ( 2^{nd} ‘ 𝑇 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑇 ) ) 𝑅 ℎ ) } ) ) ) ) ∈ V 
21 

fveqeq2 
⊢ ( 𝑥 = 𝑇 → ( ( 2^{nd} ‘ 𝑥 ) = 0 ↔ ( 2^{nd} ‘ 𝑇 ) = 0 ) ) 
22 

fveq2 
⊢ ( 𝑥 = 𝑇 → ( 2^{nd} ‘ 𝑥 ) = ( 2^{nd} ‘ 𝑇 ) ) 
23 
22

sneqd 
⊢ ( 𝑥 = 𝑇 → { ( 2^{nd} ‘ 𝑥 ) } = { ( 2^{nd} ‘ 𝑇 ) } ) 
24 
23

fveq2d 
⊢ ( 𝑥 = 𝑇 → ( 𝑁 ‘ { ( 2^{nd} ‘ 𝑥 ) } ) = ( 𝑁 ‘ { ( 2^{nd} ‘ 𝑇 ) } ) ) 
25 
24

fveqeq2d 
⊢ ( 𝑥 = 𝑇 → ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^{nd} ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ↔ ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^{nd} ‘ 𝑇 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ) ) 
26 

2fveq3 
⊢ ( 𝑥 = 𝑇 → ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) = ( 1^{st} ‘ ( 1^{st} ‘ 𝑇 ) ) ) 
27 
26 22

oveq12d 
⊢ ( 𝑥 = 𝑇 → ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) − ( 2^{nd} ‘ 𝑥 ) ) = ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑇 ) ) − ( 2^{nd} ‘ 𝑇 ) ) ) 
28 
27

sneqd 
⊢ ( 𝑥 = 𝑇 → { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) − ( 2^{nd} ‘ 𝑥 ) ) } = { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑇 ) ) − ( 2^{nd} ‘ 𝑇 ) ) } ) 
29 
28

fveq2d 
⊢ ( 𝑥 = 𝑇 → ( 𝑁 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) − ( 2^{nd} ‘ 𝑥 ) ) } ) = ( 𝑁 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑇 ) ) − ( 2^{nd} ‘ 𝑇 ) ) } ) ) 
30 
29

fveq2d 
⊢ ( 𝑥 = 𝑇 → ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) − ( 2^{nd} ‘ 𝑥 ) ) } ) ) = ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑇 ) ) − ( 2^{nd} ‘ 𝑇 ) ) } ) ) ) 
31 

2fveq3 
⊢ ( 𝑥 = 𝑇 → ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) = ( 2^{nd} ‘ ( 1^{st} ‘ 𝑇 ) ) ) 
32 
31

oveq1d 
⊢ ( 𝑥 = 𝑇 → ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) 𝑅 ℎ ) = ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑇 ) ) 𝑅 ℎ ) ) 
33 
32

sneqd 
⊢ ( 𝑥 = 𝑇 → { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) 𝑅 ℎ ) } = { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑇 ) ) 𝑅 ℎ ) } ) 
34 
33

fveq2d 
⊢ ( 𝑥 = 𝑇 → ( 𝐽 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) 𝑅 ℎ ) } ) = ( 𝐽 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑇 ) ) 𝑅 ℎ ) } ) ) 
35 
30 34

eqeq12d 
⊢ ( 𝑥 = 𝑇 → ( ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) − ( 2^{nd} ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ↔ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑇 ) ) − ( 2^{nd} ‘ 𝑇 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑇 ) ) 𝑅 ℎ ) } ) ) ) 
36 
25 35

anbi12d 
⊢ ( 𝑥 = 𝑇 → ( ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^{nd} ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) − ( 2^{nd} ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ↔ ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^{nd} ‘ 𝑇 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑇 ) ) − ( 2^{nd} ‘ 𝑇 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑇 ) ) 𝑅 ℎ ) } ) ) ) ) 
37 
36

riotabidv 
⊢ ( 𝑥 = 𝑇 → ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^{nd} ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) − ( 2^{nd} ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) = ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^{nd} ‘ 𝑇 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑇 ) ) − ( 2^{nd} ‘ 𝑇 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑇 ) ) 𝑅 ℎ ) } ) ) ) ) 
38 
21 37

ifbieq2d 
⊢ ( 𝑥 = 𝑇 → if ( ( 2^{nd} ‘ 𝑥 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^{nd} ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) − ( 2^{nd} ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) = if ( ( 2^{nd} ‘ 𝑇 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^{nd} ‘ 𝑇 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑇 ) ) − ( 2^{nd} ‘ 𝑇 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑇 ) ) 𝑅 ℎ ) } ) ) ) ) ) 
39 

eqid 
⊢ ( 𝑥 ∈ ( ( 𝑉 × 𝐷 ) × 𝑉 ) ↦ if ( ( 2^{nd} ‘ 𝑥 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^{nd} ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) − ( 2^{nd} ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) ) = ( 𝑥 ∈ ( ( 𝑉 × 𝐷 ) × 𝑉 ) ↦ if ( ( 2^{nd} ‘ 𝑥 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^{nd} ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) − ( 2^{nd} ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) ) 
40 
38 39

fvmptg 
⊢ ( ( 𝑇 ∈ ( ( 𝑉 × 𝐷 ) × 𝑉 ) ∧ if ( ( 2^{nd} ‘ 𝑇 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^{nd} ‘ 𝑇 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑇 ) ) − ( 2^{nd} ‘ 𝑇 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑇 ) ) 𝑅 ℎ ) } ) ) ) ) ∈ V ) → ( ( 𝑥 ∈ ( ( 𝑉 × 𝐷 ) × 𝑉 ) ↦ if ( ( 2^{nd} ‘ 𝑥 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^{nd} ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) − ( 2^{nd} ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) ) ‘ 𝑇 ) = if ( ( 2^{nd} ‘ 𝑇 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^{nd} ‘ 𝑇 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑇 ) ) − ( 2^{nd} ‘ 𝑇 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑇 ) ) 𝑅 ℎ ) } ) ) ) ) ) 
41 
15 20 40

sylancl 
⊢ ( 𝜑 → ( ( 𝑥 ∈ ( ( 𝑉 × 𝐷 ) × 𝑉 ) ↦ if ( ( 2^{nd} ‘ 𝑥 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^{nd} ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) − ( 2^{nd} ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) ) ‘ 𝑇 ) = if ( ( 2^{nd} ‘ 𝑇 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^{nd} ‘ 𝑇 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑇 ) ) − ( 2^{nd} ‘ 𝑇 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑇 ) ) 𝑅 ℎ ) } ) ) ) ) ) 
42 
17 41

eqtrd 
⊢ ( 𝜑 → ( 𝐼 ‘ 𝑇 ) = if ( ( 2^{nd} ‘ 𝑇 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^{nd} ‘ 𝑇 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑇 ) ) − ( 2^{nd} ‘ 𝑇 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑇 ) ) 𝑅 ℎ ) } ) ) ) ) ) 