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 ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) } ) )

Proof

Step	Hyp	Ref	Expression
1		hdmap1val.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		elex	⊢ ( 𝐾 ∈ 𝑋 → 𝐾 ∈ V )
3		fveq2	⊢ ( 𝑘 = 𝐾 → ( LHyp ‘ 𝑘 ) = ( LHyp ‘ 𝐾 ) )
4	3 1	eqtr4di	⊢ ( 𝑘 = 𝐾 → ( 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		df-hdmap1	⊢ 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 ‘ 𝑐 ) ℎ ) } ) ) ) ) ) } ) )

Metamath Proof Explorer

Theorem hdmap1ffval

Proof