hdmaplkr

Description: Kernel of the vector to dual map. Line 16 in Holland95 p. 14. TODO: eliminate F hypothesis. (Contributed by NM, 9-Jun-2015)

	Ref	Expression
Hypotheses	hdmaplkr.h	$⊢ H = LHyp (K)$
	hdmaplkr.o	$⊢ O = ocH (K) (W)$
	hdmaplkr.u	$⊢ U = DVecH (K) (W)$
	hdmaplkr.v	$⊢ V = {Base}_{U}$
	hdmaplkr.f	$⊢ F = LFnl (U)$
	hdmaplkr.y	$⊢ Y = LKer (U)$
	hdmaplkr.s	$⊢ S = HDMap (K) (W)$
	hdmaplkr.k	$⊢ φ \to (K \in HL \land W \in H)$
	hdmaplkr.x	$⊢ φ \to X \in V$
Assertion	hdmaplkr	$⊢ φ \to Y (S (X)) = O (\{X\})$

Proof

Step	Hyp	Ref	Expression
1		hdmaplkr.h	$⊢ H = LHyp (K)$
2		hdmaplkr.o	$⊢ O = ocH (K) (W)$
3		hdmaplkr.u	$⊢ U = DVecH (K) (W)$
4		hdmaplkr.v	$⊢ V = {Base}_{U}$
5		hdmaplkr.f	$⊢ F = LFnl (U)$
6		hdmaplkr.y	$⊢ Y = LKer (U)$
7		hdmaplkr.s	$⊢ S = HDMap (K) (W)$
8		hdmaplkr.k	$⊢ φ \to (K \in HL \land W \in H)$
9		hdmaplkr.x	$⊢ φ \to X \in V$
10		fveq2	$⊢ X = 0_{U} \to S (X) = S (0_{U})$
11	10	fveq2d	$⊢ X = 0_{U} \to Y (S (X)) = Y (S (0_{U}))$
12		sneq	$⊢ X = 0_{U} \to \{X\} = \{0_{U}\}$
13	12	fveq2d	$⊢ X = 0_{U} \to O (\{X\}) = O (\{0_{U}\})$
14	11 13	sseq12d	$⊢ X = 0_{U} \to (Y (S (X)) \subseteq O (\{X\}) \leftrightarrow Y (S (0_{U})) \subseteq O (\{0_{U}\}))$
15		eqid	$⊢ LCDual (K) (W) = LCDual (K) (W)$
16	1 15 8	lcdlmod	$⊢ φ \to LCDual (K) (W) \in LMod$
17		eqid	$⊢ {Base}_{LCDual (K) (W)} = {Base}_{LCDual (K) (W)}$
18	1 3 4 15 17 7 8 9	hdmapcl	$⊢ φ \to S (X) \in {Base}_{LCDual (K) (W)}$
19		eqid	$⊢ LSpan (LCDual (K) (W)) = LSpan (LCDual (K) (W))$
20	17 19	lspsnid	$⊢ (LCDual (K) (W) \in LMod \land S (X) \in {Base}_{LCDual (K) (W)}) \to S (X) \in LSpan (LCDual (K) (W)) (\{S (X)\})$
21	16 18 20	syl2anc	$⊢ φ \to S (X) \in LSpan (LCDual (K) (W)) (\{S (X)\})$
22		eqid	$⊢ LSpan (U) = LSpan (U)$
23		eqid	$⊢ mapd (K) (W) = mapd (K) (W)$
24	1 3 4 22 15 19 23 7 8 9	hdmap10	$⊢ φ \to mapd (K) (W) (LSpan (U) (\{X\})) = LSpan (LCDual (K) (W)) (\{S (X)\})$
25		eqid	$⊢ LFnl (U) = LFnl (U)$
26	1 2 23 3 4 22 25 6 8 9	mapdsn	$⊢ φ \to mapd (K) (W) (LSpan (U) (\{X\})) = \{f \in LFnl (U) \| O (\{X\}) \subseteq Y (f)\}$
27	24 26	eqtr3d	$⊢ φ \to LSpan (LCDual (K) (W)) (\{S (X)\}) = \{f \in LFnl (U) \| O (\{X\}) \subseteq Y (f)\}$
28	21 27	eleqtrd	$⊢ φ \to S (X) \in \{f \in LFnl (U) \| O (\{X\}) \subseteq Y (f)\}$
29	1 15 17 3 25 8 18	lcdvbaselfl	$⊢ φ \to S (X) \in LFnl (U)$
30		fveq2	$⊢ f = S (X) \to Y (f) = Y (S (X))$
31	30	sseq2d	$⊢ f = S (X) \to (O (\{X\}) \subseteq Y (f) \leftrightarrow O (\{X\}) \subseteq Y (S (X)))$
32	31	elrab3	$⊢ S (X) \in LFnl (U) \to (S (X) \in \{f \in LFnl (U) \| O (\{X\}) \subseteq Y (f)\} \leftrightarrow O (\{X\}) \subseteq Y (S (X)))$
33	29 32	syl	$⊢ φ \to (S (X) \in \{f \in LFnl (U) \| O (\{X\}) \subseteq Y (f)\} \leftrightarrow O (\{X\}) \subseteq Y (S (X)))$
34	28 33	mpbid	$⊢ φ \to O (\{X\}) \subseteq Y (S (X))$
35	34	adantr	$⊢ (φ \land X \neq 0_{U}) \to O (\{X\}) \subseteq Y (S (X))$
36		eqid	$⊢ LSHyp (U) = LSHyp (U)$
37	1 3 8	dvhlvec	$⊢ φ \to U \in LVec$
38	37	adantr	$⊢ (φ \land X \neq 0_{U}) \to U \in LVec$
39		eqid	$⊢ 0_{U} = 0_{U}$
40	8	adantr	$⊢ (φ \land X \neq 0_{U}) \to (K \in HL \land W \in H)$
41	9	anim1i	$⊢ (φ \land X \neq 0_{U}) \to (X \in V \land X \neq 0_{U})$
42		eldifsn	$⊢ X \in (V ∖ \{0_{U}\}) \leftrightarrow (X \in V \land X \neq 0_{U})$
43	41 42	sylibr	$⊢ (φ \land X \neq 0_{U}) \to X \in (V ∖ \{0_{U}\})$
44	1 2 3 4 39 36 40 43	dochsnshp	$⊢ (φ \land X \neq 0_{U}) \to O (\{X\}) \in LSHyp (U)$
45	29	adantr	$⊢ (φ \land X \neq 0_{U}) \to S (X) \in LFnl (U)$
46		eqid	$⊢ Scalar (U) = Scalar (U)$
47		eqid	$⊢ 0_{Scalar (U)} = 0_{Scalar (U)}$
48		eqid	$⊢ 0_{LCDual (K) (W)} = 0_{LCDual (K) (W)}$
49	1 3 4 46 47 15 48 8	lcd0v	$⊢ φ \to 0_{LCDual (K) (W)} = V \times \{0_{Scalar (U)}\}$
50	49	eqeq2d	$⊢ φ \to (S (X) = 0_{LCDual (K) (W)} \leftrightarrow S (X) = V \times \{0_{Scalar (U)}\})$
51	1 3 4 39 15 48 7 8 9	hdmapeq0	$⊢ φ \to (S (X) = 0_{LCDual (K) (W)} \leftrightarrow X = 0_{U})$
52	50 51	bitr3d	$⊢ φ \to (S (X) = V \times \{0_{Scalar (U)}\} \leftrightarrow X = 0_{U})$
53	52	necon3bid	$⊢ φ \to (S (X) \neq V \times \{0_{Scalar (U)}\} \leftrightarrow X \neq 0_{U})$
54	53	biimpar	$⊢ (φ \land X \neq 0_{U}) \to S (X) \neq V \times \{0_{Scalar (U)}\}$
55	4 46 47 36 25 6	lkrshp	$⊢ (U \in LVec \land S (X) \in LFnl (U) \land S (X) \neq V \times \{0_{Scalar (U)}\}) \to Y (S (X)) \in LSHyp (U)$
56	38 45 54 55	syl3anc	$⊢ (φ \land X \neq 0_{U}) \to Y (S (X)) \in LSHyp (U)$
57	36 38 44 56	lshpcmp	$⊢ (φ \land X \neq 0_{U}) \to (O (\{X\}) \subseteq Y (S (X)) \leftrightarrow O (\{X\}) = Y (S (X)))$
58	35 57	mpbid	$⊢ (φ \land X \neq 0_{U}) \to O (\{X\}) = Y (S (X))$
59		eqimss2	$⊢ O (\{X\}) = Y (S (X)) \to Y (S (X)) \subseteq O (\{X\})$
60	58 59	syl	$⊢ (φ \land X \neq 0_{U}) \to Y (S (X)) \subseteq O (\{X\})$
61	1 3 8	dvhlmod	$⊢ φ \to U \in LMod$
62	4 39	lmod0vcl	$⊢ U \in LMod \to 0_{U} \in V$
63	61 62	syl	$⊢ φ \to 0_{U} \in V$
64	1 3 4 15 17 7 8 63	hdmapcl	$⊢ φ \to S (0_{U}) \in {Base}_{LCDual (K) (W)}$
65	1 15 17 3 25 8 64	lcdvbaselfl	$⊢ φ \to S (0_{U}) \in LFnl (U)$
66	4 25 6 61 65	lkrssv	$⊢ φ \to Y (S (0_{U})) \subseteq V$
67	1 3 2 4 39	doch0	$⊢ (K \in HL \land W \in H) \to O (\{0_{U}\}) = V$
68	8 67	syl	$⊢ φ \to O (\{0_{U}\}) = V$
69	66 68	sseqtrrd	$⊢ φ \to Y (S (0_{U})) \subseteq O (\{0_{U}\})$
70	14 60 69	pm2.61ne	$⊢ φ \to Y (S (X)) \subseteq O (\{X\})$
71	70 34	eqssd	$⊢ φ \to Y (S (X)) = O (\{X\})$

Metamath Proof Explorer

Theorem hdmaplkr

Proof