# Metamath Proof Explorer

## Theorem hvmaplkr

Description: Kernel of the vector to functional map. TODO: make this become lcfrlem11 . (Contributed by NM, 29-Mar-2015)

Ref Expression
Hypotheses hvmaplkr.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
hvmaplkr.o ${⊢}{O}=\mathrm{ocH}\left({K}\right)\left({W}\right)$
hvmaplkr.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
hvmaplkr.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
hvmaplkr.z
hvmaplkr.l ${⊢}{L}=\mathrm{LKer}\left({U}\right)$
hvmaplkr.m ${⊢}{M}=\mathrm{HVMap}\left({K}\right)\left({W}\right)$
hvmaplkr.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
hvmaplkr.x
Assertion hvmaplkr ${⊢}{\phi }\to {L}\left({M}\left({X}\right)\right)={O}\left(\left\{{X}\right\}\right)$

### Proof

Step Hyp Ref Expression
1 hvmaplkr.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 hvmaplkr.o ${⊢}{O}=\mathrm{ocH}\left({K}\right)\left({W}\right)$
3 hvmaplkr.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
4 hvmaplkr.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
5 hvmaplkr.z
6 hvmaplkr.l ${⊢}{L}=\mathrm{LKer}\left({U}\right)$
7 hvmaplkr.m ${⊢}{M}=\mathrm{HVMap}\left({K}\right)\left({W}\right)$
8 hvmaplkr.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
9 hvmaplkr.x
10 eqid ${⊢}{+}_{{U}}={+}_{{U}}$
11 eqid ${⊢}{\cdot }_{{U}}={\cdot }_{{U}}$
12 eqid ${⊢}\mathrm{Scalar}\left({U}\right)=\mathrm{Scalar}\left({U}\right)$
13 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({U}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({U}\right)}$
14 1 3 2 4 10 11 5 12 13 7 8 hvmapfval
15 14 fveq1d
16 15 fveq2d
17 eqid ${⊢}\mathrm{LFnl}\left({U}\right)=\mathrm{LFnl}\left({U}\right)$
18 eqid ${⊢}\mathrm{LDual}\left({U}\right)=\mathrm{LDual}\left({U}\right)$
19 eqid ${⊢}{0}_{\mathrm{LDual}\left({U}\right)}={0}_{\mathrm{LDual}\left({U}\right)}$
20 eqid ${⊢}\left\{{f}\in \mathrm{LFnl}\left({U}\right)|{O}\left({O}\left({L}\left({f}\right)\right)\right)={L}\left({f}\right)\right\}=\left\{{f}\in \mathrm{LFnl}\left({U}\right)|{O}\left({O}\left({L}\left({f}\right)\right)\right)={L}\left({f}\right)\right\}$
21 eqid
22 1 2 3 4 10 11 12 13 5 17 6 18 19 20 21 8 9 lcfrlem11
23 16 22 eqtrd ${⊢}{\phi }\to {L}\left({M}\left({X}\right)\right)={O}\left(\left\{{X}\right\}\right)$