hdmapval0

Description: Value of map from vectors to functionals at zero. Note: we use dvh3dim for convenience, even though 3 dimensions aren't necessary at this point. TODO: I think either this or hdmapeq0 could be derived from the other to shorten proof. (Contributed by NM, 17-May-2015)

	Ref	Expression
Hypotheses	hdmapval0.h	$⊢ H = LHyp (K)$
	hdmapval0.u	$⊢ U = DVecH (K) (W)$
	hdmapval0.o	$⊢ \underset{˙}{0} = 0_{U}$
	hdmapval0.c	$⊢ C = LCDual (K) (W)$
	hdmapval0.q	$⊢ Q = 0_{C}$
	hdmapval0.s	$⊢ S = HDMap (K) (W)$
	hdmapval0.k	$⊢ φ \to (K \in HL \land W \in H)$
Assertion	hdmapval0	$⊢ φ \to S (\underset{˙}{0}) = Q$

Proof

Step	Hyp	Ref	Expression
1		hdmapval0.h	$⊢ H = LHyp (K)$
2		hdmapval0.u	$⊢ U = DVecH (K) (W)$
3		hdmapval0.o	$⊢ \underset{˙}{0} = 0_{U}$
4		hdmapval0.c	$⊢ C = LCDual (K) (W)$
5		hdmapval0.q	$⊢ Q = 0_{C}$
6		hdmapval0.s	$⊢ S = HDMap (K) (W)$
7		hdmapval0.k	$⊢ φ \to (K \in HL \land W \in H)$
8		eqid	$⊢ {Base}_{U} = {Base}_{U}$
9		eqid	$⊢ LSpan (U) = LSpan (U)$
10		eqid	$⊢ {Base}_{K} = {Base}_{K}$
11		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
12		eqid	$⊢ ⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩ = ⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩$
13	1 10 11 2 8 3 12 7	dvheveccl	$⊢ φ \to ⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩ \in ({Base}_{U} ∖ \{\underset{˙}{0}\})$
14	13	eldifad	$⊢ φ \to ⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩ \in {Base}_{U}$
15	1 2 7	dvhlmod	$⊢ φ \to U \in LMod$
16	8 3	lmod0vcl	$⊢ U \in LMod \to \underset{˙}{0} \in {Base}_{U}$
17	15 16	syl	$⊢ φ \to \underset{˙}{0} \in {Base}_{U}$
18	1 2 8 9 7 14 17	dvh3dim	$⊢ φ \to \exists x \in {Base}_{U} \neg x \in LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, \underset{˙}{0}\})$
19		eqid	$⊢ {Base}_{C} = {Base}_{C}$
20		eqid	$⊢ HVMap (K) (W) = HVMap (K) (W)$
21		eqid	$⊢ HDMap1 (K) (W) = HDMap1 (K) (W)$
22	7	3ad2ant1	$⊢ (φ \land x \in {Base}_{U} \land \neg x \in LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, \underset{˙}{0}\})) \to (K \in HL \land W \in H)$
23	17	3ad2ant1	$⊢ (φ \land x \in {Base}_{U} \land \neg x \in LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, \underset{˙}{0}\})) \to \underset{˙}{0} \in {Base}_{U}$
24		simp2	$⊢ (φ \land x \in {Base}_{U} \land \neg x \in LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, \underset{˙}{0}\})) \to x \in {Base}_{U}$
25		eqid	$⊢ LSubSp (U) = LSubSp (U)$
26	8 25 9 15 14 17	lspprcl	$⊢ φ \to LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, \underset{˙}{0}\}) \in LSubSp (U)$
27	8 9 15 14 17	lspprid1	$⊢ φ \to ⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩ \in LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, \underset{˙}{0}\})$
28	25 9 15 26 27	ellspsn5	$⊢ φ \to LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩\}) \subseteq LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, \underset{˙}{0}\})$
29	8 9 15 14 17	lspprid2	$⊢ φ \to \underset{˙}{0} \in LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, \underset{˙}{0}\})$
30	25 9 15 26 29	ellspsn5	$⊢ φ \to LSpan (U) (\{\underset{˙}{0}\}) \subseteq LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, \underset{˙}{0}\})$
31	28 30	unssd	$⊢ φ \to LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩\}) \cup LSpan (U) (\{\underset{˙}{0}\}) \subseteq LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, \underset{˙}{0}\})$
32	31	ssneld	$⊢ φ \to (\neg x \in LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, \underset{˙}{0}\}) \to \neg x \in (LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩\}) \cup LSpan (U) (\{\underset{˙}{0}\})))$
33	32	adantr	$⊢ (φ \land x \in {Base}_{U}) \to (\neg x \in LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, \underset{˙}{0}\}) \to \neg x \in (LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩\}) \cup LSpan (U) (\{\underset{˙}{0}\})))$
34	33	3impia	$⊢ (φ \land x \in {Base}_{U} \land \neg x \in LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, \underset{˙}{0}\})) \to \neg x \in (LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩\}) \cup LSpan (U) (\{\underset{˙}{0}\}))$
35	1 12 2 8 9 4 19 20 21 6 22 23 24 34	hdmapval2	$⊢ (φ \land x \in {Base}_{U} \land \neg x \in LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, \underset{˙}{0}\})) \to S (\underset{˙}{0}) = HDMap1 (K) (W) (⟨x, HDMap1 (K) (W) (⟨⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, HVMap (K) (W) (⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩), x⟩), \underset{˙}{0}⟩)$
36		eqid	$⊢ LSpan (C) = LSpan (C)$
37		eqid	$⊢ mapd (K) (W) = mapd (K) (W)$
38	1 2 8 3 4 19 5 20 7 13	hvmapcl2	$⊢ φ \to HVMap (K) (W) (⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩) \in ({Base}_{C} ∖ \{Q\})$
39	38	eldifad	$⊢ φ \to HVMap (K) (W) (⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩) \in {Base}_{C}$
40	39	3ad2ant1	$⊢ (φ \land x \in {Base}_{U} \land \neg x \in LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, \underset{˙}{0}\})) \to HVMap (K) (W) (⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩) \in {Base}_{C}$
41	1 2 8 3 9 4 36 37 20 7 13	mapdhvmap	$⊢ φ \to mapd (K) (W) (LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩\})) = LSpan (C) (\{HVMap (K) (W) (⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩)\})$
42	41	3ad2ant1	$⊢ (φ \land x \in {Base}_{U} \land \neg x \in LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, \underset{˙}{0}\})) \to mapd (K) (W) (LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩\})) = LSpan (C) (\{HVMap (K) (W) (⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩)\})$
43	1 2 7	dvhlvec	$⊢ φ \to U \in LVec$
44	43	3ad2ant1	$⊢ (φ \land x \in {Base}_{U} \land \neg x \in LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, \underset{˙}{0}\})) \to U \in LVec$
45	14	3ad2ant1	$⊢ (φ \land x \in {Base}_{U} \land \neg x \in LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, \underset{˙}{0}\})) \to ⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩ \in {Base}_{U}$
46		simp3	$⊢ (φ \land x \in {Base}_{U} \land \neg x \in LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, \underset{˙}{0}\})) \to \neg x \in LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, \underset{˙}{0}\})$
47	8 9 44 24 45 23 46	lspindpi	$⊢ (φ \land x \in {Base}_{U} \land \neg x \in LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, \underset{˙}{0}\})) \to (LSpan (U) (\{x\}) \neq LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩\}) \land LSpan (U) (\{x\}) \neq LSpan (U) (\{\underset{˙}{0}\}))$
48	47	simpld	$⊢ (φ \land x \in {Base}_{U} \land \neg x \in LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, \underset{˙}{0}\})) \to LSpan (U) (\{x\}) \neq LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩\})$
49	48	necomd	$⊢ (φ \land x \in {Base}_{U} \land \neg x \in LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, \underset{˙}{0}\})) \to LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩\}) \neq LSpan (U) (\{x\})$
50	13	3ad2ant1	$⊢ (φ \land x \in {Base}_{U} \land \neg x \in LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, \underset{˙}{0}\})) \to ⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩ \in ({Base}_{U} ∖ \{\underset{˙}{0}\})$
51	1 2 8 3 9 4 19 36 37 21 22 40 42 49 50 24	hdmap1cl	$⊢ (φ \land x \in {Base}_{U} \land \neg x \in LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, \underset{˙}{0}\})) \to HDMap1 (K) (W) (⟨⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, HVMap (K) (W) (⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩), x⟩) \in {Base}_{C}$
52	1 2 8 3 4 19 5 21 22 51 24	hdmap1val0	$⊢ (φ \land x \in {Base}_{U} \land \neg x \in LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, \underset{˙}{0}\})) \to HDMap1 (K) (W) (⟨x, HDMap1 (K) (W) (⟨⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, HVMap (K) (W) (⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩), x⟩), \underset{˙}{0}⟩) = Q$
53	35 52	eqtrd	$⊢ (φ \land x \in {Base}_{U} \land \neg x \in LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, \underset{˙}{0}\})) \to S (\underset{˙}{0}) = Q$
54	53	rexlimdv3a	$⊢ φ \to (\exists x \in {Base}_{U} \neg x \in LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, \underset{˙}{0}\}) \to S (\underset{˙}{0}) = Q)$
55	18 54	mpd	$⊢ φ \to S (\underset{˙}{0}) = Q$

Metamath Proof Explorer

Theorem hdmapval0

Proof