Metamath Proof Explorer

Theorem hgmapfval

Description: Map from the scalar division ring of the vector space to the scalar division ring of its closed kernel dual. (Contributed by NM, 25-Mar-2015)

Ref Expression
Hypotheses hgmapval.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
hgmapfval.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hgmapfval.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
hgmapfval.t ⊢ · = ( ·𝑠 ‘ 𝑈 )
hgmapfval.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
hgmapfval.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
hgmapfval.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
hgmapfval.s ⊢ ∙ = ( ·𝑠 ‘ 𝐶 )
hgmapfval.m ⊢ 𝑀 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hgmapfval.i ⊢ 𝐼 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
hgmapfval.k ⊢ ( 𝜑 → ( 𝐾 ∈ 𝑌 ∧ 𝑊 ∈ 𝐻 ) )
Assertion hgmapfval ( 𝜑 → 𝐼 = ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 hgmapval.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 hgmapfval.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hgmapfval.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 hgmapfval.t ⊢ · = ( ·𝑠 ‘ 𝑈 )
5 hgmapfval.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
6 hgmapfval.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
7 hgmapfval.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
8 hgmapfval.s ⊢ ∙ = ( ·𝑠 ‘ 𝐶 )
9 hgmapfval.m ⊢ 𝑀 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
10 hgmapfval.i ⊢ 𝐼 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
11 hgmapfval.k ⊢ ( 𝜑 → ( 𝐾 ∈ 𝑌 ∧ 𝑊 ∈ 𝐻 ) )
12 1 hgmapffval ⊢ ( 𝐾 ∈ 𝑌 → ( HGMap ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ { 𝑎 ∣ [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ ( Scalar ‘ 𝑢 ) ) / 𝑏 ] [ ( ( HDMap ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) } ) )
13 12 fveq1d ⊢ ( 𝐾 ∈ 𝑌 → ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) = ( ( 𝑤 ∈ 𝐻 ↦ { 𝑎 ∣ [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ ( Scalar ‘ 𝑢 ) ) / 𝑏 ] [ ( ( HDMap ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) } ) ‘ 𝑊 ) )
14 10 13 syl5eq ⊢ ( 𝐾 ∈ 𝑌 → 𝐼 = ( ( 𝑤 ∈ 𝐻 ↦ { 𝑎 ∣ [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ ( Scalar ‘ 𝑢 ) ) / 𝑏 ] [ ( ( HDMap ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) } ) ‘ 𝑊 ) )
15 fveq2 ⊢ ( 𝑤 = 𝑊 → ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
16 15 2 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) = 𝑈 )
17 fveq2 ⊢ ( 𝑤 = 𝑊 → ( ( HDMap ‘ 𝐾 ) ‘ 𝑤 ) = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) )
18 17 9 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( ( HDMap ‘ 𝐾 ) ‘ 𝑤 ) = 𝑀 )
19 2fveq3 ⊢ ( 𝑤 = 𝑊 → ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) = ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
20 19 oveqd ⊢ ( 𝑤 = 𝑊 → ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) )
21 20 eqeq2d ⊢ ( 𝑤 = 𝑊 → ( ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ↔ ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) ) )
22 21 ralbidv ⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ↔ ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) ) )
23 22 riotabidv ⊢ ( 𝑤 = 𝑊 → ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) = ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) ) )
24 23 mpteq2dv ⊢ ( 𝑤 = 𝑊 → ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) = ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) )
25 24 eleq2d ⊢ ( 𝑤 = 𝑊 → ( 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) ↔ 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) ) )
26 18 25 sbceqbid ⊢ ( 𝑤 = 𝑊 → ( [ ( ( HDMap ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) ↔ [ 𝑀 / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) ) )
27 26 sbcbidv ⊢ ( 𝑤 = 𝑊 → ( [ ( Base ‘ ( Scalar ‘ 𝑢 ) ) / 𝑏 ] [ ( ( HDMap ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) ↔ [ ( Base ‘ ( Scalar ‘ 𝑢 ) ) / 𝑏 ] [ 𝑀 / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) ) )
28 16 27 sbceqbid ⊢ ( 𝑤 = 𝑊 → ( [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ ( Scalar ‘ 𝑢 ) ) / 𝑏 ] [ ( ( HDMap ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) ↔ [ 𝑈 / 𝑢 ] [ ( Base ‘ ( Scalar ‘ 𝑢 ) ) / 𝑏 ] [ 𝑀 / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) ) )
29 2 fvexi ⊢ 𝑈 ∈ V
30 fvex ⊢ ( Base ‘ ( Scalar ‘ 𝑢 ) ) ∈ V
31 9 fvexi ⊢ 𝑀 ∈ V
32 simp2 ⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = ( Base ‘ ( Scalar ‘ 𝑢 ) ) ∧ 𝑚 = 𝑀 ) → 𝑏 = ( Base ‘ ( Scalar ‘ 𝑢 ) ) )
33 simp1 ⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = ( Base ‘ ( Scalar ‘ 𝑢 ) ) ∧ 𝑚 = 𝑀 ) → 𝑢 = 𝑈 )
34 33 fveq2d ⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = ( Base ‘ ( Scalar ‘ 𝑢 ) ) ∧ 𝑚 = 𝑀 ) → ( Scalar ‘ 𝑢 ) = ( Scalar ‘ 𝑈 ) )
35 34 5 eqtr4di ⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = ( Base ‘ ( Scalar ‘ 𝑢 ) ) ∧ 𝑚 = 𝑀 ) → ( Scalar ‘ 𝑢 ) = 𝑅 )
36 35 fveq2d ⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = ( Base ‘ ( Scalar ‘ 𝑢 ) ) ∧ 𝑚 = 𝑀 ) → ( Base ‘ ( Scalar ‘ 𝑢 ) ) = ( Base ‘ 𝑅 ) )
37 32 36 eqtrd ⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = ( Base ‘ ( Scalar ‘ 𝑢 ) ) ∧ 𝑚 = 𝑀 ) → 𝑏 = ( Base ‘ 𝑅 ) )
38 37 6 eqtr4di ⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = ( Base ‘ ( Scalar ‘ 𝑢 ) ) ∧ 𝑚 = 𝑀 ) → 𝑏 = 𝐵 )
39 simp2 ⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → 𝑏 = 𝐵 )
40 simp1 ⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → 𝑢 = 𝑈 )
41 40 fveq2d ⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( Base ‘ 𝑢 ) = ( Base ‘ 𝑈 ) )
42 41 3 eqtr4di ⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( Base ‘ 𝑢 ) = 𝑉 )
43 simp3 ⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → 𝑚 = 𝑀 )
44 40 fveq2d ⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( ·𝑠 ‘ 𝑢 ) = ( ·𝑠 ‘ 𝑈 ) )
45 44 4 eqtr4di ⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( ·𝑠 ‘ 𝑢 ) = · )
46 45 oveqd ⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) = ( 𝑥 · 𝑣 ) )
47 43 46 fveq12d ⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) )
48 eqidd ⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
49 48 7 eqtr4di ⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) = 𝐶 )
50 49 fveq2d ⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ·𝑠 ‘ 𝐶 ) )
51 50 8 eqtr4di ⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ∙ )
52 eqidd ⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → 𝑦 = 𝑦 )
53 43 fveq1d ⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( 𝑚 ‘ 𝑣 ) = ( 𝑀 ‘ 𝑣 ) )
54 51 52 53 oveq123d ⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) )
55 47 54 eqeq12d ⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) ↔ ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) )
56 42 55 raleqbidv ⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) ↔ ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) )
57 39 56 riotaeqbidv ⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) ) = ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) )
58 39 57 mpteq12dv ⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) = ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) ) )
59 58 eleq2d ⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = 𝐵 ∧ 𝑚 = 𝑀 ) → ( 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) ↔ 𝑎 ∈ ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) ) ) )
60 38 59 syld3an2 ⊢ ( ( 𝑢 = 𝑈 ∧ 𝑏 = ( Base ‘ ( Scalar ‘ 𝑢 ) ) ∧ 𝑚 = 𝑀 ) → ( 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) ↔ 𝑎 ∈ ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) ) ) )
61 29 30 31 60 sbc3ie ⊢ ( [ 𝑈 / 𝑢 ] [ ( Base ‘ ( Scalar ‘ 𝑢 ) ) / 𝑏 ] [ 𝑀 / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) ↔ 𝑎 ∈ ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) ) )
62 28 61 bitrdi ⊢ ( 𝑤 = 𝑊 → ( [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ ( Scalar ‘ 𝑢 ) ) / 𝑏 ] [ ( ( HDMap ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) ↔ 𝑎 ∈ ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) ) ) )
63 62 abbi1dv ⊢ ( 𝑤 = 𝑊 → { 𝑎 ∣ [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ ( Scalar ‘ 𝑢 ) ) / 𝑏 ] [ ( ( HDMap ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) } = ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) ) )
64 eqid ⊢ ( 𝑤 ∈ 𝐻 ↦ { 𝑎 ∣ [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ ( Scalar ‘ 𝑢 ) ) / 𝑏 ] [ ( ( HDMap ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) } ) = ( 𝑤 ∈ 𝐻 ↦ { 𝑎 ∣ [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ ( Scalar ‘ 𝑢 ) ) / 𝑏 ] [ ( ( HDMap ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) } )
65 63 64 6 mptfvmpt ⊢ ( 𝑊 ∈ 𝐻 → ( ( 𝑤 ∈ 𝐻 ↦ { 𝑎 ∣ [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ ( Scalar ‘ 𝑢 ) ) / 𝑏 ] [ ( ( HDMap ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑦 ∈ 𝑏 ∀ 𝑣 ∈ ( Base ‘ 𝑢 ) ( 𝑚 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑢 ) 𝑣 ) ) = ( 𝑦 ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑚 ‘ 𝑣 ) ) ) ) } ) ‘ 𝑊 ) = ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) ) )
66 14 65 sylan9eq ⊢ ( ( 𝐾 ∈ 𝑌 ∧ 𝑊 ∈ 𝐻 ) → 𝐼 = ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) ) )
67 11 66 syl ⊢ ( 𝜑 → 𝐼 = ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑥 · 𝑣 ) ) = ( 𝑦 ∙ ( 𝑀 ‘ 𝑣 ) ) ) ) )