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 \in V ⟼ (w \in LHyp (k) ⟼ (s \in LSubSp (DVecH (k) (w)) ⟼ \{f \in LFnl (DVecH (k) (w)) \| (ocH (k) (w) (ocH (k) (w) (LKer (DVecH (k) (w)) (f))) = LKer (DVecH (k) (w)) (f) \land ocH (k) (w) (LKer (DVecH (k) (w)) (f)) \subseteq s)\})))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmpd	$class mapd$
1		vk	$setvar k$
2		cvv	$class V$
3		vw	$setvar w$
4		clh	$class LHyp$
5	1	cv	$setvar k$
6	5 4	cfv	$class LHyp (k)$
7		vs	$setvar s$
8		clss	$class LSubSp$
9		cdvh	$class DVecH$
10	5 9	cfv	$class DVecH (k)$
11	3	cv	$setvar w$
12	11 10	cfv	$class DVecH (k) (w)$
13	12 8	cfv	$class LSubSp (DVecH (k) (w))$
14		vf	$setvar f$
15		clfn	$class LFnl$
16	12 15	cfv	$class LFnl (DVecH (k) (w))$
17		coch	$class ocH$
18	5 17	cfv	$class ocH (k)$
19	11 18	cfv	$class ocH (k) (w)$
20		clk	$class LKer$
21	12 20	cfv	$class LKer (DVecH (k) (w))$
22	14	cv	$setvar f$
23	22 21	cfv	$class LKer (DVecH (k) (w)) (f)$
24	23 19	cfv	$class ocH (k) (w) (LKer (DVecH (k) (w)) (f))$
25	24 19	cfv	$class ocH (k) (w) (ocH (k) (w) (LKer (DVecH (k) (w)) (f)))$
26	25 23	wceq	$wff ocH (k) (w) (ocH (k) (w) (LKer (DVecH (k) (w)) (f))) = LKer (DVecH (k) (w)) (f)$
27	7	cv	$setvar s$
28	24 27	wss	$wff ocH (k) (w) (LKer (DVecH (k) (w)) (f)) \subseteq s$
29	26 28	wa	$wff (ocH (k) (w) (ocH (k) (w) (LKer (DVecH (k) (w)) (f))) = LKer (DVecH (k) (w)) (f) \land ocH (k) (w) (LKer (DVecH (k) (w)) (f)) \subseteq s)$
30	29 14 16	crab	$class \{f \in LFnl (DVecH (k) (w)) \| (ocH (k) (w) (ocH (k) (w) (LKer (DVecH (k) (w)) (f))) = LKer (DVecH (k) (w)) (f) \land ocH (k) (w) (LKer (DVecH (k) (w)) (f)) \subseteq s)\}$
31	7 13 30	cmpt	$class (s \in LSubSp (DVecH (k) (w)) ⟼ \{f \in LFnl (DVecH (k) (w)) \| (ocH (k) (w) (ocH (k) (w) (LKer (DVecH (k) (w)) (f))) = LKer (DVecH (k) (w)) (f) \land ocH (k) (w) (LKer (DVecH (k) (w)) (f)) \subseteq s)\})$
32	3 6 31	cmpt	$class (w \in LHyp (k) ⟼ (s \in LSubSp (DVecH (k) (w)) ⟼ \{f \in LFnl (DVecH (k) (w)) \| (ocH (k) (w) (ocH (k) (w) (LKer (DVecH (k) (w)) (f))) = LKer (DVecH (k) (w)) (f) \land ocH (k) (w) (LKer (DVecH (k) (w)) (f)) \subseteq s)\}))$
33	1 2 32	cmpt	$class (k \in V ⟼ (w \in LHyp (k) ⟼ (s \in LSubSp (DVecH (k) (w)) ⟼ \{f \in LFnl (DVecH (k) (w)) \| (ocH (k) (w) (ocH (k) (w) (LKer (DVecH (k) (w)) (f))) = LKer (DVecH (k) (w)) (f) \land ocH (k) (w) (LKer (DVecH (k) (w)) (f)) \subseteq s)\})))$
34	0 33	wceq	$wff mapd = (k \in V ⟼ (w \in LHyp (k) ⟼ (s \in LSubSp (DVecH (k) (w)) ⟼ \{f \in LFnl (DVecH (k) (w)) \| (ocH (k) (w) (ocH (k) (w) (LKer (DVecH (k) (w)) (f))) = LKer (DVecH (k) (w)) (f) \land ocH (k) (w) (LKer (DVecH (k) (w)) (f)) \subseteq s)\})))$

Metamath Proof Explorer

Definition df-mapd

Detailed syntax breakdown