mapdval4N

Description: Value of projectivity from vector space H to dual space. TODO: 1. This is shorter than others - make it the official def? (but is not as obvious that it is C_ C ) 2. The unneeded direction of lcfl8a has awkward E. - add another thm with only one direction of it? 3. Swap O{ v } and Lf ? (Contributed by NM, 31-Jan-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mapdval4.h	$⊢ H = LHyp (K)$
	mapdval4.u	$⊢ U = DVecH (K) (W)$
	mapdval4.s	$⊢ S = LSubSp (U)$
	mapdval4.f	$⊢ F = LFnl (U)$
	mapdval4.l	$⊢ L = LKer (U)$
	mapdval4.o	$⊢ O = ocH (K) (W)$
	mapdval4.m	$⊢ M = mapd (K) (W)$
	mapdval4.k	$⊢ φ \to (K \in HL \land W \in H)$
	mapdval4.t	$⊢ φ \to T \in S$
Assertion	mapdval4N	$⊢ φ \to M (T) = \{f \in F \| \exists v \in T O (\{v\}) = L (f)\}$

Proof

Step	Hyp	Ref	Expression
1		mapdval4.h	$⊢ H = LHyp (K)$
2		mapdval4.u	$⊢ U = DVecH (K) (W)$
3		mapdval4.s	$⊢ S = LSubSp (U)$
4		mapdval4.f	$⊢ F = LFnl (U)$
5		mapdval4.l	$⊢ L = LKer (U)$
6		mapdval4.o	$⊢ O = ocH (K) (W)$
7		mapdval4.m	$⊢ M = mapd (K) (W)$
8		mapdval4.k	$⊢ φ \to (K \in HL \land W \in H)$
9		mapdval4.t	$⊢ φ \to T \in S$
10		eqid	$⊢ LSpan (U) = LSpan (U)$
11		eqid	$⊢ \{g \in F \| O (O (L (g))) = L (g)\} = \{g \in F \| O (O (L (g))) = L (g)\}$
12	1 2 3 10 4 5 6 7 8 9 11	mapdval2N	$⊢ φ \to M (T) = \{f \in \{g \in F \| O (O (L (g))) = L (g)\} \| \exists v \in T O (L (f)) = LSpan (U) (\{v\})\}$
13	11	lcfl1lem	$⊢ f \in \{g \in F \| O (O (L (g))) = L (g)\} \leftrightarrow (f \in F \land O (O (L (f))) = L (f))$
14	13	anbi1i	$⊢ (f \in \{g \in F \| O (O (L (g))) = L (g)\} \land \exists v \in T O (L (f)) = LSpan (U) (\{v\})) \leftrightarrow ((f \in F \land O (O (L (f))) = L (f)) \land \exists v \in T O (L (f)) = LSpan (U) (\{v\}))$
15		anass	$⊢ ((f \in F \land O (O (L (f))) = L (f)) \land \exists v \in T O (L (f)) = LSpan (U) (\{v\})) \leftrightarrow (f \in F \land (O (O (L (f))) = L (f) \land \exists v \in T O (L (f)) = LSpan (U) (\{v\})))$
16	14 15	bitri	$⊢ (f \in \{g \in F \| O (O (L (g))) = L (g)\} \land \exists v \in T O (L (f)) = LSpan (U) (\{v\})) \leftrightarrow (f \in F \land (O (O (L (f))) = L (f) \land \exists v \in T O (L (f)) = LSpan (U) (\{v\})))$
17		r19.42v	$⊢ \exists v \in T (O (O (L (f))) = L (f) \land O (L (f)) = LSpan (U) (\{v\})) \leftrightarrow (O (O (L (f))) = L (f) \land \exists v \in T O (L (f)) = LSpan (U) (\{v\}))$
18		simprr	$⊢ (((φ \land f \in F) \land v \in T) \land (O (O (L (f))) = L (f) \land O (L (f)) = LSpan (U) (\{v\}))) \to O (L (f)) = LSpan (U) (\{v\})$
19	18	fveq2d	$⊢ (((φ \land f \in F) \land v \in T) \land (O (O (L (f))) = L (f) \land O (L (f)) = LSpan (U) (\{v\}))) \to O (O (L (f))) = O (LSpan (U) (\{v\}))$
20		simprl	$⊢ (((φ \land f \in F) \land v \in T) \land (O (O (L (f))) = L (f) \land O (L (f)) = LSpan (U) (\{v\}))) \to O (O (L (f))) = L (f)$
21		eqid	$⊢ {Base}_{U} = {Base}_{U}$
22	8	adantr	$⊢ (φ \land f \in F) \to (K \in HL \land W \in H)$
23	22	adantr	$⊢ ((φ \land f \in F) \land v \in T) \to (K \in HL \land W \in H)$
24	23	adantr	$⊢ (((φ \land f \in F) \land v \in T) \land (O (O (L (f))) = L (f) \land O (L (f)) = LSpan (U) (\{v\}))) \to (K \in HL \land W \in H)$
25	9	adantr	$⊢ (φ \land f \in F) \to T \in S$
26	21 3	lssel	$⊢ (T \in S \land v \in T) \to v \in {Base}_{U}$
27	25 26	sylan	$⊢ ((φ \land f \in F) \land v \in T) \to v \in {Base}_{U}$
28	27	snssd	$⊢ ((φ \land f \in F) \land v \in T) \to \{v\} \subseteq {Base}_{U}$
29	28	adantr	$⊢ (((φ \land f \in F) \land v \in T) \land (O (O (L (f))) = L (f) \land O (L (f)) = LSpan (U) (\{v\}))) \to \{v\} \subseteq {Base}_{U}$
30	1 2 6 21 10 24 29	dochocsp	$⊢ (((φ \land f \in F) \land v \in T) \land (O (O (L (f))) = L (f) \land O (L (f)) = LSpan (U) (\{v\}))) \to O (LSpan (U) (\{v\})) = O (\{v\})$
31	19 20 30	3eqtr3rd	$⊢ (((φ \land f \in F) \land v \in T) \land (O (O (L (f))) = L (f) \land O (L (f)) = LSpan (U) (\{v\}))) \to O (\{v\}) = L (f)$
32	27	adantr	$⊢ (((φ \land f \in F) \land v \in T) \land O (\{v\}) = L (f)) \to v \in {Base}_{U}$
33		simpr	$⊢ (((φ \land f \in F) \land v \in T) \land O (\{v\}) = L (f)) \to O (\{v\}) = L (f)$
34	33	eqcomd	$⊢ (((φ \land f \in F) \land v \in T) \land O (\{v\}) = L (f)) \to L (f) = O (\{v\})$
35		sneq	$⊢ w = v \to \{w\} = \{v\}$
36	35	fveq2d	$⊢ w = v \to O (\{w\}) = O (\{v\})$
37	36	rspceeqv	$⊢ (v \in {Base}_{U} \land L (f) = O (\{v\})) \to \exists w \in {Base}_{U} L (f) = O (\{w\})$
38	32 34 37	syl2anc	$⊢ (((φ \land f \in F) \land v \in T) \land O (\{v\}) = L (f)) \to \exists w \in {Base}_{U} L (f) = O (\{w\})$
39	23	adantr	$⊢ (((φ \land f \in F) \land v \in T) \land O (\{v\}) = L (f)) \to (K \in HL \land W \in H)$
40		simpllr	$⊢ (((φ \land f \in F) \land v \in T) \land O (\{v\}) = L (f)) \to f \in F$
41	1 6 2 21 4 5 39 40	lcfl8a	$⊢ (((φ \land f \in F) \land v \in T) \land O (\{v\}) = L (f)) \to (O (O (L (f))) = L (f) \leftrightarrow \exists w \in {Base}_{U} L (f) = O (\{w\}))$
42	38 41	mpbird	$⊢ (((φ \land f \in F) \land v \in T) \land O (\{v\}) = L (f)) \to O (O (L (f))) = L (f)$
43	1 2 6 21 10 23 27	dochocsn	$⊢ ((φ \land f \in F) \land v \in T) \to O (O (\{v\})) = LSpan (U) (\{v\})$
44		fveq2	$⊢ O (\{v\}) = L (f) \to O (O (\{v\})) = O (L (f))$
45	43 44	sylan9req	$⊢ (((φ \land f \in F) \land v \in T) \land O (\{v\}) = L (f)) \to LSpan (U) (\{v\}) = O (L (f))$
46	45	eqcomd	$⊢ (((φ \land f \in F) \land v \in T) \land O (\{v\}) = L (f)) \to O (L (f)) = LSpan (U) (\{v\})$
47	42 46	jca	$⊢ (((φ \land f \in F) \land v \in T) \land O (\{v\}) = L (f)) \to (O (O (L (f))) = L (f) \land O (L (f)) = LSpan (U) (\{v\}))$
48	31 47	impbida	$⊢ ((φ \land f \in F) \land v \in T) \to ((O (O (L (f))) = L (f) \land O (L (f)) = LSpan (U) (\{v\})) \leftrightarrow O (\{v\}) = L (f))$
49	48	rexbidva	$⊢ (φ \land f \in F) \to (\exists v \in T (O (O (L (f))) = L (f) \land O (L (f)) = LSpan (U) (\{v\})) \leftrightarrow \exists v \in T O (\{v\}) = L (f))$
50	17 49	bitr3id	$⊢ (φ \land f \in F) \to ((O (O (L (f))) = L (f) \land \exists v \in T O (L (f)) = LSpan (U) (\{v\})) \leftrightarrow \exists v \in T O (\{v\}) = L (f))$
51	50	pm5.32da	$⊢ φ \to ((f \in F \land (O (O (L (f))) = L (f) \land \exists v \in T O (L (f)) = LSpan (U) (\{v\}))) \leftrightarrow (f \in F \land \exists v \in T O (\{v\}) = L (f)))$
52	16 51	syl5bb	$⊢ φ \to ((f \in \{g \in F \| O (O (L (g))) = L (g)\} \land \exists v \in T O (L (f)) = LSpan (U) (\{v\})) \leftrightarrow (f \in F \land \exists v \in T O (\{v\}) = L (f)))$
53	52	rabbidva2	$⊢ φ \to \{f \in \{g \in F \| O (O (L (g))) = L (g)\} \| \exists v \in T O (L (f)) = LSpan (U) (\{v\})\} = \{f \in F \| \exists v \in T O (\{v\}) = L (f)\}$
54	12 53	eqtrd	$⊢ φ \to M (T) = \{f \in F \| \exists v \in T O (\{v\}) = L (f)\}$

Metamath Proof Explorer

Theorem mapdval4N

Proof