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 38831
Description: Extend class notation with a one-to-one onto (mapd1o 38854), order-preserving (mapdord 38844) 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 38830 . 2 class mapd
2 vk . . 3 setvar 𝑘
3 cvv 3480 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1537 . . . . 5 class 𝑘
6 clh 37190 . . . . 5 class LHyp
75, 6cfv 6343 . . . 4 class (LHyp‘𝑘)
8 vs . . . . 5 setvar 𝑠
94cv 1537 . . . . . . 7 class 𝑤
10 cdvh 38284 . . . . . . . 8 class DVecH
115, 10cfv 6343 . . . . . . 7 class (DVecH‘𝑘)
129, 11cfv 6343 . . . . . 6 class ((DVecH‘𝑘)‘𝑤)
13 clss 19696 . . . . . 6 class LSubSp
1412, 13cfv 6343 . . . . 5 class (LSubSp‘((DVecH‘𝑘)‘𝑤))
15 vf . . . . . . . . . . . 12 setvar 𝑓
1615cv 1537 . . . . . . . . . . 11 class 𝑓
17 clk 36291 . . . . . . . . . . . 12 class LKer
1812, 17cfv 6343 . . . . . . . . . . 11 class (LKer‘((DVecH‘𝑘)‘𝑤))
1916, 18cfv 6343 . . . . . . . . . 10 class ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)
20 coch 38553 . . . . . . . . . . . 12 class ocH
215, 20cfv 6343 . . . . . . . . . . 11 class (ocH‘𝑘)
229, 21cfv 6343 . . . . . . . . . 10 class ((ocH‘𝑘)‘𝑤)
2319, 22cfv 6343 . . . . . . . . 9 class (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))
2423, 22cfv 6343 . . . . . . . 8 class (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)))
2524, 19wceq 1538 . . . . . . 7 wff (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)
268cv 1537 . . . . . . . 8 class 𝑠
2723, 26wss 3919 . . . . . . 7 wff (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)) ⊆ 𝑠
2825, 27wa 399 . . . . . 6 wff ((((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓) ∧ (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)) ⊆ 𝑠)
29 clfn 36263 . . . . . . 7 class LFnl
3012, 29cfv 6343 . . . . . 6 class (LFnl‘((DVecH‘𝑘)‘𝑤))
3128, 15, 30crab 3137 . . . . 5 class {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ ((((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓) ∧ (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)) ⊆ 𝑠)}
328, 14, 31cmpt 5132 . . . 4 class (𝑠 ∈ (LSubSp‘((DVecH‘𝑘)‘𝑤)) ↦ {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ ((((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓) ∧ (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)) ⊆ 𝑠)})
334, 7, 32cmpt 5132 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑠 ∈ (LSubSp‘((DVecH‘𝑘)‘𝑤)) ↦ {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ ((((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓) ∧ (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)) ⊆ 𝑠)}))
342, 3, 33cmpt 5132 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑠 ∈ (LSubSp‘((DVecH‘𝑘)‘𝑤)) ↦ {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ ((((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓) ∧ (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)) ⊆ 𝑠)})))
351, 34wceq 1538 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  38832
  Copyright terms: Public domain W3C validator