Metamath Proof Explorer


Theorem hvmaplfl

Description: The vector to functional map value is a functional. (Contributed by NM, 28-Mar-2015)

Ref Expression
Hypotheses hvmaplfl.h H=LHypK
hvmaplfl.u U=DVecHKW
hvmaplfl.v V=BaseU
hvmaplfl.z 0˙=0U
hvmaplfl.f F=LFnlU
hvmaplfl.m M=HVMapKW
hvmaplfl.k φKHLWH
hvmaplfl.x φXV0˙
Assertion hvmaplfl φMXF

Proof

Step Hyp Ref Expression
1 hvmaplfl.h H=LHypK
2 hvmaplfl.u U=DVecHKW
3 hvmaplfl.v V=BaseU
4 hvmaplfl.z 0˙=0U
5 hvmaplfl.f F=LFnlU
6 hvmaplfl.m M=HVMapKW
7 hvmaplfl.k φKHLWH
8 hvmaplfl.x φXV0˙
9 eqid LCDualKW=LCDualKW
10 eqid BaseLCDualKW=BaseLCDualKW
11 eqid 0LCDualKW=0LCDualKW
12 1 2 3 4 9 10 11 6 7 8 hvmapcl2 φMXBaseLCDualKW0LCDualKW
13 12 eldifad φMXBaseLCDualKW
14 1 9 10 2 5 7 13 lcdvbaselfl φMXF