hdmapval3lemN

Description: Value of map from vectors to functionals at arguments not colinear with the reference vector E . (Contributed by NM, 17-May-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hdmapval3.h	$⊢ H = LHyp (K)$
	hdmapval3.e	$⊢ E = ⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩$
	hdmapval3.u	$⊢ U = DVecH (K) (W)$
	hdmapval3.v	$⊢ V = {Base}_{U}$
	hdmapval3.n	$⊢ N = LSpan (U)$
	hdmapval3.c	$⊢ C = LCDual (K) (W)$
	hdmapval3.d	$⊢ D = {Base}_{C}$
	hdmapval3.j	$⊢ J = HVMap (K) (W)$
	hdmapval3.i	$⊢ I = HDMap1 (K) (W)$
	hdmapval3.s	$⊢ S = HDMap (K) (W)$
	hdmapval3.k	$⊢ φ \to (K \in HL \land W \in H)$
	hdmapval3.te	$⊢ φ \to N (\{T\}) \neq N (\{E\})$
	hdmapval3lem.t	$⊢ φ \to T \in (V ∖ \{0_{U}\})$
	hdmapval3lem.x	$⊢ φ \to x \in V$
	hdmapval3lem.xn	$⊢ φ \to \neg x \in N (\{E, T\})$
Assertion	hdmapval3lemN	$⊢ φ \to S (T) = I (⟨E, J (E), T⟩)$

Proof

Step	Hyp	Ref	Expression
1		hdmapval3.h	$⊢ H = LHyp (K)$
2		hdmapval3.e	$⊢ E = ⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩$
3		hdmapval3.u	$⊢ U = DVecH (K) (W)$
4		hdmapval3.v	$⊢ V = {Base}_{U}$
5		hdmapval3.n	$⊢ N = LSpan (U)$
6		hdmapval3.c	$⊢ C = LCDual (K) (W)$
7		hdmapval3.d	$⊢ D = {Base}_{C}$
8		hdmapval3.j	$⊢ J = HVMap (K) (W)$
9		hdmapval3.i	$⊢ I = HDMap1 (K) (W)$
10		hdmapval3.s	$⊢ S = HDMap (K) (W)$
11		hdmapval3.k	$⊢ φ \to (K \in HL \land W \in H)$
12		hdmapval3.te	$⊢ φ \to N (\{T\}) \neq N (\{E\})$
13		hdmapval3lem.t	$⊢ φ \to T \in (V ∖ \{0_{U}\})$
14		hdmapval3lem.x	$⊢ φ \to x \in V$
15		hdmapval3lem.xn	$⊢ φ \to \neg x \in N (\{E, T\})$
16		eqid	$⊢ 0_{U} = 0_{U}$
17		eqid	$⊢ LSpan (C) = LSpan (C)$
18		eqid	$⊢ mapd (K) (W) = mapd (K) (W)$
19		eqid	$⊢ 0_{C} = 0_{C}$
20		eqid	$⊢ {Base}_{K} = {Base}_{K}$
21		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
22	1 20 21 3 4 16 2 11	dvheveccl	$⊢ φ \to E \in (V ∖ \{0_{U}\})$
23	1 3 4 16 6 7 19 8 11 22	hvmapcl2	$⊢ φ \to J (E) \in (D ∖ \{0_{C}\})$
24	23	eldifad	$⊢ φ \to J (E) \in D$
25	1 3 4 16 5 6 17 18 8 11 22	mapdhvmap	$⊢ φ \to mapd (K) (W) (N (\{E\})) = LSpan (C) (\{J (E)\})$
26	1 3 11	dvhlvec	$⊢ φ \to U \in LVec$
27	22	eldifad	$⊢ φ \to E \in V$
28	13	eldifad	$⊢ φ \to T \in V$
29	4 5 26 14 27 28 15	lspindpi	$⊢ φ \to (N (\{x\}) \neq N (\{E\}) \land N (\{x\}) \neq N (\{T\}))$
30	29	simpld	$⊢ φ \to N (\{x\}) \neq N (\{E\})$
31	30	necomd	$⊢ φ \to N (\{E\}) \neq N (\{x\})$
32	1 3 4 16 5 6 7 17 18 9 11 24 25 31 22 14	hdmap1cl	$⊢ φ \to I (⟨E, J (E), x⟩) \in D$
33		eqidd	$⊢ φ \to I (⟨E, J (E), x⟩) = I (⟨E, J (E), x⟩)$
34		eqid	$⊢ -_{U} = -_{U}$
35		eqid	$⊢ -_{C} = -_{C}$
36		eqid	$⊢ LSubSp (U) = LSubSp (U)$
37	1 3 11	dvhlmod	$⊢ φ \to U \in LMod$
38	4 36 5 37 27 28	lspprcl	$⊢ φ \to N (\{E, T\}) \in LSubSp (U)$
39	16 36 37 38 14 15	lssneln0	$⊢ φ \to x \in (V ∖ \{0_{U}\})$
40	1 3 4 34 16 5 6 7 35 17 18 9 11 22 24 39 32 31 25	hdmap1eq	$⊢ φ \to (I (⟨E, J (E), x⟩) = I (⟨E, J (E), x⟩) \leftrightarrow (mapd (K) (W) (N (\{x\})) = LSpan (C) (\{I (⟨E, J (E), x⟩)\}) \land mapd (K) (W) (N (\{E -_{U} x\})) = LSpan (C) (\{J (E) -_{C} I (⟨E, J (E), x⟩)\})))$
41	33 40	mpbid	$⊢ φ \to (mapd (K) (W) (N (\{x\})) = LSpan (C) (\{I (⟨E, J (E), x⟩)\}) \land mapd (K) (W) (N (\{E -_{U} x\})) = LSpan (C) (\{J (E) -_{C} I (⟨E, J (E), x⟩)\}))$
42	41	simpld	$⊢ φ \to mapd (K) (W) (N (\{x\})) = LSpan (C) (\{I (⟨E, J (E), x⟩)\})$
43	12	necomd	$⊢ φ \to N (\{E\}) \neq N (\{T\})$
44	4 5 37 27 28	lspprid1	$⊢ φ \to E \in N (\{E, T\})$
45	36 5 37 38 44	ellspsn5	$⊢ φ \to N (\{E\}) \subseteq N (\{E, T\})$
46	45 45	unssd	$⊢ φ \to N (\{E\}) \cup N (\{E\}) \subseteq N (\{E, T\})$
47	46 15	ssneldd	$⊢ φ \to \neg x \in (N (\{E\}) \cup N (\{E\}))$
48	1 2 3 4 5 6 7 8 9 10 11 27 14 47	hdmapval2	$⊢ φ \to S (E) = I (⟨x, I (⟨E, J (E), x⟩), E⟩)$
49	1 2 8 10 11	hdmapevec	$⊢ φ \to S (E) = J (E)$
50	48 49	eqtr3d	$⊢ φ \to I (⟨x, I (⟨E, J (E), x⟩), E⟩) = J (E)$
51	4 5 37 27 28	lspprid2	$⊢ φ \to T \in N (\{E, T\})$
52	36 5 37 38 51	ellspsn5	$⊢ φ \to N (\{T\}) \subseteq N (\{E, T\})$
53	45 52	unssd	$⊢ φ \to N (\{E\}) \cup N (\{T\}) \subseteq N (\{E, T\})$
54	53 15	ssneldd	$⊢ φ \to \neg x \in (N (\{E\}) \cup N (\{T\}))$
55	1 2 3 4 5 6 7 8 9 10 11 28 14 54	hdmapval2	$⊢ φ \to S (T) = I (⟨x, I (⟨E, J (E), x⟩), T⟩)$
56	55	eqcomd	$⊢ φ \to I (⟨x, I (⟨E, J (E), x⟩), T⟩) = S (T)$
57	1 3 4 16 5 6 7 17 18 9 11 32 42 39 22 13 43 15 50 56	hdmap1eq4N	$⊢ φ \to I (⟨E, J (E), T⟩) = S (T)$
58	57	eqcomd	$⊢ φ \to S (T) = I (⟨E, J (E), T⟩)$

Metamath Proof Explorer

Theorem hdmapval3lemN

Proof