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

Definition df-mapd 35110
Description: Extend class notation with a one-to-one onto (mapd1o 35133), order-preserving (mapdord 35123) 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  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  ( s  e.  ( LSubSp `  (
( DVecH `  k ) `  w ) )  |->  { f  e.  (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 ) )  C_  s ) } ) ) )
Distinct variable group:    k, s, w, f

Detailed syntax breakdown of Definition df-mapd
StepHypRef Expression
1 cmpd 35109 . 2  class mapd
2 vk . . 3  setvar  k
3 cvv 2967 . . 3  class  _V
4 vw . . . 4  setvar  w
52cv 1368 . . . . 5  class  k
6 clh 33468 . . . . 5  class  LHyp
75, 6cfv 5413 . . . 4  class  ( LHyp `  k )
8 vs . . . . 5  setvar  s
94cv 1368 . . . . . . 7  class  w
10 cdvh 34563 . . . . . . . 8  class  DVecH
115, 10cfv 5413 . . . . . . 7  class  ( DVecH `  k )
129, 11cfv 5413 . . . . . 6  class  ( (
DVecH `  k ) `  w )
13 clss 16990 . . . . . 6  class  LSubSp
1412, 13cfv 5413 . . . . 5  class  ( LSubSp `  ( ( DVecH `  k
) `  w )
)
15 vf . . . . . . . . . . . 12  setvar  f
1615cv 1368 . . . . . . . . . . 11  class  f
17 clk 32570 . . . . . . . . . . . 12  class LKer
1812, 17cfv 5413 . . . . . . . . . . 11  class  (LKer `  ( ( DVecH `  k
) `  w )
)
1916, 18cfv 5413 . . . . . . . . . 10  class  ( (LKer `  ( ( DVecH `  k
) `  w )
) `  f )
20 coch 34832 . . . . . . . . . . . 12  class  ocH
215, 20cfv 5413 . . . . . . . . . . 11  class  ( ocH `  k )
229, 21cfv 5413 . . . . . . . . . 10  class  ( ( ocH `  k ) `
 w )
2319, 22cfv 5413 . . . . . . . . 9  class  ( ( ( ocH `  k
) `  w ) `  ( (LKer `  (
( DVecH `  k ) `  w ) ) `  f ) )
2423, 22cfv 5413 . . . . . . . 8  class  ( ( ( ocH `  k
) `  w ) `  ( ( ( ocH `  k ) `  w
) `  ( (LKer `  ( ( DVecH `  k
) `  w )
) `  f )
) )
2524, 19wceq 1369 . . . . . . 7  wff  ( ( ( ocH `  k
) `  w ) `  ( ( ( ocH `  k ) `  w
) `  ( (LKer `  ( ( DVecH `  k
) `  w )
) `  f )
) )  =  ( (LKer `  ( ( DVecH `  k ) `  w ) ) `  f )
268cv 1368 . . . . . . . 8  class  s
2723, 26wss 3323 . . . . . . 7  wff  ( ( ( ocH `  k
) `  w ) `  ( (LKer `  (
( DVecH `  k ) `  w ) ) `  f ) )  C_  s
2825, 27wa 369 . . . . . 6  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 ) )  C_  s )
29 clfn 32542 . . . . . . 7  class LFnl
3012, 29cfv 5413 . . . . . 6  class  (LFnl `  ( ( DVecH `  k
) `  w )
)
3128, 15, 30crab 2714 . . . . 5  class  { f  e.  (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 ) )  C_  s ) }
328, 14, 31cmpt 4345 . . . 4  class  ( s  e.  ( LSubSp `  (
( DVecH `  k ) `  w ) )  |->  { f  e.  (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 ) )  C_  s ) } )
334, 7, 32cmpt 4345 . . 3  class  ( w  e.  ( LHyp `  k
)  |->  ( s  e.  ( LSubSp `  ( ( DVecH `  k ) `  w ) )  |->  { f  e.  (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 ) )  C_  s ) } ) )
342, 3, 33cmpt 4345 . 2  class  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k
)  |->  ( s  e.  ( LSubSp `  ( ( DVecH `  k ) `  w ) )  |->  { f  e.  (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 ) )  C_  s ) } ) ) )
351, 34wceq 1369 1  wff mapd  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  ( s  e.  ( LSubSp `  (
( DVecH `  k ) `  w ) )  |->  { f  e.  (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 ) )  C_  s ) } ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  mapdffval  35111
  Copyright terms: Public domain W3C validator