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 37700
 Description: Extend class notation with a one-to-one onto (mapd1o 37723), order-preserving (mapdord 37713) 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 37699 . 2 class mapd
2 vk . . 3 setvar 𝑘
3 cvv 3414 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1657 . . . . 5 class 𝑘
6 clh 36059 . . . . 5 class LHyp
75, 6cfv 6123 . . . 4 class (LHyp‘𝑘)
8 vs . . . . 5 setvar 𝑠
94cv 1657 . . . . . . 7 class 𝑤
10 cdvh 37153 . . . . . . . 8 class DVecH
115, 10cfv 6123 . . . . . . 7 class (DVecH‘𝑘)
129, 11cfv 6123 . . . . . 6 class ((DVecH‘𝑘)‘𝑤)
13 clss 19288 . . . . . 6 class LSubSp
1412, 13cfv 6123 . . . . 5 class (LSubSp‘((DVecH‘𝑘)‘𝑤))
15 vf . . . . . . . . . . . 12 setvar 𝑓
1615cv 1657 . . . . . . . . . . 11 class 𝑓
17 clk 35160 . . . . . . . . . . . 12 class LKer
1812, 17cfv 6123 . . . . . . . . . . 11 class (LKer‘((DVecH‘𝑘)‘𝑤))
1916, 18cfv 6123 . . . . . . . . . 10 class ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)
20 coch 37422 . . . . . . . . . . . 12 class ocH
215, 20cfv 6123 . . . . . . . . . . 11 class (ocH‘𝑘)
229, 21cfv 6123 . . . . . . . . . 10 class ((ocH‘𝑘)‘𝑤)
2319, 22cfv 6123 . . . . . . . . 9 class (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))
2423, 22cfv 6123 . . . . . . . 8 class (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)))
2524, 19wceq 1658 . . . . . . 7 wff (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)
268cv 1657 . . . . . . . 8 class 𝑠
2723, 26wss 3798 . . . . . . 7 wff (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)) ⊆ 𝑠
2825, 27wa 386 . . . . . 6 wff ((((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓) ∧ (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)) ⊆ 𝑠)
29 clfn 35132 . . . . . . 7 class LFnl
3012, 29cfv 6123 . . . . . 6 class (LFnl‘((DVecH‘𝑘)‘𝑤))
3128, 15, 30crab 3121 . . . . 5 class {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ ((((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓) ∧ (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)) ⊆ 𝑠)}
328, 14, 31cmpt 4952 . . . 4 class (𝑠 ∈ (LSubSp‘((DVecH‘𝑘)‘𝑤)) ↦ {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ ((((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓) ∧ (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)) ⊆ 𝑠)})
334, 7, 32cmpt 4952 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑠 ∈ (LSubSp‘((DVecH‘𝑘)‘𝑤)) ↦ {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ ((((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓) ∧ (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)) ⊆ 𝑠)}))
342, 3, 33cmpt 4952 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑠 ∈ (LSubSp‘((DVecH‘𝑘)‘𝑤)) ↦ {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ ((((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓) ∧ (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)) ⊆ 𝑠)})))
351, 34wceq 1658 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  37701
 Copyright terms: Public domain W3C validator