Theorem hdmap1valc

Description: Connect the value of the preliminary map from vectors to functionals I to the hypothesis L used by earlier theorems. Note: the X e. ( V \ { .0. } ) hypothesis could be the more general X e. V but the former will be easier to use. TODO: use the I function directly in those theorems, so this theorem becomes unnecessary? TODO: The hdmap1cbv is probably unnecessary, but it would mean different $d's later on. (Contributed by NM, 15-May-2015)

	Ref	Expression
Hypotheses	hdmap1valc.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmap1valc.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmap1valc.v	$$⊢V={\mathrm{Base}}_U$$
	hdmap1valc.s	$$⊢\underset{\dot{}}{-}={-}_U$$
	hdmap1valc.o	$$⊢\underset{\dot{}}{0}=0_U$$
	hdmap1valc.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	hdmap1valc.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	hdmap1valc.d	$$⊢D={\mathrm{Base}}_C$$
	hdmap1valc.r	$$⊢R={-}_C$$
	hdmap1valc.q	$$⊢Q=0_C$$
	hdmap1valc.j	$$⊢J=\mathrm{LSpan}\left(C\right)$$
	hdmap1valc.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	hdmap1valc.i	$$⊢I=\mathrm{HDMap1}\left(K\right)\left(W\right)$$
	hdmap1valc.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmap1valc.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	hdmap1valc.f	$$⊢\phi \to F\in D$$
	hdmap1valc.y	$$⊢\phi \to Y\in V$$
	hdmap1valc.l	$$⊢L=\left(x\in \mathrm{V}⟼if\left(2^{nd}\left(x\right)=\underset{\dot{}}{0},Q,\left(\iota h\in D|\left(M\left(N\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(x\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}\right)\right)\right)\right)\right)$$
Assertion	hdmap1valc	$$⊢\phi \to I\left(⟨X,F,Y⟩\right)=L\left(⟨X,F,Y⟩\right)$$

Proof

Step	Hyp	Ref	Expression
1		hdmap1valc.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmap1valc.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hdmap1valc.v	$$⊢V={\mathrm{Base}}_U$$
4		hdmap1valc.s	$$⊢\underset{\dot{}}{-}={-}_U$$
5		hdmap1valc.o	$$⊢\underset{\dot{}}{0}=0_U$$
6		hdmap1valc.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
7		hdmap1valc.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
8		hdmap1valc.d	$$⊢D={\mathrm{Base}}_C$$
9		hdmap1valc.r	$$⊢R={-}_C$$
10		hdmap1valc.q	$$⊢Q=0_C$$
11		hdmap1valc.j	$$⊢J=\mathrm{LSpan}\left(C\right)$$
12		hdmap1valc.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
13		hdmap1valc.i	$$⊢I=\mathrm{HDMap1}\left(K\right)\left(W\right)$$
14		hdmap1valc.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
15		hdmap1valc.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
16		hdmap1valc.f	$$⊢\phi \to F\in D$$
17		hdmap1valc.y	$$⊢\phi \to Y\in V$$
18		hdmap1valc.l	$$⊢L=\left(x\in \mathrm{V}⟼if\left(2^{nd}\left(x\right)=\underset{\dot{}}{0},Q,\left(\iota h\in D|\left(M\left(N\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(x\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}\right)\right)\right)\right)\right)$$
19	15	eldifad	$$⊢\phi \to X\in V$$
20	1 2 3 4 5 6 7 8 9 10 11 12 13 14 19 16 17	hdmap1val	$$⊢\phi \to I\left(⟨X,F,Y⟩\right)=if\left(Y=\underset{\dot{}}{0},Q,\left(\iota g\in D|\left(M\left(N\left(\left\{Y\right\}\right)\right)=J\left(\left\{g\right\}\right)\wedge M\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\right)=J\left(\left\{FRg\right\}\right)\right)\right)\right)$$
21	18	hdmap1cbv	$$⊢L=\left(w\in \mathrm{V}⟼if\left(2^{nd}\left(w\right)=\underset{\dot{}}{0},Q,\left(\iota g\in D|\left(M\left(N\left(\left\{2^{nd}\left(w\right)\right\}\right)\right)=J\left(\left\{g\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(w\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(w\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(w\right)\right)Rg\right\}\right)\right)\right)\right)\right)$$
22	10 21 19 16 17	mapdhval	$$⊢\phi \to L\left(⟨X,F,Y⟩\right)=if\left(Y=\underset{\dot{}}{0},Q,\left(\iota g\in D|\left(M\left(N\left(\left\{Y\right\}\right)\right)=J\left(\left\{g\right\}\right)\wedge M\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\right)=J\left(\left\{FRg\right\}\right)\right)\right)\right)$$
23	20 22	eqtr4d	$$⊢\phi \to I\left(⟨X,F,Y⟩\right)=L\left(⟨X,F,Y⟩\right)$$