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 ⊢ mapd = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ s ∈ LSubSp ⁡ DVecH ⁡ k ⁡ w ⟼ f ∈ LFnl ⁡ DVecH ⁡ k ⁡ w | ocH ⁡ k ⁡ w ⁡ ocH ⁡ k ⁡ w ⁡ LKer ⁡ DVecH ⁡ k ⁡ w ⁡ f = LKer ⁡ DVecH ⁡ k ⁡ w ⁡ f ∧ ocH ⁡ k ⁡ w ⁡ LKer ⁡ DVecH ⁡ k ⁡ w ⁡ f ⊆ s

Detailed syntax breakdown

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