Definition df-mapd 41627

Description: Extend class notation with a one-to-one onto (mapd1o 41650), order-preserving (mapdord 41640) 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

Step	Hyp	Ref	Expression
1		cmpd 41626	. 2 class mapd
2		vk	. . 3 setvar 𝑘
3		cvv 3480	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1539	. . . . 5 class 𝑘
6		clh 39986	. . . . 5 class LHyp
7	5, 6	cfv 6561	. . . 4 class (LHyp‘𝑘)
8		vs	. . . . 5 setvar 𝑠
9	4	cv 1539	. . . . . . 7 class 𝑤
10		cdvh 41080	. . . . . . . 8 class DVecH
11	5, 10	cfv 6561	. . . . . . 7 class (DVecH‘𝑘)
12	9, 11	cfv 6561	. . . . . 6 class ((DVecH‘𝑘)‘𝑤)
13		clss 20929	. . . . . 6 class LSubSp
14	12, 13	cfv 6561	. . . . 5 class (LSubSp‘((DVecH‘𝑘)‘𝑤))
15		vf	. . . . . . . . . . . 12 setvar 𝑓
16	15	cv 1539	. . . . . . . . . . 11 class 𝑓
17		clk 39086	. . . . . . . . . . . 12 class LKer
18	12, 17	cfv 6561	. . . . . . . . . . 11 class (LKer‘((DVecH‘𝑘)‘𝑤))
19	16, 18	cfv 6561	. . . . . . . . . 10 class ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)
20		coch 41349	. . . . . . . . . . . 12 class ocH
21	5, 20	cfv 6561	. . . . . . . . . . 11 class (ocH‘𝑘)
22	9, 21	cfv 6561	. . . . . . . . . 10 class ((ocH‘𝑘)‘𝑤)
23	19, 22	cfv 6561	. . . . . . . . 9 class (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))
24	23, 22	cfv 6561	. . . . . . . 8 class (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)))
25	24, 19	wceq 1540	. . . . . . 7 wff (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)
26	8	cv 1539	. . . . . . . 8 class 𝑠
27	23, 26	wss 3951	. . . . . . 7 wff (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)) ⊆ 𝑠
28	25, 27	wa 395	. . . . . 6 wff ((((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓) ∧ (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)) ⊆ 𝑠)
29		clfn 39058	. . . . . . 7 class LFnl
30	12, 29	cfv 6561	. . . . . 6 class (LFnl‘((DVecH‘𝑘)‘𝑤))
31	28, 15, 30	crab 3436	. . . . 5 class {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ ((((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓) ∧ (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)) ⊆ 𝑠)}
32	8, 14, 31	cmpt 5225	. . . 4 class (𝑠 ∈ (LSubSp‘((DVecH‘𝑘)‘𝑤)) ↦ {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ ((((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓) ∧ (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)) ⊆ 𝑠)})
33	4, 7, 32	cmpt 5225	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑠 ∈ (LSubSp‘((DVecH‘𝑘)‘𝑤)) ↦ {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ ((((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓) ∧ (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)) ⊆ 𝑠)}))
34	2, 3, 33	cmpt 5225	. 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑠 ∈ (LSubSp‘((DVecH‘𝑘)‘𝑤)) ↦ {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ ((((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓) ∧ (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)) ⊆ 𝑠)})))
35	1, 34	wceq 1540	1 wff mapd = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑠 ∈ (LSubSp‘((DVecH‘𝑘)‘𝑤)) ↦ {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ ((((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓) ∧ (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)) ⊆ 𝑠)})))

This definition is referenced by:  mapdffval  41628