Metamath Proof Explorer

Theorem hvmapfval

Description: Map from nonzero vectors to nonzero functionals in the closed kernel dual space. (Contributed by NM, 23-Mar-2015)

Ref Expression
Hypotheses hvmapval.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
hvmapval.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hvmapval.o ⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
hvmapval.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
hvmapval.p ⊢ + = ( +g ‘ 𝑈 )
hvmapval.t ⊢ · = ( ·𝑠 ‘ 𝑈 )
hvmapval.z ⊢ 0 = ( 0g ‘ 𝑈 )
hvmapval.s ⊢ 𝑆 = ( Scalar ‘ 𝑈 )
hvmapval.r ⊢ 𝑅 = ( Base ‘ 𝑆 )
hvmapval.m ⊢ 𝑀 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
hvmapval.k ⊢ ( 𝜑 → ( 𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻 ) )
Assertion hvmapfval ( 𝜑 → 𝑀 = ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑗 ∈ 𝑅 ∃ 𝑡 ∈ ( 𝑂 ‘ { 𝑥 } ) 𝑣 = ( 𝑡 + ( 𝑗 · 𝑥 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 hvmapval.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 hvmapval.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hvmapval.o ⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
4 hvmapval.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 hvmapval.p ⊢ + = ( +g ‘ 𝑈 )
6 hvmapval.t ⊢ · = ( ·𝑠 ‘ 𝑈 )
7 hvmapval.z ⊢ 0 = ( 0g ‘ 𝑈 )
8 hvmapval.s ⊢ 𝑆 = ( Scalar ‘ 𝑈 )
9 hvmapval.r ⊢ 𝑅 = ( Base ‘ 𝑆 )
10 hvmapval.m ⊢ 𝑀 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
11 hvmapval.k ⊢ ( 𝜑 → ( 𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻 ) )
12 1 hvmapffval ⊢ ( 𝐾 ∈ 𝐴 → ( HVMap ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑥 ∈ ( ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ∖ { ( 0g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) } ) ↦ ( 𝑣 ∈ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ ( ℩ 𝑗 ∈ ( Base ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ) ∃ 𝑡 ∈ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ { 𝑥 } ) 𝑣 = ( 𝑡 ( +g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑗 ( ·𝑠 ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) 𝑥 ) ) ) ) ) ) )
13 12 fveq1d ⊢ ( 𝐾 ∈ 𝐴 → ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) = ( ( 𝑤 ∈ 𝐻 ↦ ( 𝑥 ∈ ( ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ∖ { ( 0g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) } ) ↦ ( 𝑣 ∈ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ ( ℩ 𝑗 ∈ ( Base ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ) ∃ 𝑡 ∈ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ { 𝑥 } ) 𝑣 = ( 𝑡 ( +g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑗 ( ·𝑠 ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) 𝑥 ) ) ) ) ) ) ‘ 𝑊 ) )
14 10 13 eqtrid ⊢ ( 𝐾 ∈ 𝐴 → 𝑀 = ( ( 𝑤 ∈ 𝐻 ↦ ( 𝑥 ∈ ( ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ∖ { ( 0g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) } ) ↦ ( 𝑣 ∈ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ ( ℩ 𝑗 ∈ ( Base ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ) ∃ 𝑡 ∈ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ { 𝑥 } ) 𝑣 = ( 𝑡 ( +g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑗 ( ·𝑠 ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) 𝑥 ) ) ) ) ) ) ‘ 𝑊 ) )
15 fveq2 ⊢ ( 𝑤 = 𝑊 → ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
16 15 2 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) = 𝑈 )
17 16 fveq2d ⊢ ( 𝑤 = 𝑊 → ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) = ( Base ‘ 𝑈 ) )
18 17 4 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) = 𝑉 )
19 16 fveq2d ⊢ ( 𝑤 = 𝑊 → ( 0g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) = ( 0g ‘ 𝑈 ) )
20 19 7 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( 0g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) = 0 )
21 20 sneqd ⊢ ( 𝑤 = 𝑊 → { ( 0g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) } = { 0 } )
22 18 21 difeq12d ⊢ ( 𝑤 = 𝑊 → ( ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ∖ { ( 0g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) } ) = ( 𝑉 ∖ { 0 } ) )
23 16 fveq2d ⊢ ( 𝑤 = 𝑊 → ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) = ( Scalar ‘ 𝑈 ) )
24 23 8 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) = 𝑆 )
25 24 fveq2d ⊢ ( 𝑤 = 𝑊 → ( Base ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ) = ( Base ‘ 𝑆 ) )
26 25 9 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( Base ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ) = 𝑅 )
27 fveq2 ⊢ ( 𝑤 = 𝑊 → ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) )
28 27 3 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) = 𝑂 )
29 28 fveq1d ⊢ ( 𝑤 = 𝑊 → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ { 𝑥 } ) = ( 𝑂 ‘ { 𝑥 } ) )
30 16 fveq2d ⊢ ( 𝑤 = 𝑊 → ( +g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) = ( +g ‘ 𝑈 ) )
31 30 5 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( +g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) = + )
32 eqidd ⊢ ( 𝑤 = 𝑊 → 𝑡 = 𝑡 )
33 16 fveq2d ⊢ ( 𝑤 = 𝑊 → ( ·𝑠 ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) = ( ·𝑠 ‘ 𝑈 ) )
34 33 6 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( ·𝑠 ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) = · )
35 34 oveqd ⊢ ( 𝑤 = 𝑊 → ( 𝑗 ( ·𝑠 ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) 𝑥 ) = ( 𝑗 · 𝑥 ) )
36 31 32 35 oveq123d ⊢ ( 𝑤 = 𝑊 → ( 𝑡 ( +g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑗 ( ·𝑠 ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) 𝑥 ) ) = ( 𝑡 + ( 𝑗 · 𝑥 ) ) )
37 36 eqeq2d ⊢ ( 𝑤 = 𝑊 → ( 𝑣 = ( 𝑡 ( +g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑗 ( ·𝑠 ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) 𝑥 ) ) ↔ 𝑣 = ( 𝑡 + ( 𝑗 · 𝑥 ) ) ) )
38 29 37 rexeqbidv ⊢ ( 𝑤 = 𝑊 → ( ∃ 𝑡 ∈ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ { 𝑥 } ) 𝑣 = ( 𝑡 ( +g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑗 ( ·𝑠 ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) 𝑥 ) ) ↔ ∃ 𝑡 ∈ ( 𝑂 ‘ { 𝑥 } ) 𝑣 = ( 𝑡 + ( 𝑗 · 𝑥 ) ) ) )
39 26 38 riotaeqbidv ⊢ ( 𝑤 = 𝑊 → ( ℩ 𝑗 ∈ ( Base ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ) ∃ 𝑡 ∈ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ { 𝑥 } ) 𝑣 = ( 𝑡 ( +g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑗 ( ·𝑠 ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) 𝑥 ) ) ) = ( ℩ 𝑗 ∈ 𝑅 ∃ 𝑡 ∈ ( 𝑂 ‘ { 𝑥 } ) 𝑣 = ( 𝑡 + ( 𝑗 · 𝑥 ) ) ) )
40 18 39 mpteq12dv ⊢ ( 𝑤 = 𝑊 → ( 𝑣 ∈ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ ( ℩ 𝑗 ∈ ( Base ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ) ∃ 𝑡 ∈ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ { 𝑥 } ) 𝑣 = ( 𝑡 ( +g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑗 ( ·𝑠 ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) 𝑥 ) ) ) ) = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑗 ∈ 𝑅 ∃ 𝑡 ∈ ( 𝑂 ‘ { 𝑥 } ) 𝑣 = ( 𝑡 + ( 𝑗 · 𝑥 ) ) ) ) )
41 22 40 mpteq12dv ⊢ ( 𝑤 = 𝑊 → ( 𝑥 ∈ ( ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ∖ { ( 0g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) } ) ↦ ( 𝑣 ∈ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ ( ℩ 𝑗 ∈ ( Base ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ) ∃ 𝑡 ∈ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ { 𝑥 } ) 𝑣 = ( 𝑡 ( +g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑗 ( ·𝑠 ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑗 ∈ 𝑅 ∃ 𝑡 ∈ ( 𝑂 ‘ { 𝑥 } ) 𝑣 = ( 𝑡 + ( 𝑗 · 𝑥 ) ) ) ) ) )
42 eqid ⊢ ( 𝑤 ∈ 𝐻 ↦ ( 𝑥 ∈ ( ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ∖ { ( 0g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) } ) ↦ ( 𝑣 ∈ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ ( ℩ 𝑗 ∈ ( Base ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ) ∃ 𝑡 ∈ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ { 𝑥 } ) 𝑣 = ( 𝑡 ( +g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑗 ( ·𝑠 ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) 𝑥 ) ) ) ) ) ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑥 ∈ ( ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ∖ { ( 0g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) } ) ↦ ( 𝑣 ∈ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ ( ℩ 𝑗 ∈ ( Base ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ) ∃ 𝑡 ∈ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ { 𝑥 } ) 𝑣 = ( 𝑡 ( +g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑗 ( ·𝑠 ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) 𝑥 ) ) ) ) ) )
43 4 fvexi ⊢ 𝑉 ∈ V
44 43 difexi ⊢ ( 𝑉 ∖ { 0 } ) ∈ V
45 44 mptex ⊢ ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑗 ∈ 𝑅 ∃ 𝑡 ∈ ( 𝑂 ‘ { 𝑥 } ) 𝑣 = ( 𝑡 + ( 𝑗 · 𝑥 ) ) ) ) ) ∈ V
46 41 42 45 fvmpt ⊢ ( 𝑊 ∈ 𝐻 → ( ( 𝑤 ∈ 𝐻 ↦ ( 𝑥 ∈ ( ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ∖ { ( 0g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) } ) ↦ ( 𝑣 ∈ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ ( ℩ 𝑗 ∈ ( Base ‘ ( Scalar ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ) ∃ 𝑡 ∈ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ { 𝑥 } ) 𝑣 = ( 𝑡 ( +g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ( 𝑗 ( ·𝑠 ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) 𝑥 ) ) ) ) ) ) ‘ 𝑊 ) = ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑗 ∈ 𝑅 ∃ 𝑡 ∈ ( 𝑂 ‘ { 𝑥 } ) 𝑣 = ( 𝑡 + ( 𝑗 · 𝑥 ) ) ) ) ) )
47 14 46 sylan9eq ⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻 ) → 𝑀 = ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑗 ∈ 𝑅 ∃ 𝑡 ∈ ( 𝑂 ‘ { 𝑥 } ) 𝑣 = ( 𝑡 + ( 𝑗 · 𝑥 ) ) ) ) ) )
48 11 47 syl ⊢ ( 𝜑 → 𝑀 = ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑗 ∈ 𝑅 ∃ 𝑡 ∈ ( 𝑂 ‘ { 𝑥 } ) 𝑣 = ( 𝑡 + ( 𝑗 · 𝑥 ) ) ) ) ) )