Metamath Proof Explorer


Theorem hvmapval

Description: Value of 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 ( 𝜑 → ( 𝐾𝐴𝑊𝐻 ) )
hvmapval.x ( 𝜑𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
Assertion hvmapval ( 𝜑 → ( 𝑀𝑋 ) = ( 𝑣𝑉 ↦ ( 𝑗𝑅𝑡 ∈ ( 𝑂 ‘ { 𝑋 } ) 𝑣 = ( 𝑡 + ( 𝑗 · 𝑋 ) ) ) ) )

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 hvmapval.x ( 𝜑𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
13 1 2 3 4 5 6 7 8 9 10 11 hvmapfval ( 𝜑𝑀 = ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑣𝑉 ↦ ( 𝑗𝑅𝑡 ∈ ( 𝑂 ‘ { 𝑥 } ) 𝑣 = ( 𝑡 + ( 𝑗 · 𝑥 ) ) ) ) ) )
14 13 fveq1d ( 𝜑 → ( 𝑀𝑋 ) = ( ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑣𝑉 ↦ ( 𝑗𝑅𝑡 ∈ ( 𝑂 ‘ { 𝑥 } ) 𝑣 = ( 𝑡 + ( 𝑗 · 𝑥 ) ) ) ) ) ‘ 𝑋 ) )
15 4 fvexi 𝑉 ∈ V
16 15 mptex ( 𝑣𝑉 ↦ ( 𝑗𝑅𝑡 ∈ ( 𝑂 ‘ { 𝑋 } ) 𝑣 = ( 𝑡 + ( 𝑗 · 𝑋 ) ) ) ) ∈ V
17 sneq ( 𝑥 = 𝑋 → { 𝑥 } = { 𝑋 } )
18 17 fveq2d ( 𝑥 = 𝑋 → ( 𝑂 ‘ { 𝑥 } ) = ( 𝑂 ‘ { 𝑋 } ) )
19 oveq2 ( 𝑥 = 𝑋 → ( 𝑗 · 𝑥 ) = ( 𝑗 · 𝑋 ) )
20 19 oveq2d ( 𝑥 = 𝑋 → ( 𝑡 + ( 𝑗 · 𝑥 ) ) = ( 𝑡 + ( 𝑗 · 𝑋 ) ) )
21 20 eqeq2d ( 𝑥 = 𝑋 → ( 𝑣 = ( 𝑡 + ( 𝑗 · 𝑥 ) ) ↔ 𝑣 = ( 𝑡 + ( 𝑗 · 𝑋 ) ) ) )
22 18 21 rexeqbidv ( 𝑥 = 𝑋 → ( ∃ 𝑡 ∈ ( 𝑂 ‘ { 𝑥 } ) 𝑣 = ( 𝑡 + ( 𝑗 · 𝑥 ) ) ↔ ∃ 𝑡 ∈ ( 𝑂 ‘ { 𝑋 } ) 𝑣 = ( 𝑡 + ( 𝑗 · 𝑋 ) ) ) )
23 22 riotabidv ( 𝑥 = 𝑋 → ( 𝑗𝑅𝑡 ∈ ( 𝑂 ‘ { 𝑥 } ) 𝑣 = ( 𝑡 + ( 𝑗 · 𝑥 ) ) ) = ( 𝑗𝑅𝑡 ∈ ( 𝑂 ‘ { 𝑋 } ) 𝑣 = ( 𝑡 + ( 𝑗 · 𝑋 ) ) ) )
24 23 mpteq2dv ( 𝑥 = 𝑋 → ( 𝑣𝑉 ↦ ( 𝑗𝑅𝑡 ∈ ( 𝑂 ‘ { 𝑥 } ) 𝑣 = ( 𝑡 + ( 𝑗 · 𝑥 ) ) ) ) = ( 𝑣𝑉 ↦ ( 𝑗𝑅𝑡 ∈ ( 𝑂 ‘ { 𝑋 } ) 𝑣 = ( 𝑡 + ( 𝑗 · 𝑋 ) ) ) ) )
25 eqid ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑣𝑉 ↦ ( 𝑗𝑅𝑡 ∈ ( 𝑂 ‘ { 𝑥 } ) 𝑣 = ( 𝑡 + ( 𝑗 · 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑣𝑉 ↦ ( 𝑗𝑅𝑡 ∈ ( 𝑂 ‘ { 𝑥 } ) 𝑣 = ( 𝑡 + ( 𝑗 · 𝑥 ) ) ) ) )
26 24 25 fvmptg ( ( 𝑋 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑣𝑉 ↦ ( 𝑗𝑅𝑡 ∈ ( 𝑂 ‘ { 𝑋 } ) 𝑣 = ( 𝑡 + ( 𝑗 · 𝑋 ) ) ) ) ∈ V ) → ( ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑣𝑉 ↦ ( 𝑗𝑅𝑡 ∈ ( 𝑂 ‘ { 𝑥 } ) 𝑣 = ( 𝑡 + ( 𝑗 · 𝑥 ) ) ) ) ) ‘ 𝑋 ) = ( 𝑣𝑉 ↦ ( 𝑗𝑅𝑡 ∈ ( 𝑂 ‘ { 𝑋 } ) 𝑣 = ( 𝑡 + ( 𝑗 · 𝑋 ) ) ) ) )
27 12 16 26 sylancl ( 𝜑 → ( ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑣𝑉 ↦ ( 𝑗𝑅𝑡 ∈ ( 𝑂 ‘ { 𝑥 } ) 𝑣 = ( 𝑡 + ( 𝑗 · 𝑥 ) ) ) ) ) ‘ 𝑋 ) = ( 𝑣𝑉 ↦ ( 𝑗𝑅𝑡 ∈ ( 𝑂 ‘ { 𝑋 } ) 𝑣 = ( 𝑡 + ( 𝑗 · 𝑋 ) ) ) ) )
28 14 27 eqtrd ( 𝜑 → ( 𝑀𝑋 ) = ( 𝑣𝑉 ↦ ( 𝑗𝑅𝑡 ∈ ( 𝑂 ‘ { 𝑋 } ) 𝑣 = ( 𝑡 + ( 𝑗 · 𝑋 ) ) ) ) )