mapd1o

Description: The map defined by df-mapd is one-to-one and onto the set of dual subspaces of functionals with closed kernels. This shows M satisfies part of the definition of projectivity of Baer p. 40. TODO: change theorems leading to this ( lcfr , mapdrval , lclkrs , lclkr ,...) to use T i^i ~P C ? TODO: maybe get rid of $d's for g versus K U W ; propagate to mapdrn and any others. (Contributed by NM, 12-Mar-2015)

	Ref	Expression
Hypotheses	mapd1o.h	$⊢ H = LHyp (K)$
	mapd1o.o	$⊢ O = ocH (K) (W)$
	mapd1o.m	$⊢ M = mapd (K) (W)$
	mapd1o.u	$⊢ U = DVecH (K) (W)$
	mapd1o.s	$⊢ S = LSubSp (U)$
	mapd1o.f	$⊢ F = LFnl (U)$
	mapd1o.l	$⊢ L = LKer (U)$
	mapd1o.d	$⊢ D = LDual (U)$
	mapd1o.t	$⊢ T = LSubSp (D)$
	mapd1o.c	$⊢ C = \{g \in F \| O (O (L (g))) = L (g)\}$
	mapd1o.k	$⊢ φ \to (K \in HL \land W \in H)$
Assertion	mapd1o	$⊢ φ \to M : S \underset{1-1 onto}{⟶} T \cap 𝒫 C$

Proof

