hdmap1vallem

Description: Value of preliminary map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 15-May-2015)

	Ref	Expression
Hypotheses	hdmap1val.h	$⊢ H = LHyp (K)$
	hdmap1fval.u	$⊢ U = DVecH (K) (W)$
	hdmap1fval.v	$⊢ V = {Base}_{U}$
	hdmap1fval.s	$⊢ \underset{˙}{-} = -_{U}$
	hdmap1fval.o	$⊢ \underset{˙}{0} = 0_{U}$
	hdmap1fval.n	$⊢ N = LSpan (U)$
	hdmap1fval.c	$⊢ C = LCDual (K) (W)$
	hdmap1fval.d	$⊢ D = {Base}_{C}$
	hdmap1fval.r	$⊢ R = -_{C}$
	hdmap1fval.q	$⊢ Q = 0_{C}$
	hdmap1fval.j	$⊢ J = LSpan (C)$
	hdmap1fval.m	$⊢ M = mapd (K) (W)$
	hdmap1fval.i	$⊢ I = HDMap1 (K) (W)$
	hdmap1fval.k	$⊢ φ \to (K \in A \land W \in H)$
	hdmap1val.t	$⊢ φ \to T \in ((V \times D) \times V)$
Assertion	hdmap1vallem	$⊢ φ \to I (T) = if (2^{nd} (T) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (T)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (T)) \underset{˙}{-} 2^{nd} (T)\})) = J (\{2^{nd} (1^{st} (T)) R h\}))))$

Proof

