hdmap1val

Description: Value of preliminary map from vectors to functionals in the closed kernel dual space. (Restatement of mapdhval .) TODO: change I = ( x e. _V |-> ... to ( ph -> ( I<. X , F , Y > ) = ... in e.g. mapdh8 to shorten proofs with no $d on x . (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.x	$⊢ φ \to X \in V$
	hdmap1val.f	$⊢ φ \to F \in D$
	hdmap1val.y	$⊢ φ \to Y \in V$
Assertion	hdmap1val	$⊢ φ \to I (⟨X, F, Y⟩) = if (Y = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{F 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.x	$⊢ φ \to X \in V$
16		hdmap1val.f	$⊢ φ \to F \in D$
17		hdmap1val.y	$⊢ φ \to Y \in V$
18		df-ot	$⊢ ⟨X, F, Y⟩ = ⟨⟨X, F⟩, Y⟩$
19		opelxp	$⊢ ⟨X, F⟩ \in (V \times D) \leftrightarrow (X \in V \land F \in D)$
20	15 16 19	sylanbrc	$⊢ φ \to ⟨X, F⟩ \in (V \times D)$
21		opelxp	$⊢ ⟨⟨X, F⟩, Y⟩ \in ((V \times D) \times V) \leftrightarrow (⟨X, F⟩ \in (V \times D) \land Y \in V)$
22	20 17 21	sylanbrc	$⊢ φ \to ⟨⟨X, F⟩, Y⟩ \in ((V \times D) \times V)$
23	18 22	eqeltrid	$⊢ φ \to ⟨X, F, Y⟩ \in ((V \times D) \times V)$
24	1 2 3 4 5 6 7 8 9 10 11 12 13 14 23	hdmap1vallem	$⊢ φ \to I (⟨X, F, Y⟩) = if (2^{nd} (⟨X, F, Y⟩) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (⟨X, F, Y⟩)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (⟨X, F, Y⟩)) \underset{˙}{-} 2^{nd} (⟨X, F, Y⟩)\})) = J (\{2^{nd} (1^{st} (⟨X, F, Y⟩)) R h\}))))$
25		ot3rdg	$⊢ Y \in V \to 2^{nd} (⟨X, F, Y⟩) = Y$
26	17 25	syl	$⊢ φ \to 2^{nd} (⟨X, F, Y⟩) = Y$
27	26	eqeq1d	$⊢ φ \to (2^{nd} (⟨X, F, Y⟩) = \underset{˙}{0} \leftrightarrow Y = \underset{˙}{0})$
28	26	sneqd	$⊢ φ \to \{2^{nd} (⟨X, F, Y⟩)\} = \{Y\}$
29	28	fveq2d	$⊢ φ \to N (\{2^{nd} (⟨X, F, Y⟩)\}) = N (\{Y\})$
30	29	fveqeq2d	$⊢ φ \to (M (N (\{2^{nd} (⟨X, F, Y⟩)\})) = J (\{h\}) \leftrightarrow M (N (\{Y\})) = J (\{h\}))$
31		ot1stg	$⊢ (X \in V \land F \in D \land Y \in V) \to 1^{st} (1^{st} (⟨X, F, Y⟩)) = X$
32	15 16 17 31	syl3anc	$⊢ φ \to 1^{st} (1^{st} (⟨X, F, Y⟩)) = X$
33	32 26	oveq12d	$⊢ φ \to 1^{st} (1^{st} (⟨X, F, Y⟩)) \underset{˙}{-} 2^{nd} (⟨X, F, Y⟩) = X \underset{˙}{-} Y$
34	33	sneqd	$⊢ φ \to \{1^{st} (1^{st} (⟨X, F, Y⟩)) \underset{˙}{-} 2^{nd} (⟨X, F, Y⟩)\} = \{X \underset{˙}{-} Y\}$
35	34	fveq2d	$⊢ φ \to N (\{1^{st} (1^{st} (⟨X, F, Y⟩)) \underset{˙}{-} 2^{nd} (⟨X, F, Y⟩)\}) = N (\{X \underset{˙}{-} Y\})$
36	35	fveq2d	$⊢ φ \to M (N (\{1^{st} (1^{st} (⟨X, F, Y⟩)) \underset{˙}{-} 2^{nd} (⟨X, F, Y⟩)\})) = M (N (\{X \underset{˙}{-} Y\}))$
37		ot2ndg	$⊢ (X \in V \land F \in D \land Y \in V) \to 2^{nd} (1^{st} (⟨X, F, Y⟩)) = F$
38	15 16 17 37	syl3anc	$⊢ φ \to 2^{nd} (1^{st} (⟨X, F, Y⟩)) = F$
39	38	oveq1d	$⊢ φ \to 2^{nd} (1^{st} (⟨X, F, Y⟩)) R h = F R h$
40	39	sneqd	$⊢ φ \to \{2^{nd} (1^{st} (⟨X, F, Y⟩)) R h\} = \{F R h\}$
41	40	fveq2d	$⊢ φ \to J (\{2^{nd} (1^{st} (⟨X, F, Y⟩)) R h\}) = J (\{F R h\})$
42	36 41	eqeq12d	$⊢ φ \to (M (N (\{1^{st} (1^{st} (⟨X, F, Y⟩)) \underset{˙}{-} 2^{nd} (⟨X, F, Y⟩)\})) = J (\{2^{nd} (1^{st} (⟨X, F, Y⟩)) R h\}) \leftrightarrow M (N (\{X \underset{˙}{-} Y\})) = J (\{F R h\}))$
43	30 42	anbi12d	$⊢ φ \to ((M (N (\{2^{nd} (⟨X, F, Y⟩)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (⟨X, F, Y⟩)) \underset{˙}{-} 2^{nd} (⟨X, F, Y⟩)\})) = J (\{2^{nd} (1^{st} (⟨X, F, Y⟩)) R h\})) \leftrightarrow (M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{F R h\})))$
44	43	riotabidv	$⊢ φ \to (ι h \in D \| (M (N (\{2^{nd} (⟨X, F, Y⟩)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (⟨X, F, Y⟩)) \underset{˙}{-} 2^{nd} (⟨X, F, Y⟩)\})) = J (\{2^{nd} (1^{st} (⟨X, F, Y⟩)) R h\}))) = (ι h \in D \| (M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{F R h\})))$
45	27 44	ifbieq2d	$⊢ φ \to if (2^{nd} (⟨X, F, Y⟩) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (⟨X, F, Y⟩)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (⟨X, F, Y⟩)) \underset{˙}{-} 2^{nd} (⟨X, F, Y⟩)\})) = J (\{2^{nd} (1^{st} (⟨X, F, Y⟩)) R h\})))) = if (Y = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{F R h\}))))$
46	24 45	eqtrd	$⊢ φ \to I (⟨X, F, Y⟩) = if (Y = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{F R h\}))))$

Metamath Proof Explorer

Theorem hdmap1val

Proof