Step 
Hyp 
Ref 
Expression 
1 

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

elex 
⊢ ( 𝐾 ∈ 𝑋 → 𝐾 ∈ V ) 
3 

fveq2 
⊢ ( 𝑘 = 𝐾 → ( LHyp ‘ 𝑘 ) = ( LHyp ‘ 𝐾 ) ) 
4 
3 1

syl6eqr 
⊢ ( 𝑘 = 𝐾 → ( LHyp ‘ 𝑘 ) = 𝐻 ) 
5 

fveq2 
⊢ ( 𝑘 = 𝐾 → ( DVecH ‘ 𝑘 ) = ( DVecH ‘ 𝐾 ) ) 
6 
5

fveq1d 
⊢ ( 𝑘 = 𝐾 → ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) 
7 

fveq2 
⊢ ( 𝑘 = 𝐾 → ( LCDual ‘ 𝑘 ) = ( LCDual ‘ 𝐾 ) ) 
8 
7

fveq1d 
⊢ ( 𝑘 = 𝐾 → ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) = ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) 
9 

fveq2 
⊢ ( 𝑘 = 𝐾 → ( mapd ‘ 𝑘 ) = ( mapd ‘ 𝐾 ) ) 
10 
9

fveq1d 
⊢ ( 𝑘 = 𝐾 → ( ( mapd ‘ 𝑘 ) ‘ 𝑤 ) = ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) ) 
11 
10

sbceq1d 
⊢ ( 𝑘 = 𝐾 → ( [ ( ( mapd ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^{nd} ‘ 𝑥 ) = ( 0_{g} ‘ 𝑢 ) , ( 0_{g} ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^{nd} ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑢 ) ( 2^{nd} ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ↔ [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^{nd} ‘ 𝑥 ) = ( 0_{g} ‘ 𝑢 ) , ( 0_{g} ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^{nd} ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑢 ) ( 2^{nd} ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ) ) 
12 
11

sbcbidv 
⊢ ( 𝑘 = 𝐾 → ( [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^{nd} ‘ 𝑥 ) = ( 0_{g} ‘ 𝑢 ) , ( 0_{g} ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^{nd} ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑢 ) ( 2^{nd} ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ↔ [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^{nd} ‘ 𝑥 ) = ( 0_{g} ‘ 𝑢 ) , ( 0_{g} ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^{nd} ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑢 ) ( 2^{nd} ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ) ) 
13 
12

sbcbidv 
⊢ ( 𝑘 = 𝐾 → ( [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^{nd} ‘ 𝑥 ) = ( 0_{g} ‘ 𝑢 ) , ( 0_{g} ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^{nd} ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑢 ) ( 2^{nd} ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ↔ [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^{nd} ‘ 𝑥 ) = ( 0_{g} ‘ 𝑢 ) , ( 0_{g} ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^{nd} ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑢 ) ( 2^{nd} ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ) ) 
14 
8 13

sbceqbid 
⊢ ( 𝑘 = 𝐾 → ( [ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^{nd} ‘ 𝑥 ) = ( 0_{g} ‘ 𝑢 ) , ( 0_{g} ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^{nd} ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑢 ) ( 2^{nd} ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ↔ [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^{nd} ‘ 𝑥 ) = ( 0_{g} ‘ 𝑢 ) , ( 0_{g} ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^{nd} ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑢 ) ( 2^{nd} ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ) ) 
15 
14

sbcbidv 
⊢ ( 𝑘 = 𝐾 → ( [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^{nd} ‘ 𝑥 ) = ( 0_{g} ‘ 𝑢 ) , ( 0_{g} ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^{nd} ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑢 ) ( 2^{nd} ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ↔ [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^{nd} ‘ 𝑥 ) = ( 0_{g} ‘ 𝑢 ) , ( 0_{g} ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^{nd} ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑢 ) ( 2^{nd} ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ) ) 
16 
15

sbcbidv 
⊢ ( 𝑘 = 𝐾 → ( [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^{nd} ‘ 𝑥 ) = ( 0_{g} ‘ 𝑢 ) , ( 0_{g} ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^{nd} ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑢 ) ( 2^{nd} ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ↔ [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^{nd} ‘ 𝑥 ) = ( 0_{g} ‘ 𝑢 ) , ( 0_{g} ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^{nd} ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑢 ) ( 2^{nd} ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ) ) 
17 
6 16

sbceqbid 
⊢ ( 𝑘 = 𝐾 → ( [ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^{nd} ‘ 𝑥 ) = ( 0_{g} ‘ 𝑢 ) , ( 0_{g} ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^{nd} ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑢 ) ( 2^{nd} ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ↔ [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^{nd} ‘ 𝑥 ) = ( 0_{g} ‘ 𝑢 ) , ( 0_{g} ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^{nd} ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑢 ) ( 2^{nd} ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ) ) 
18 
17

abbidv 
⊢ ( 𝑘 = 𝐾 → { 𝑎 ∣ [ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^{nd} ‘ 𝑥 ) = ( 0_{g} ‘ 𝑢 ) , ( 0_{g} ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^{nd} ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑢 ) ( 2^{nd} ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑐 ) ℎ ) } ) ) ) ) ) } = { 𝑎 ∣ [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^{nd} ‘ 𝑥 ) = ( 0_{g} ‘ 𝑢 ) , ( 0_{g} ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^{nd} ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑢 ) ( 2^{nd} ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑐 ) ℎ ) } ) ) ) ) ) } ) 
19 
4 18

mpteq12dv 
⊢ ( 𝑘 = 𝐾 → ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑎 ∣ [ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^{nd} ‘ 𝑥 ) = ( 0_{g} ‘ 𝑢 ) , ( 0_{g} ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^{nd} ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑢 ) ( 2^{nd} ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑐 ) ℎ ) } ) ) ) ) ) } ) = ( 𝑤 ∈ 𝐻 ↦ { 𝑎 ∣ [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^{nd} ‘ 𝑥 ) = ( 0_{g} ‘ 𝑢 ) , ( 0_{g} ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^{nd} ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑢 ) ( 2^{nd} ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑐 ) ℎ ) } ) ) ) ) ) } ) ) 
20 

dfhdmap1 
⊢ HDMap1 = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑎 ∣ [ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^{nd} ‘ 𝑥 ) = ( 0_{g} ‘ 𝑢 ) , ( 0_{g} ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^{nd} ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑢 ) ( 2^{nd} ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑐 ) ℎ ) } ) ) ) ) ) } ) ) 
21 
19 20 1

mptfvmpt 
⊢ ( 𝐾 ∈ V → ( HDMap1 ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ { 𝑎 ∣ [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^{nd} ‘ 𝑥 ) = ( 0_{g} ‘ 𝑢 ) , ( 0_{g} ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^{nd} ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑢 ) ( 2^{nd} ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑐 ) ℎ ) } ) ) ) ) ) } ) ) 
22 
2 21

syl 
⊢ ( 𝐾 ∈ 𝑋 → ( HDMap1 ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ { 𝑎 ∣ [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^{nd} ‘ 𝑥 ) = ( 0_{g} ‘ 𝑢 ) , ( 0_{g} ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^{nd} ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑢 ) ( 2^{nd} ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) ( _{g} ‘ 𝑐 ) ℎ ) } ) ) ) ) ) } ) ) 