Metamath Proof Explorer


Theorem hdmap1ffval

Description: Preliminary map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 14-May-2015)

Ref Expression
Hypothesis hdmap1val.h 𝐻 = ( LHyp ‘ 𝐾 )
Assertion hdmap1ffval ( 𝐾𝑋 → ( HDMap1 ‘ 𝐾 ) = ( 𝑤𝐻 ↦ { 𝑎[ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2nd𝑥 ) = ( 0g𝑢 ) , ( 0g𝑐 ) , ( 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝑗 ‘ { } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( -g𝑢 ) ( 2nd𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) ( -g𝑐 ) ) } ) ) ) ) ) } ) )

Proof

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 ( ( 2nd𝑥 ) = ( 0g𝑢 ) , ( 0g𝑐 ) , ( 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝑗 ‘ { } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( -g𝑢 ) ( 2nd𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) ( -g𝑐 ) ) } ) ) ) ) ) ↔ [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2nd𝑥 ) = ( 0g𝑢 ) , ( 0g𝑐 ) , ( 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝑗 ‘ { } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( -g𝑢 ) ( 2nd𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) ( -g𝑐 ) ) } ) ) ) ) ) ) )
12 11 sbcbidv ( 𝑘 = 𝐾 → ( [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2nd𝑥 ) = ( 0g𝑢 ) , ( 0g𝑐 ) , ( 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝑗 ‘ { } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( -g𝑢 ) ( 2nd𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) ( -g𝑐 ) ) } ) ) ) ) ) ↔ [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2nd𝑥 ) = ( 0g𝑢 ) , ( 0g𝑐 ) , ( 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝑗 ‘ { } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( -g𝑢 ) ( 2nd𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) ( -g𝑐 ) ) } ) ) ) ) ) ) )
13 12 sbcbidv ( 𝑘 = 𝐾 → ( [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2nd𝑥 ) = ( 0g𝑢 ) , ( 0g𝑐 ) , ( 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝑗 ‘ { } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( -g𝑢 ) ( 2nd𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) ( -g𝑐 ) ) } ) ) ) ) ) ↔ [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2nd𝑥 ) = ( 0g𝑢 ) , ( 0g𝑐 ) , ( 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝑗 ‘ { } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( -g𝑢 ) ( 2nd𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) ( -g𝑐 ) ) } ) ) ) ) ) ) )
14 8 13 sbceqbid ( 𝑘 = 𝐾 → ( [ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2nd𝑥 ) = ( 0g𝑢 ) , ( 0g𝑐 ) , ( 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝑗 ‘ { } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( -g𝑢 ) ( 2nd𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) ( -g𝑐 ) ) } ) ) ) ) ) ↔ [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2nd𝑥 ) = ( 0g𝑢 ) , ( 0g𝑐 ) , ( 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝑗 ‘ { } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( -g𝑢 ) ( 2nd𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) ( -g𝑐 ) ) } ) ) ) ) ) ) )
15 14 sbcbidv ( 𝑘 = 𝐾 → ( [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2nd𝑥 ) = ( 0g𝑢 ) , ( 0g𝑐 ) , ( 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝑗 ‘ { } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( -g𝑢 ) ( 2nd𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) ( -g𝑐 ) ) } ) ) ) ) ) ↔ [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2nd𝑥 ) = ( 0g𝑢 ) , ( 0g𝑐 ) , ( 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝑗 ‘ { } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( -g𝑢 ) ( 2nd𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) ( -g𝑐 ) ) } ) ) ) ) ) ) )
16 15 sbcbidv ( 𝑘 = 𝐾 → ( [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2nd𝑥 ) = ( 0g𝑢 ) , ( 0g𝑐 ) , ( 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝑗 ‘ { } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( -g𝑢 ) ( 2nd𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) ( -g𝑐 ) ) } ) ) ) ) ) ↔ [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2nd𝑥 ) = ( 0g𝑢 ) , ( 0g𝑐 ) , ( 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝑗 ‘ { } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( -g𝑢 ) ( 2nd𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) ( -g𝑐 ) ) } ) ) ) ) ) ) )
17 6 16 sbceqbid ( 𝑘 = 𝐾 → ( [ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2nd𝑥 ) = ( 0g𝑢 ) , ( 0g𝑐 ) , ( 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝑗 ‘ { } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( -g𝑢 ) ( 2nd𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) ( -g𝑐 ) ) } ) ) ) ) ) ↔ [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2nd𝑥 ) = ( 0g𝑢 ) , ( 0g𝑐 ) , ( 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝑗 ‘ { } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( -g𝑢 ) ( 2nd𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) ( -g𝑐 ) ) } ) ) ) ) ) ) )
18 17 abbidv ( 𝑘 = 𝐾 → { 𝑎[ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2nd𝑥 ) = ( 0g𝑢 ) , ( 0g𝑐 ) , ( 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝑗 ‘ { } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( -g𝑢 ) ( 2nd𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) ( -g𝑐 ) ) } ) ) ) ) ) } = { 𝑎[ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2nd𝑥 ) = ( 0g𝑢 ) , ( 0g𝑐 ) , ( 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝑗 ‘ { } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( -g𝑢 ) ( 2nd𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) ( -g𝑐 ) ) } ) ) ) ) ) } )
19 4 18 mpteq12dv ( 𝑘 = 𝐾 → ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑎[ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2nd𝑥 ) = ( 0g𝑢 ) , ( 0g𝑐 ) , ( 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝑗 ‘ { } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( -g𝑢 ) ( 2nd𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) ( -g𝑐 ) ) } ) ) ) ) ) } ) = ( 𝑤𝐻 ↦ { 𝑎[ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2nd𝑥 ) = ( 0g𝑢 ) , ( 0g𝑐 ) , ( 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝑗 ‘ { } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( -g𝑢 ) ( 2nd𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) ( -g𝑐 ) ) } ) ) ) ) ) } ) )
20 df-hdmap1 HDMap1 = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑎[ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝑘 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝑘 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2nd𝑥 ) = ( 0g𝑢 ) , ( 0g𝑐 ) , ( 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝑗 ‘ { } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( -g𝑢 ) ( 2nd𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) ( -g𝑐 ) ) } ) ) ) ) ) } ) )
21 19 20 1 mptfvmpt ( 𝐾 ∈ V → ( HDMap1 ‘ 𝐾 ) = ( 𝑤𝐻 ↦ { 𝑎[ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2nd𝑥 ) = ( 0g𝑢 ) , ( 0g𝑐 ) , ( 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝑗 ‘ { } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( -g𝑢 ) ( 2nd𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) ( -g𝑐 ) ) } ) ) ) ) ) } ) )
22 2 21 syl ( 𝐾𝑋 → ( HDMap1 ‘ 𝐾 ) = ( 𝑤𝐻 ↦ { 𝑎[ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2nd𝑥 ) = ( 0g𝑢 ) , ( 0g𝑐 ) , ( 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝑗 ‘ { } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( -g𝑢 ) ( 2nd𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) ( -g𝑐 ) ) } ) ) ) ) ) } ) )