mapdval2N

Description: Value of projectivity from vector space H to dual space. (Contributed by NM, 31-Jan-2015) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		mapdval2.h	$⊢ H = LHyp (K)$
2		mapdval2.u	$⊢ U = DVecH (K) (W)$
3		mapdval2.s	$⊢ S = LSubSp (U)$
4		mapdval2.n	$⊢ N = LSpan (U)$
5		mapdval2.f	$⊢ F = LFnl (U)$
6		mapdval2.l	$⊢ L = LKer (U)$
7		mapdval2.o	$⊢ O = ocH (K) (W)$
8		mapdval2.m	$⊢ M = mapd (K) (W)$
9		mapdval2.k	$⊢ φ \to (K \in HL \land W \in H)$
10		mapdval2.t	$⊢ φ \to T \in S$
11		mapdval2.c	$⊢ C = \{g \in F \| O (O (L (g))) = L (g)\}$
12	1 2 3 5 6 7 8 9 10 11	mapdvalc	$⊢ φ \to M (T) = \{f \in C \| O (L (f)) \subseteq T\}$
13	1 2 9	dvhlmod	$⊢ φ \to U \in LMod$
14	13	ad3antrrr	$⊢ (((φ \land f \in C) \land O (L (f)) \in LSAtoms (U)) \land O (L (f)) \subseteq T) \to U \in LMod$
15		simplr	$⊢ (((φ \land f \in C) \land O (L (f)) \in LSAtoms (U)) \land O (L (f)) \subseteq T) \to O (L (f)) \in LSAtoms (U)$
16		eqid	$⊢ {Base}_{U} = {Base}_{U}$
17		eqid	$⊢ LSAtoms (U) = LSAtoms (U)$
18	16 4 17	islsati	$⊢ (U \in LMod \land O (L (f)) \in LSAtoms (U)) \to \exists v \in {Base}_{U} O (L (f)) = N (\{v\})$
19	14 15 18	syl2anc	$⊢ (((φ \land f \in C) \land O (L (f)) \in LSAtoms (U)) \land O (L (f)) \subseteq T) \to \exists v \in {Base}_{U} O (L (f)) = N (\{v\})$
20		simprr	$⊢ ((((φ \land f \in C) \land O (L (f)) \in LSAtoms (U)) \land O (L (f)) \subseteq T) \land (v \in {Base}_{U} \land O (L (f)) = N (\{v\}))) \to O (L (f)) = N (\{v\})$
21		simplr	$⊢ ((((φ \land f \in C) \land O (L (f)) \in LSAtoms (U)) \land O (L (f)) \subseteq T) \land (v \in {Base}_{U} \land O (L (f)) = N (\{v\}))) \to O (L (f)) \subseteq T$
22	20 21	eqsstrrd	$⊢ ((((φ \land f \in C) \land O (L (f)) \in LSAtoms (U)) \land O (L (f)) \subseteq T) \land (v \in {Base}_{U} \land O (L (f)) = N (\{v\}))) \to N (\{v\}) \subseteq T$
23	13	adantr	$⊢ (φ \land f \in C) \to U \in LMod$
24	23	ad3antrrr	$⊢ ((((φ \land f \in C) \land O (L (f)) \in LSAtoms (U)) \land O (L (f)) \subseteq T) \land (v \in {Base}_{U} \land O (L (f)) = N (\{v\}))) \to U \in LMod$
25	10	adantr	$⊢ (φ \land f \in C) \to T \in S$
26	25	ad3antrrr	$⊢ ((((φ \land f \in C) \land O (L (f)) \in LSAtoms (U)) \land O (L (f)) \subseteq T) \land (v \in {Base}_{U} \land O (L (f)) = N (\{v\}))) \to T \in S$
27		simprl	$⊢ ((((φ \land f \in C) \land O (L (f)) \in LSAtoms (U)) \land O (L (f)) \subseteq T) \land (v \in {Base}_{U} \land O (L (f)) = N (\{v\}))) \to v \in {Base}_{U}$
28	16 3 4 24 26 27	lspsnel5	$⊢ ((((φ \land f \in C) \land O (L (f)) \in LSAtoms (U)) \land O (L (f)) \subseteq T) \land (v \in {Base}_{U} \land O (L (f)) = N (\{v\}))) \to (v \in T \leftrightarrow N (\{v\}) \subseteq T)$
29	22 28	mpbird	$⊢ ((((φ \land f \in C) \land O (L (f)) \in LSAtoms (U)) \land O (L (f)) \subseteq T) \land (v \in {Base}_{U} \land O (L (f)) = N (\{v\}))) \to v \in T$
30	19 29 20	reximssdv	$⊢ (((φ \land f \in C) \land O (L (f)) \in LSAtoms (U)) \land O (L (f)) \subseteq T) \to \exists v \in T O (L (f)) = N (\{v\})$
31	30	ex	$⊢ ((φ \land f \in C) \land O (L (f)) \in LSAtoms (U)) \to (O (L (f)) \subseteq T \to \exists v \in T O (L (f)) = N (\{v\}))$
32		eqid	$⊢ 0_{U} = 0_{U}$
33	32 3	lss0cl	$⊢ (U \in LMod \land T \in S) \to 0_{U} \in T$
34	13 10 33	syl2anc	$⊢ φ \to 0_{U} \in T$
35	34	adantr	$⊢ (φ \land O (L (f)) = \{0_{U}\}) \to 0_{U} \in T$
36		simpr	$⊢ (φ \land O (L (f)) = \{0_{U}\}) \to O (L (f)) = \{0_{U}\}$
37	13	adantr	$⊢ (φ \land O (L (f)) = \{0_{U}\}) \to U \in LMod$
38	32 4	lspsn0	$⊢ U \in LMod \to N (\{0_{U}\}) = \{0_{U}\}$
39	37 38	syl	$⊢ (φ \land O (L (f)) = \{0_{U}\}) \to N (\{0_{U}\}) = \{0_{U}\}$
40	36 39	eqtr4d	$⊢ (φ \land O (L (f)) = \{0_{U}\}) \to O (L (f)) = N (\{0_{U}\})$
41		sneq	$⊢ v = 0_{U} \to \{v\} = \{0_{U}\}$
42	41	fveq2d	$⊢ v = 0_{U} \to N (\{v\}) = N (\{0_{U}\})$
43	42	rspceeqv	$⊢ (0_{U} \in T \land O (L (f)) = N (\{0_{U}\})) \to \exists v \in T O (L (f)) = N (\{v\})$
44	35 40 43	syl2anc	$⊢ (φ \land O (L (f)) = \{0_{U}\}) \to \exists v \in T O (L (f)) = N (\{v\})$
45	44	adantlr	$⊢ ((φ \land f \in C) \land O (L (f)) = \{0_{U}\}) \to \exists v \in T O (L (f)) = N (\{v\})$
46	45	a1d	$⊢ ((φ \land f \in C) \land O (L (f)) = \{0_{U}\}) \to (O (L (f)) \subseteq T \to \exists v \in T O (L (f)) = N (\{v\}))$
47	9	adantr	$⊢ (φ \land f \in C) \to (K \in HL \land W \in H)$
48	11	lcfl1lem	$⊢ f \in C \leftrightarrow (f \in F \land O (O (L (f))) = L (f))$
49	48	simplbi	$⊢ f \in C \to f \in F$
50	49	adantl	$⊢ (φ \land f \in C) \to f \in F$
51	1 7 2 32 17 5 6 47 50	dochsat0	$⊢ (φ \land f \in C) \to (O (L (f)) \in LSAtoms (U) \lor O (L (f)) = \{0_{U}\})$
52	31 46 51	mpjaodan	$⊢ (φ \land f \in C) \to (O (L (f)) \subseteq T \to \exists v \in T O (L (f)) = N (\{v\}))$
53		simp3	$⊢ ((φ \land f \in C) \land v \in T \land O (L (f)) = N (\{v\})) \to O (L (f)) = N (\{v\})$
54	23	3ad2ant1	$⊢ ((φ \land f \in C) \land v \in T \land O (L (f)) = N (\{v\})) \to U \in LMod$
55	25	3ad2ant1	$⊢ ((φ \land f \in C) \land v \in T \land O (L (f)) = N (\{v\})) \to T \in S$
56		simp2	$⊢ ((φ \land f \in C) \land v \in T \land O (L (f)) = N (\{v\})) \to v \in T$
57	3 4 54 55 56	lspsnel5a	$⊢ ((φ \land f \in C) \land v \in T \land O (L (f)) = N (\{v\})) \to N (\{v\}) \subseteq T$
58	53 57	eqsstrd	$⊢ ((φ \land f \in C) \land v \in T \land O (L (f)) = N (\{v\})) \to O (L (f)) \subseteq T$
59	58	rexlimdv3a	$⊢ (φ \land f \in C) \to (\exists v \in T O (L (f)) = N (\{v\}) \to O (L (f)) \subseteq T)$
60	52 59	impbid	$⊢ (φ \land f \in C) \to (O (L (f)) \subseteq T \leftrightarrow \exists v \in T O (L (f)) = N (\{v\}))$
61	60	rabbidva	$⊢ φ \to \{f \in C \| O (L (f)) \subseteq T\} = \{f \in C \| \exists v \in T O (L (f)) = N (\{v\})\}$
62	12 61	eqtrd	$⊢ φ \to M (T) = \{f \in C \| \exists v \in T O (L (f)) = N (\{v\})\}$

Metamath Proof Explorer

Theorem mapdval2N

Proof