Theorem 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=\mathrm{LHyp}\left(K\right)$$
	hdmap1fval.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmap1fval.v	$$⊢V={\mathrm{Base}}_U$$
	hdmap1fval.s	$$⊢\underset{\dot{}}{-}={-}_U$$
	hdmap1fval.o	$$⊢\underset{\dot{}}{0}=0_U$$
	hdmap1fval.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	hdmap1fval.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	hdmap1fval.d	$$⊢D={\mathrm{Base}}_C$$
	hdmap1fval.r	$$⊢R={-}_C$$
	hdmap1fval.q	$$⊢Q=0_C$$
	hdmap1fval.j	$$⊢J=\mathrm{LSpan}\left(C\right)$$
	hdmap1fval.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	hdmap1fval.i	$$⊢I=\mathrm{HDMap1}\left(K\right)\left(W\right)$$
	hdmap1fval.k	$$⊢\phi \to \left(K\in A\wedge W\in H\right)$$
	hdmap1val.t	$$⊢\phi \to T\in \left(\left(V\times D\right)\times V\right)$$
Assertion	hdmap1vallem	$$⊢\phi \to I\left(T\right)=if\left(2^{nd}\left(T\right)=\underset{\dot{}}{0},Q,\left(\iota h\in D|\left(M\left(N\left(\left\{2^{nd}\left(T\right)\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(T\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(T\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)Rh\right\}\right)\right)\right)\right)$$

Proof

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