Step	Hyp	Ref	Expression
1		mapd1o.h	$⊢ H = LHyp (K)$
2		mapd1o.o	$⊢ O = ocH (K) (W)$
3		mapd1o.m	$⊢ M = mapd (K) (W)$
4		mapd1o.u	$⊢ U = DVecH (K) (W)$
5		mapd1o.s	$⊢ S = LSubSp (U)$
6		mapd1o.f	$⊢ F = LFnl (U)$
7		mapd1o.l	$⊢ L = LKer (U)$
8		mapd1o.d	$⊢ D = LDual (U)$
9		mapd1o.t	$⊢ T = LSubSp (D)$
10		mapd1o.c	$⊢ C = \{g \in F \| O (O (L (g))) = L (g)\}$
11		mapd1o.k	$⊢ φ \to (K \in HL \land W \in H)$
12	6	fvexi	$⊢ F \in V$
13	12	rabex	$⊢ \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq t)\} \in V$
14		eqid	$⊢ (t \in S ⟼ \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq t)\}) = (t \in S ⟼ \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq t)\})$
15	13 14	fnmpti	$⊢ (t \in S ⟼ \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq t)\}) Fn S$
16	1 4 5 6 7 2 3	mapdfval	$⊢ (K \in HL \land W \in H) \to M = (t \in S ⟼ \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq t)\})$
17	11 16	syl	$⊢ φ \to M = (t \in S ⟼ \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq t)\})$
18	17	fneq1d	$⊢ φ \to (M Fn S \leftrightarrow (t \in S ⟼ \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq t)\}) Fn S)$
19	15 18	mpbiri	$⊢ φ \to M Fn S$
20	12	rabex	$⊢ \{g \in F \| (O (O (L (g))) = L (g) \land O (L (g)) \subseteq t)\} \in V$
21		eqid	$⊢ (t \in S ⟼ \{g \in F \| (O (O (L (g))) = L (g) \land O (L (g)) \subseteq t)\}) = (t \in S ⟼ \{g \in F \| (O (O (L (g))) = L (g) \land O (L (g)) \subseteq t)\})$
22	20 21	fnmpti	$⊢ (t \in S ⟼ \{g \in F \| (O (O (L (g))) = L (g) \land O (L (g)) \subseteq t)\}) Fn S$
23	1 4 5 6 7 2 3	mapdfval	$⊢ (K \in HL \land W \in H) \to M = (t \in S ⟼ \{g \in F \| (O (O (L (g))) = L (g) \land O (L (g)) \subseteq t)\})$
24	11 23	syl	$⊢ φ \to M = (t \in S ⟼ \{g \in F \| (O (O (L (g))) = L (g) \land O (L (g)) \subseteq t)\})$
25	24	fneq1d	$⊢ φ \to (M Fn S \leftrightarrow (t \in S ⟼ \{g \in F \| (O (O (L (g))) = L (g) \land O (L (g)) \subseteq t)\}) Fn S)$
26	22 25	mpbiri	$⊢ φ \to M Fn S$
27		fvelrnb	$⊢ M Fn S \to (t \in ran M \leftrightarrow \exists c \in S M (c) = t)$
28	26 27	syl	$⊢ φ \to (t \in ran M \leftrightarrow \exists c \in S M (c) = t)$
29	11	adantr	$⊢ (φ \land c \in S) \to (K \in HL \land W \in H)$
30		simpr	$⊢ (φ \land c \in S) \to c \in S$
31	1 4 5 6 7 2 3 29 30	mapdval	$⊢ (φ \land c \in S) \to M (c) = \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq c)\}$
32		eqid	$⊢ \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq c)\} = \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq c)\}$
33	1 2 4 5 6 7 8 9 10 32 29 30	lclkrs2	$⊢ (φ \land c \in S) \to (\{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq c)\} \in T \land \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq c)\} \subseteq C)$
34		elin	$⊢ \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq c)\} \in (T \cap 𝒫 C) \leftrightarrow (\{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq c)\} \in T \land \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq c)\} \in 𝒫 C)$
35	12	rabex	$⊢ \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq c)\} \in V$
36	35	elpw	$⊢ \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq c)\} \in 𝒫 C \leftrightarrow \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq c)\} \subseteq C$
37	36	anbi2i	$⊢ (\{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq c)\} \in T \land \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq c)\} \in 𝒫 C) \leftrightarrow (\{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq c)\} \in T \land \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq c)\} \subseteq C)$
38	34 37	bitr2i	$⊢ (\{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq c)\} \in T \land \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq c)\} \subseteq C) \leftrightarrow \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq c)\} \in (T \cap 𝒫 C)$
39	33 38	sylib	$⊢ (φ \land c \in S) \to \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq c)\} \in (T \cap 𝒫 C)$
40	31 39	eqeltrd	$⊢ (φ \land c \in S) \to M (c) \in (T \cap 𝒫 C)$
41		eleq1	$⊢ M (c) = t \to (M (c) \in (T \cap 𝒫 C) \leftrightarrow t \in (T \cap 𝒫 C))$
42	40 41	syl5ibcom	$⊢ (φ \land c \in S) \to (M (c) = t \to t \in (T \cap 𝒫 C))$
43	42	rexlimdva	$⊢ φ \to (\exists c \in S M (c) = t \to t \in (T \cap 𝒫 C))$
44		eqid	$⊢ ⋃_{f \in t} O (L (f)) = ⋃_{f \in t} O (L (f))$
45	11	adantr	$⊢ (φ \land t \in (T \cap 𝒫 C)) \to (K \in HL \land W \in H)$
46		inss1	$⊢ T \cap 𝒫 C \subseteq T$
47	46	sseli	$⊢ t \in (T \cap 𝒫 C) \to t \in T$
48	47	adantl	$⊢ (φ \land t \in (T \cap 𝒫 C)) \to t \in T$
49		inss2	$⊢ T \cap 𝒫 C \subseteq 𝒫 C$
50	49	sseli	$⊢ t \in (T \cap 𝒫 C) \to t \in 𝒫 C$
51	50	elpwid	$⊢ t \in (T \cap 𝒫 C) \to t \subseteq C$
52	51	adantl	$⊢ (φ \land t \in (T \cap 𝒫 C)) \to t \subseteq C$
53	1 2 4 5 6 7 8 9 10 44 45 48 52	lcfr	$⊢ (φ \land t \in (T \cap 𝒫 C)) \to ⋃_{f \in t} O (L (f)) \in S$
54	1 2 3 4 5 6 7 8 9 10 45 48 52 44	mapdrval	$⊢ (φ \land t \in (T \cap 𝒫 C)) \to M (⋃_{f \in t} O (L (f))) = t$
55		fveqeq2	$⊢ c = ⋃_{f \in t} O (L (f)) \to (M (c) = t \leftrightarrow M (⋃_{f \in t} O (L (f))) = t)$
56	55	rspcev	$⊢ (⋃_{f \in t} O (L (f)) \in S \land M (⋃_{f \in t} O (L (f))) = t) \to \exists c \in S M (c) = t$
57	53 54 56	syl2anc	$⊢ (φ \land t \in (T \cap 𝒫 C)) \to \exists c \in S M (c) = t$
58	57	ex	$⊢ φ \to (t \in (T \cap 𝒫 C) \to \exists c \in S M (c) = t)$
59	43 58	impbid	$⊢ φ \to (\exists c \in S M (c) = t \leftrightarrow t \in (T \cap 𝒫 C))$
60	28 59	bitrd	$⊢ φ \to (t \in ran M \leftrightarrow t \in (T \cap 𝒫 C))$
61	60	eqrdv	$⊢ φ \to ran M = T \cap 𝒫 C$
62	11	adantr	$⊢ (φ \land (t \in S \land u \in S)) \to (K \in HL \land W \in H)$
63		simprl	$⊢ (φ \land (t \in S \land u \in S)) \to t \in S$
64		simprr	$⊢ (φ \land (t \in S \land u \in S)) \to u \in S$
65	1 4 5 3 62 63 64	mapd11	$⊢ (φ \land (t \in S \land u \in S)) \to (M (t) = M (u) \leftrightarrow t = u)$
66	65	biimpd	$⊢ (φ \land (t \in S \land u \in S)) \to (M (t) = M (u) \to t = u)$
67	66	ralrimivva	$⊢ φ \to \forall t \in S \forall u \in S (M (t) = M (u) \to t = u)$
68		dff1o6	$⊢ M : S \underset{1-1 onto}{⟶} T \cap 𝒫 C \leftrightarrow (M Fn S \land ran M = T \cap 𝒫 C \land \forall t \in S \forall u \in S (M (t) = M (u) \to t = u))$
69	19 61 67 68	syl3anbrc	$⊢ φ \to M : S \underset{1-1 onto}{⟶} T \cap 𝒫 C$

Metamath Proof Explorer

Theorem mapd1o

Proof