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 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 ) } ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmpd 
 |-  mapd
1 vk 
 |-  k
2 cvv 
 |-  _V
3 vw 
 |-  w
4 clh 
 |-  LHyp
5 1 cv 
 |-  k
6 5 4 cfv 
 |-  ( LHyp ` k )
7 vs 
 |-  s
8 clss 
 |-  LSubSp
9 cdvh 
 |-  DVecH
10 5 9 cfv 
 |-  ( DVecH ` k )
11 3 cv 
 |-  w
12 11 10 cfv 
 |-  ( ( DVecH ` k ) ` w )
13 12 8 cfv 
 |-  ( LSubSp ` ( ( DVecH ` k ) ` w ) )
14 vf 
 |-  f
15 clfn 
 |-  LFnl
16 12 15 cfv 
 |-  ( LFnl ` ( ( DVecH ` k ) ` w ) )
17 coch 
 |-  ocH
18 5 17 cfv 
 |-  ( ocH ` k )
19 11 18 cfv 
 |-  ( ( ocH ` k ) ` w )
20 clk 
 |-  LKer
21 12 20 cfv 
 |-  ( LKer ` ( ( DVecH ` k ) ` w ) )
22 14 cv 
 |-  f
23 22 21 cfv 
 |-  ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f )
24 23 19 cfv 
 |-  ( ( ( ocH ` k ) ` w ) ` ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) )
25 24 19 cfv 
 |-  ( ( ( ocH ` k ) ` w ) ` ( ( ( ocH ` k ) ` w ) ` ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) ) )
26 25 23 wceq 
 |-  ( ( ( ocH ` k ) ` w ) ` ( ( ( ocH ` k ) ` w ) ` ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) ) ) = ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f )
27 7 cv 
 |-  s
28 24 27 wss 
 |-  ( ( ( ocH ` k ) ` w ) ` ( ( LKer ` ( ( DVecH ` k ) ` w ) ) ` f ) ) C_ s
29 26 28 wa 
 |-  ( ( ( ( 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 )
30 29 14 16 crab 
 |-  { 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 ) }
31 7 13 30 cmpt 
 |-  ( 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 ) } )
32 3 6 31 cmpt 
 |-  ( 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 ) } ) )
33 1 2 32 cmpt 
 |-  ( 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 ) } ) ) )
34 0 33 wceq 
 |-  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 ) } ) ) )