# Metamath Proof Explorer

## Theorem hvmap1o2

Description: The vector to functional map provides a bijection from nonzero vectors V to nonzero functionals with closed kernels C . (Contributed by NM, 27-Mar-2015)

Ref Expression
Hypotheses hvmap1o2.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
hvmap1o2.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
hvmap1o2.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
hvmap1o2.z
hvmap1o2.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
hvmap1o2.f ${⊢}{F}={\mathrm{Base}}_{{C}}$
hvmap1o2.o ${⊢}{O}={0}_{{C}}$
hvmap1o2.m ${⊢}{M}=\mathrm{HVMap}\left({K}\right)\left({W}\right)$
hvmap1o2.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
Assertion hvmap1o2

### Proof

Step Hyp Ref Expression
1 hvmap1o2.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 hvmap1o2.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 hvmap1o2.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
4 hvmap1o2.z
5 hvmap1o2.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
6 hvmap1o2.f ${⊢}{F}={\mathrm{Base}}_{{C}}$
7 hvmap1o2.o ${⊢}{O}={0}_{{C}}$
8 hvmap1o2.m ${⊢}{M}=\mathrm{HVMap}\left({K}\right)\left({W}\right)$
9 hvmap1o2.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
10 eqid ${⊢}\mathrm{ocH}\left({K}\right)\left({W}\right)=\mathrm{ocH}\left({K}\right)\left({W}\right)$
11 eqid ${⊢}\mathrm{LFnl}\left({U}\right)=\mathrm{LFnl}\left({U}\right)$
12 eqid ${⊢}\mathrm{LKer}\left({U}\right)=\mathrm{LKer}\left({U}\right)$
13 eqid ${⊢}\mathrm{LDual}\left({U}\right)=\mathrm{LDual}\left({U}\right)$
14 eqid ${⊢}{0}_{\mathrm{LDual}\left({U}\right)}={0}_{\mathrm{LDual}\left({U}\right)}$
15 eqid ${⊢}\left\{{f}\in \mathrm{LFnl}\left({U}\right)|\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({f}\right)\right)\right)=\mathrm{LKer}\left({U}\right)\left({f}\right)\right\}=\left\{{f}\in \mathrm{LFnl}\left({U}\right)|\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({f}\right)\right)\right)=\mathrm{LKer}\left({U}\right)\left({f}\right)\right\}$
16 1 10 2 3 4 11 12 13 14 15 8 9 hvmap1o
17 1 10 5 6 2 11 12 15 9 lcdvbase ${⊢}{\phi }\to {F}=\left\{{f}\in \mathrm{LFnl}\left({U}\right)|\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({f}\right)\right)\right)=\mathrm{LKer}\left({U}\right)\left({f}\right)\right\}$
18 1 2 13 14 5 7 9 lcd0v2 ${⊢}{\phi }\to {O}={0}_{\mathrm{LDual}\left({U}\right)}$
19 18 sneqd ${⊢}{\phi }\to \left\{{O}\right\}=\left\{{0}_{\mathrm{LDual}\left({U}\right)}\right\}$
20 17 19 difeq12d ${⊢}{\phi }\to {F}\setminus \left\{{O}\right\}=\left\{{f}\in \mathrm{LFnl}\left({U}\right)|\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({f}\right)\right)\right)=\mathrm{LKer}\left({U}\right)\left({f}\right)\right\}\setminus \left\{{0}_{\mathrm{LDual}\left({U}\right)}\right\}$
21 f1oeq3
22 20 21 syl
23 16 22 mpbird