hdmapval3N

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\})$
	hdmapval3.t	$⊢ φ \to T \in V$
Assertion	hdmapval3N	$⊢ φ \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		hdmapval3.t	$⊢ φ \to T \in V$
14		fveq2	$⊢ T = 0_{U} \to S (T) = S (0_{U})$
15		oteq3	$⊢ T = 0_{U} \to ⟨E, J (E), T⟩ = ⟨E, J (E), 0_{U}⟩$
16	15	fveq2d	$⊢ T = 0_{U} \to I (⟨E, J (E), T⟩) = I (⟨E, J (E), 0_{U}⟩)$
17	14 16	eqeq12d	$⊢ T = 0_{U} \to (S (T) = I (⟨E, J (E), T⟩) \leftrightarrow S (0_{U}) = I (⟨E, J (E), 0_{U}⟩))$
18		eqid	$⊢ {Base}_{K} = {Base}_{K}$
19		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
20		eqid	$⊢ 0_{U} = 0_{U}$
21	1 18 19 3 4 20 2 11	dvheveccl	$⊢ φ \to E \in (V ∖ \{0_{U}\})$
22	21	eldifad	$⊢ φ \to E \in V$
23	1 3 4 5 11 22 13	dvh3dim	$⊢ φ \to \exists x \in V \neg x \in N (\{E, T\})$
24	23	adantr	$⊢ (φ \land T \neq 0_{U}) \to \exists x \in V \neg x \in N (\{E, T\})$
25		simp1l	$⊢ ((φ \land T \neq 0_{U}) \land x \in V \land \neg x \in N (\{E, T\})) \to φ$
26	25 11	syl	$⊢ ((φ \land T \neq 0_{U}) \land x \in V \land \neg x \in N (\{E, T\})) \to (K \in HL \land W \in H)$
27	25 12	syl	$⊢ ((φ \land T \neq 0_{U}) \land x \in V \land \neg x \in N (\{E, T\})) \to N (\{T\}) \neq N (\{E\})$
28	25 13	syl	$⊢ ((φ \land T \neq 0_{U}) \land x \in V \land \neg x \in N (\{E, T\})) \to T \in V$
29		simp1r	$⊢ ((φ \land T \neq 0_{U}) \land x \in V \land \neg x \in N (\{E, T\})) \to T \neq 0_{U}$
30		eldifsn	$⊢ T \in (V ∖ \{0_{U}\}) \leftrightarrow (T \in V \land T \neq 0_{U})$
31	28 29 30	sylanbrc	$⊢ ((φ \land T \neq 0_{U}) \land x \in V \land \neg x \in N (\{E, T\})) \to T \in (V ∖ \{0_{U}\})$
32		simp2	$⊢ ((φ \land T \neq 0_{U}) \land x \in V \land \neg x \in N (\{E, T\})) \to x \in V$
33		simp3	$⊢ ((φ \land T \neq 0_{U}) \land x \in V \land \neg x \in N (\{E, T\})) \to \neg x \in N (\{E, T\})$
34	1 2 3 4 5 6 7 8 9 10 26 27 31 32 33	hdmapval3lemN	$⊢ ((φ \land T \neq 0_{U}) \land x \in V \land \neg x \in N (\{E, T\})) \to S (T) = I (⟨E, J (E), T⟩)$
35	34	rexlimdv3a	$⊢ (φ \land T \neq 0_{U}) \to (\exists x \in V \neg x \in N (\{E, T\}) \to S (T) = I (⟨E, J (E), T⟩))$
36	24 35	mpd	$⊢ (φ \land T \neq 0_{U}) \to S (T) = I (⟨E, J (E), T⟩)$
37		eqid	$⊢ 0_{C} = 0_{C}$
38	1 3 20 6 37 10 11	hdmapval0	$⊢ φ \to S (0_{U}) = 0_{C}$
39	1 3 4 20 6 7 37 8 11 21	hvmapcl2	$⊢ φ \to J (E) \in (D ∖ \{0_{C}\})$
40	39	eldifad	$⊢ φ \to J (E) \in D$
41	1 3 4 20 6 7 37 9 11 40 22	hdmap1val0	$⊢ φ \to I (⟨E, J (E), 0_{U}⟩) = 0_{C}$
42	38 41	eqtr4d	$⊢ φ \to S (0_{U}) = I (⟨E, J (E), 0_{U}⟩)$
43	17 36 42	pm2.61ne	$⊢ φ \to S (T) = I (⟨E, J (E), T⟩)$

Metamath Proof Explorer

Theorem hdmapval3N

Proof