# Metamath Proof Explorer

## Definition df-mapd

Description: Extend class notation with a one-to-one onto ( mapd1o ), order-preserving ( mapdord ) map, called a projectivity (definition of projectivity in Baer p. 40), from subspaces of vector space H to those subspaces of the dual space having functionals with closed kernels. (Contributed by NM, 25-Jan-2015)

Ref Expression
Assertion df-mapd ${⊢}\mathrm{mapd}=\left({k}\in \mathrm{V}⟼\left({w}\in \mathrm{LHyp}\left({k}\right)⟼\left({s}\in \mathrm{LSubSp}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)⟼\left\{{f}\in \mathrm{LFnl}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)|\left(\mathrm{ocH}\left({k}\right)\left({w}\right)\left(\mathrm{ocH}\left({k}\right)\left({w}\right)\left(\mathrm{LKer}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)\left({f}\right)\right)\right)=\mathrm{LKer}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)\left({f}\right)\wedge \mathrm{ocH}\left({k}\right)\left({w}\right)\left(\mathrm{LKer}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)\left({f}\right)\right)\subseteq {s}\right)\right\}\right)\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cmpd ${class}\mathrm{mapd}$
1 vk ${setvar}{k}$
2 cvv ${class}\mathrm{V}$
3 vw ${setvar}{w}$
4 clh ${class}\mathrm{LHyp}$
5 1 cv ${setvar}{k}$
6 5 4 cfv ${class}\mathrm{LHyp}\left({k}\right)$
7 vs ${setvar}{s}$
8 clss ${class}\mathrm{LSubSp}$
9 cdvh ${class}\mathrm{DVecH}$
10 5 9 cfv ${class}\mathrm{DVecH}\left({k}\right)$
11 3 cv ${setvar}{w}$
12 11 10 cfv ${class}\mathrm{DVecH}\left({k}\right)\left({w}\right)$
13 12 8 cfv ${class}\mathrm{LSubSp}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)$
14 vf ${setvar}{f}$
15 clfn ${class}\mathrm{LFnl}$
16 12 15 cfv ${class}\mathrm{LFnl}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)$
17 coch ${class}\mathrm{ocH}$
18 5 17 cfv ${class}\mathrm{ocH}\left({k}\right)$
19 11 18 cfv ${class}\mathrm{ocH}\left({k}\right)\left({w}\right)$
20 clk ${class}\mathrm{LKer}$
21 12 20 cfv ${class}\mathrm{LKer}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)$
22 14 cv ${setvar}{f}$
23 22 21 cfv ${class}\mathrm{LKer}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)\left({f}\right)$
24 23 19 cfv ${class}\mathrm{ocH}\left({k}\right)\left({w}\right)\left(\mathrm{LKer}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)\left({f}\right)\right)$
25 24 19 cfv ${class}\mathrm{ocH}\left({k}\right)\left({w}\right)\left(\mathrm{ocH}\left({k}\right)\left({w}\right)\left(\mathrm{LKer}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)\left({f}\right)\right)\right)$
26 25 23 wceq ${wff}\mathrm{ocH}\left({k}\right)\left({w}\right)\left(\mathrm{ocH}\left({k}\right)\left({w}\right)\left(\mathrm{LKer}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)\left({f}\right)\right)\right)=\mathrm{LKer}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)\left({f}\right)$
27 7 cv ${setvar}{s}$
28 24 27 wss ${wff}\mathrm{ocH}\left({k}\right)\left({w}\right)\left(\mathrm{LKer}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)\left({f}\right)\right)\subseteq {s}$
29 26 28 wa ${wff}\left(\mathrm{ocH}\left({k}\right)\left({w}\right)\left(\mathrm{ocH}\left({k}\right)\left({w}\right)\left(\mathrm{LKer}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)\left({f}\right)\right)\right)=\mathrm{LKer}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)\left({f}\right)\wedge \mathrm{ocH}\left({k}\right)\left({w}\right)\left(\mathrm{LKer}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)\left({f}\right)\right)\subseteq {s}\right)$
30 29 14 16 crab ${class}\left\{{f}\in \mathrm{LFnl}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)|\left(\mathrm{ocH}\left({k}\right)\left({w}\right)\left(\mathrm{ocH}\left({k}\right)\left({w}\right)\left(\mathrm{LKer}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)\left({f}\right)\right)\right)=\mathrm{LKer}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)\left({f}\right)\wedge \mathrm{ocH}\left({k}\right)\left({w}\right)\left(\mathrm{LKer}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)\left({f}\right)\right)\subseteq {s}\right)\right\}$
31 7 13 30 cmpt ${class}\left({s}\in \mathrm{LSubSp}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)⟼\left\{{f}\in \mathrm{LFnl}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)|\left(\mathrm{ocH}\left({k}\right)\left({w}\right)\left(\mathrm{ocH}\left({k}\right)\left({w}\right)\left(\mathrm{LKer}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)\left({f}\right)\right)\right)=\mathrm{LKer}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)\left({f}\right)\wedge \mathrm{ocH}\left({k}\right)\left({w}\right)\left(\mathrm{LKer}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)\left({f}\right)\right)\subseteq {s}\right)\right\}\right)$
32 3 6 31 cmpt ${class}\left({w}\in \mathrm{LHyp}\left({k}\right)⟼\left({s}\in \mathrm{LSubSp}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)⟼\left\{{f}\in \mathrm{LFnl}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)|\left(\mathrm{ocH}\left({k}\right)\left({w}\right)\left(\mathrm{ocH}\left({k}\right)\left({w}\right)\left(\mathrm{LKer}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)\left({f}\right)\right)\right)=\mathrm{LKer}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)\left({f}\right)\wedge \mathrm{ocH}\left({k}\right)\left({w}\right)\left(\mathrm{LKer}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)\left({f}\right)\right)\subseteq {s}\right)\right\}\right)\right)$
33 1 2 32 cmpt ${class}\left({k}\in \mathrm{V}⟼\left({w}\in \mathrm{LHyp}\left({k}\right)⟼\left({s}\in \mathrm{LSubSp}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)⟼\left\{{f}\in \mathrm{LFnl}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)|\left(\mathrm{ocH}\left({k}\right)\left({w}\right)\left(\mathrm{ocH}\left({k}\right)\left({w}\right)\left(\mathrm{LKer}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)\left({f}\right)\right)\right)=\mathrm{LKer}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)\left({f}\right)\wedge \mathrm{ocH}\left({k}\right)\left({w}\right)\left(\mathrm{LKer}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)\left({f}\right)\right)\subseteq {s}\right)\right\}\right)\right)\right)$
34 0 33 wceq ${wff}\mathrm{mapd}=\left({k}\in \mathrm{V}⟼\left({w}\in \mathrm{LHyp}\left({k}\right)⟼\left({s}\in \mathrm{LSubSp}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)⟼\left\{{f}\in \mathrm{LFnl}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)|\left(\mathrm{ocH}\left({k}\right)\left({w}\right)\left(\mathrm{ocH}\left({k}\right)\left({w}\right)\left(\mathrm{LKer}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)\left({f}\right)\right)\right)=\mathrm{LKer}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)\left({f}\right)\wedge \mathrm{ocH}\left({k}\right)\left({w}\right)\left(\mathrm{LKer}\left(\mathrm{DVecH}\left({k}\right)\left({w}\right)\right)\left({f}\right)\right)\subseteq {s}\right)\right\}\right)\right)\right)$