Metamath Proof Explorer


Theorem hvmapidN

Description: The value of the vector to functional map, at the vector, is one. (Contributed by NM, 23-Mar-2015) (New usage is discouraged.)

Ref Expression
Hypotheses hvmapid.h 𝐻 = ( LHyp ‘ 𝐾 )
hvmapid.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hvmapid.v 𝑉 = ( Base ‘ 𝑈 )
hvmapid.z 0 = ( 0g𝑈 )
hvmapid.s 𝑆 = ( Scalar ‘ 𝑈 )
hvmapid.i 1 = ( 1r𝑆 )
hvmapid.m 𝑀 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
hvmapid.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
hvmapid.x ( 𝜑𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
Assertion hvmapidN ( 𝜑 → ( ( 𝑀𝑋 ) ‘ 𝑋 ) = 1 )

Proof

Step Hyp Ref Expression
1 hvmapid.h 𝐻 = ( LHyp ‘ 𝐾 )
2 hvmapid.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hvmapid.v 𝑉 = ( Base ‘ 𝑈 )
4 hvmapid.z 0 = ( 0g𝑈 )
5 hvmapid.s 𝑆 = ( Scalar ‘ 𝑈 )
6 hvmapid.i 1 = ( 1r𝑆 )
7 hvmapid.m 𝑀 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
8 hvmapid.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
9 hvmapid.x ( 𝜑𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
10 eqid ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
11 eqid ( +g𝑈 ) = ( +g𝑈 )
12 eqid ( ·𝑠𝑈 ) = ( ·𝑠𝑈 )
13 eqid ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
14 1 2 10 3 11 12 4 5 13 7 8 9 hvmapval ( 𝜑 → ( 𝑀𝑋 ) = ( 𝑣𝑉 ↦ ( 𝑗 ∈ ( Base ‘ 𝑆 ) ∃ 𝑡 ∈ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑋 } ) 𝑣 = ( 𝑡 ( +g𝑈 ) ( 𝑗 ( ·𝑠𝑈 ) 𝑋 ) ) ) ) )
15 14 fveq1d ( 𝜑 → ( ( 𝑀𝑋 ) ‘ 𝑋 ) = ( ( 𝑣𝑉 ↦ ( 𝑗 ∈ ( Base ‘ 𝑆 ) ∃ 𝑡 ∈ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑋 } ) 𝑣 = ( 𝑡 ( +g𝑈 ) ( 𝑗 ( ·𝑠𝑈 ) 𝑋 ) ) ) ) ‘ 𝑋 ) )
16 eqid ( 𝑣𝑉 ↦ ( 𝑗 ∈ ( Base ‘ 𝑆 ) ∃ 𝑡 ∈ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑋 } ) 𝑣 = ( 𝑡 ( +g𝑈 ) ( 𝑗 ( ·𝑠𝑈 ) 𝑋 ) ) ) ) = ( 𝑣𝑉 ↦ ( 𝑗 ∈ ( Base ‘ 𝑆 ) ∃ 𝑡 ∈ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑋 } ) 𝑣 = ( 𝑡 ( +g𝑈 ) ( 𝑗 ( ·𝑠𝑈 ) 𝑋 ) ) ) )
17 1 10 2 3 11 12 4 5 13 6 8 9 16 dochfl1 ( 𝜑 → ( ( 𝑣𝑉 ↦ ( 𝑗 ∈ ( Base ‘ 𝑆 ) ∃ 𝑡 ∈ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑋 } ) 𝑣 = ( 𝑡 ( +g𝑈 ) ( 𝑗 ( ·𝑠𝑈 ) 𝑋 ) ) ) ) ‘ 𝑋 ) = 1 )
18 15 17 eqtrd ( 𝜑 → ( ( 𝑀𝑋 ) ‘ 𝑋 ) = 1 )