Step	Hyp	Ref	Expression
1		hdmap1val.h	$⊢ H = LHyp (K)$
2		hdmap1fval.u	$⊢ U = DVecH (K) (W)$
3		hdmap1fval.v	$⊢ V = {Base}_{U}$
4		hdmap1fval.s	$⊢ \underset{˙}{-} = -_{U}$
5		hdmap1fval.o	$⊢ \underset{˙}{0} = 0_{U}$
6		hdmap1fval.n	$⊢ N = LSpan (U)$
7		hdmap1fval.c	$⊢ C = LCDual (K) (W)$
8		hdmap1fval.d	$⊢ D = {Base}_{C}$
9		hdmap1fval.r	$⊢ R = -_{C}$
10		hdmap1fval.q	$⊢ Q = 0_{C}$
11		hdmap1fval.j	$⊢ J = LSpan (C)$
12		hdmap1fval.m	$⊢ M = mapd (K) (W)$
13		hdmap1fval.i	$⊢ I = HDMap1 (K) (W)$
14		hdmap1fval.k	$⊢ φ \to (K \in A \land W \in H)$
15		hdmap1val.t	$⊢ φ \to T \in ((V \times D) \times V)$
16	1 2 3 4 5 6 7 8 9 10 11 12 13 14	hdmap1fval	$⊢ φ \to I = (x \in ((V \times D) \times V) ⟼ if (2^{nd} (x) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (x)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\})) = J (\{2^{nd} (1^{st} (x)) R h\})))))$
17	16	fveq1d	$⊢ φ \to I (T) = (x \in ((V \times D) \times V) ⟼ if (2^{nd} (x) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (x)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\})) = J (\{2^{nd} (1^{st} (x)) R h\}))))) (T)$
18	10	fvexi	$⊢ Q \in V$
19		riotaex	$⊢ (ι h \in D \| (M (N (\{2^{nd} (T)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (T)) \underset{˙}{-} 2^{nd} (T)\})) = J (\{2^{nd} (1^{st} (T)) R h\}))) \in V$
20	18 19	ifex	$⊢ if (2^{nd} (T) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (T)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (T)) \underset{˙}{-} 2^{nd} (T)\})) = J (\{2^{nd} (1^{st} (T)) R h\})))) \in V$
21		fveqeq2	$⊢ x = T \to (2^{nd} (x) = \underset{˙}{0} \leftrightarrow 2^{nd} (T) = \underset{˙}{0})$
22		fveq2	$⊢ x = T \to 2^{nd} (x) = 2^{nd} (T)$
23	22	sneqd	$⊢ x = T \to \{2^{nd} (x)\} = \{2^{nd} (T)\}$
24	23	fveq2d	$⊢ x = T \to N (\{2^{nd} (x)\}) = N (\{2^{nd} (T)\})$
25	24	fveqeq2d	$⊢ x = T \to (M (N (\{2^{nd} (x)\})) = J (\{h\}) \leftrightarrow M (N (\{2^{nd} (T)\})) = J (\{h\}))$
26		2fveq3	$⊢ x = T \to 1^{st} (1^{st} (x)) = 1^{st} (1^{st} (T))$
27	26 22	oveq12d	$⊢ x = T \to 1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x) = 1^{st} (1^{st} (T)) \underset{˙}{-} 2^{nd} (T)$
28	27	sneqd	$⊢ x = T \to \{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\} = \{1^{st} (1^{st} (T)) \underset{˙}{-} 2^{nd} (T)\}$
29	28	fveq2d	$⊢ x = T \to N (\{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\}) = N (\{1^{st} (1^{st} (T)) \underset{˙}{-} 2^{nd} (T)\})$
30	29	fveq2d	$⊢ x = T \to M (N (\{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\})) = M (N (\{1^{st} (1^{st} (T)) \underset{˙}{-} 2^{nd} (T)\}))$
31		2fveq3	$⊢ x = T \to 2^{nd} (1^{st} (x)) = 2^{nd} (1^{st} (T))$
32	31	oveq1d	$⊢ x = T \to 2^{nd} (1^{st} (x)) R h = 2^{nd} (1^{st} (T)) R h$
33	32	sneqd	$⊢ x = T \to \{2^{nd} (1^{st} (x)) R h\} = \{2^{nd} (1^{st} (T)) R h\}$
34	33	fveq2d	$⊢ x = T \to J (\{2^{nd} (1^{st} (x)) R h\}) = J (\{2^{nd} (1^{st} (T)) R h\})$
35	30 34	eqeq12d	$⊢ x = T \to (M (N (\{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\})) = J (\{2^{nd} (1^{st} (x)) R h\}) \leftrightarrow M (N (\{1^{st} (1^{st} (T)) \underset{˙}{-} 2^{nd} (T)\})) = J (\{2^{nd} (1^{st} (T)) R h\}))$
36	25 35	anbi12d	$⊢ x = T \to ((M (N (\{2^{nd} (x)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\})) = J (\{2^{nd} (1^{st} (x)) R h\})) \leftrightarrow (M (N (\{2^{nd} (T)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (T)) \underset{˙}{-} 2^{nd} (T)\})) = J (\{2^{nd} (1^{st} (T)) R h\})))$
37	36	riotabidv	$⊢ x = T \to (ι h \in D \| (M (N (\{2^{nd} (x)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\})) = J (\{2^{nd} (1^{st} (x)) R h\}))) = (ι h \in D \| (M (N (\{2^{nd} (T)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (T)) \underset{˙}{-} 2^{nd} (T)\})) = J (\{2^{nd} (1^{st} (T)) R h\})))$
38	21 37	ifbieq2d	$⊢ x = T \to if (2^{nd} (x) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (x)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\})) = J (\{2^{nd} (1^{st} (x)) R h\})))) = if (2^{nd} (T) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (T)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (T)) \underset{˙}{-} 2^{nd} (T)\})) = J (\{2^{nd} (1^{st} (T)) R h\}))))$
39		eqid	$⊢ (x \in ((V \times D) \times V) ⟼ if (2^{nd} (x) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (x)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\})) = J (\{2^{nd} (1^{st} (x)) R h\}))))) = (x \in ((V \times D) \times V) ⟼ if (2^{nd} (x) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (x)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\})) = J (\{2^{nd} (1^{st} (x)) R h\})))))$
40	38 39	fvmptg	$⊢ (T \in ((V \times D) \times V) \land if (2^{nd} (T) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (T)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (T)) \underset{˙}{-} 2^{nd} (T)\})) = J (\{2^{nd} (1^{st} (T)) R h\})))) \in V) \to (x \in ((V \times D) \times V) ⟼ if (2^{nd} (x) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (x)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\})) = J (\{2^{nd} (1^{st} (x)) R h\}))))) (T) = if (2^{nd} (T) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (T)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (T)) \underset{˙}{-} 2^{nd} (T)\})) = J (\{2^{nd} (1^{st} (T)) R h\}))))$
41	15 20 40	sylancl	$⊢ φ \to (x \in ((V \times D) \times V) ⟼ if (2^{nd} (x) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (x)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\})) = J (\{2^{nd} (1^{st} (x)) R h\}))))) (T) = if (2^{nd} (T) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (T)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (T)) \underset{˙}{-} 2^{nd} (T)\})) = J (\{2^{nd} (1^{st} (T)) R h\}))))$
42	17 41	eqtrd	$⊢ φ \to I (T) = if (2^{nd} (T) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (T)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (T)) \underset{˙}{-} 2^{nd} (T)\})) = J (\{2^{nd} (1^{st} (T)) R h\}))))$

Metamath Proof Explorer

Theorem hdmap1vallem

Proof