# Metamath Proof Explorer

## Theorem hdmapf1oN

Description: Part 12 in Baer p. 49. The map from vectors to functionals with closed kernels maps one-to-one onto. Combined with hdmapadd , this shows the map is an automorphism from the additive group of vectors to the additive group of functionals with closed kernels. (Contributed by NM, 30-May-2015) (New usage is discouraged.)

Ref Expression
Hypotheses hdmapf1o.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
hdmapf1o.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
hdmapf1o.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
hdmapf1o.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
hdmapf1o.d ${⊢}{D}={\mathrm{Base}}_{{C}}$
hdmapf1o.s ${⊢}{S}=\mathrm{HDMap}\left({K}\right)\left({W}\right)$
hdmapf1o.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
Assertion hdmapf1oN ${⊢}{\phi }\to {S}:{V}\underset{1-1 onto}{⟶}{D}$

### Proof

Step Hyp Ref Expression
1 hdmapf1o.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 hdmapf1o.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 hdmapf1o.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
4 hdmapf1o.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
5 hdmapf1o.d ${⊢}{D}={\mathrm{Base}}_{{C}}$
6 hdmapf1o.s ${⊢}{S}=\mathrm{HDMap}\left({K}\right)\left({W}\right)$
7 hdmapf1o.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
8 1 2 3 6 7 hdmapfnN ${⊢}{\phi }\to {S}Fn{V}$
9 1 4 5 6 7 hdmaprnN ${⊢}{\phi }\to \mathrm{ran}{S}={D}$
10 7 adantr ${⊢}\left({\phi }\wedge \left({x}\in {V}\wedge {y}\in {V}\right)\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
11 simprl ${⊢}\left({\phi }\wedge \left({x}\in {V}\wedge {y}\in {V}\right)\right)\to {x}\in {V}$
12 simprr ${⊢}\left({\phi }\wedge \left({x}\in {V}\wedge {y}\in {V}\right)\right)\to {y}\in {V}$
13 1 2 3 6 10 11 12 hdmap11 ${⊢}\left({\phi }\wedge \left({x}\in {V}\wedge {y}\in {V}\right)\right)\to \left({S}\left({x}\right)={S}\left({y}\right)↔{x}={y}\right)$
14 13 biimpd ${⊢}\left({\phi }\wedge \left({x}\in {V}\wedge {y}\in {V}\right)\right)\to \left({S}\left({x}\right)={S}\left({y}\right)\to {x}={y}\right)$
15 14 ralrimivva ${⊢}{\phi }\to \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\forall {y}\in {V}\phantom{\rule{.4em}{0ex}}\left({S}\left({x}\right)={S}\left({y}\right)\to {x}={y}\right)$
16 dff1o6 ${⊢}{S}:{V}\underset{1-1 onto}{⟶}{D}↔\left({S}Fn{V}\wedge \mathrm{ran}{S}={D}\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\forall {y}\in {V}\phantom{\rule{.4em}{0ex}}\left({S}\left({x}\right)={S}\left({y}\right)\to {x}={y}\right)\right)$
17 8 9 15 16 syl3anbrc ${⊢}{\phi }\to {S}:{V}\underset{1-1 onto}{⟶}{D}$