Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mapd Structured version   Visualization version   GIF version

Definition df-mapd 37231
Description: Extend class notation with a one-to-one onto (mapd1o 37254), order-preserving (mapdord 37244) 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.)
Assertion
Ref Expression
df-mapd mapd = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑠 ∈ (LSubSp‘((DVecH‘𝑘)‘𝑤)) ↦ {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ ((((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓) ∧ (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)) ⊆ 𝑠)})))
Distinct variable group:   𝑘,𝑠,𝑤,𝑓

Detailed syntax breakdown of Definition df-mapd
StepHypRef Expression
1 cmpd 37230 . 2 class mapd
2 vk . . 3 setvar 𝑘
3 cvv 3231 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1522 . . . . 5 class 𝑘
6 clh 35588 . . . . 5 class LHyp
75, 6cfv 5926 . . . 4 class (LHyp‘𝑘)
8 vs . . . . 5 setvar 𝑠
94cv 1522 . . . . . . 7 class 𝑤
10 cdvh 36684 . . . . . . . 8 class DVecH
115, 10cfv 5926 . . . . . . 7 class (DVecH‘𝑘)
129, 11cfv 5926 . . . . . 6 class ((DVecH‘𝑘)‘𝑤)
13 clss 18980 . . . . . 6 class LSubSp
1412, 13cfv 5926 . . . . 5 class (LSubSp‘((DVecH‘𝑘)‘𝑤))
15 vf . . . . . . . . . . . 12 setvar 𝑓
1615cv 1522 . . . . . . . . . . 11 class 𝑓
17 clk 34690 . . . . . . . . . . . 12 class LKer
1812, 17cfv 5926 . . . . . . . . . . 11 class (LKer‘((DVecH‘𝑘)‘𝑤))
1916, 18cfv 5926 . . . . . . . . . 10 class ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)
20 coch 36953 . . . . . . . . . . . 12 class ocH
215, 20cfv 5926 . . . . . . . . . . 11 class (ocH‘𝑘)
229, 21cfv 5926 . . . . . . . . . 10 class ((ocH‘𝑘)‘𝑤)
2319, 22cfv 5926 . . . . . . . . 9 class (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))
2423, 22cfv 5926 . . . . . . . 8 class (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)))
2524, 19wceq 1523 . . . . . . 7 wff (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)
268cv 1522 . . . . . . . 8 class 𝑠
2723, 26wss 3607 . . . . . . 7 wff (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)) ⊆ 𝑠
2825, 27wa 383 . . . . . 6 wff ((((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓) ∧ (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)) ⊆ 𝑠)
29 clfn 34662 . . . . . . 7 class LFnl
3012, 29cfv 5926 . . . . . 6 class (LFnl‘((DVecH‘𝑘)‘𝑤))
3128, 15, 30crab 2945 . . . . 5 class {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ ((((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓) ∧ (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)) ⊆ 𝑠)}
328, 14, 31cmpt 4762 . . . 4 class (𝑠 ∈ (LSubSp‘((DVecH‘𝑘)‘𝑤)) ↦ {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ ((((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓) ∧ (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)) ⊆ 𝑠)})
334, 7, 32cmpt 4762 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑠 ∈ (LSubSp‘((DVecH‘𝑘)‘𝑤)) ↦ {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ ((((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓) ∧ (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)) ⊆ 𝑠)}))
342, 3, 33cmpt 4762 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑠 ∈ (LSubSp‘((DVecH‘𝑘)‘𝑤)) ↦ {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ ((((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓) ∧ (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)) ⊆ 𝑠)})))
351, 34wceq 1523 1 wff mapd = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑠 ∈ (LSubSp‘((DVecH‘𝑘)‘𝑤)) ↦ {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ ((((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓) ∧ (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)) ⊆ 𝑠)})))
Colors of variables: wff setvar class
This definition is referenced by:  mapdffval  37232
  Copyright terms: Public domain W3C validator