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

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

This definition is referenced by:  mapdffval  35111