Theorem hdmap1val2

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

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

Proof

Step	Hyp	Ref	Expression
1		hdmap1val2.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmap1val2.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hdmap1val2.v	$$⊢V={\mathrm{Base}}_U$$
4		hdmap1val2.s	$$⊢\underset{\dot{}}{-}={-}_U$$
5		hdmap1val2.o	$$⊢\underset{\dot{}}{0}=0_U$$
6		hdmap1val2.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
7		hdmap1val2.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
8		hdmap1val2.d	$$⊢D={\mathrm{Base}}_C$$
9		hdmap1val2.r	$$⊢R={-}_C$$
10		hdmap1val2.l	$$⊢L=\mathrm{LSpan}\left(C\right)$$
11		hdmap1val2.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
12		hdmap1val2.i	$$⊢I=\mathrm{HDMap1}\left(K\right)\left(W\right)$$
13		hdmap1val2.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
14		hdmap1val2.x	$$⊢\phi \to X\in V$$
15		hdmap1val2.f	$$⊢\phi \to F\in D$$
16		hdmap1val2.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
17		eqid	$$⊢0_C=0_C$$
18	16	eldifad	$$⊢\phi \to Y\in V$$
19	1 2 3 4 5 6 7 8 9 17 10 11 12 13 14 15 18	hdmap1val	$$⊢\phi \to I\left(⟨X,F,Y⟩\right)=if\left(Y=\underset{\dot{}}{0},0_C,\left(\iota h\in D|\left(M\left(N\left(\left\{Y\right\}\right)\right)=L\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\right)=L\left(\left\{FRh\right\}\right)\right)\right)\right)$$
20		eldifsni	$$⊢Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to Y\ne \underset{\dot{}}{0}$$
21	20	neneqd	$$⊢Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to \neg Y=\underset{\dot{}}{0}$$
22		iffalse	$$⊢\neg Y=\underset{\dot{}}{0}\to if\left(Y=\underset{\dot{}}{0},0_C,\left(\iota h\in D|\left(M\left(N\left(\left\{Y\right\}\right)\right)=L\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\right)=L\left(\left\{FRh\right\}\right)\right)\right)\right)=\left(\iota h\in D|\left(M\left(N\left(\left\{Y\right\}\right)\right)=L\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\right)=L\left(\left\{FRh\right\}\right)\right)\right)$$
23	16 21 22	3syl	$$⊢\phi \to if\left(Y=\underset{\dot{}}{0},0_C,\left(\iota h\in D|\left(M\left(N\left(\left\{Y\right\}\right)\right)=L\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\right)=L\left(\left\{FRh\right\}\right)\right)\right)\right)=\left(\iota h\in D|\left(M\left(N\left(\left\{Y\right\}\right)\right)=L\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\right)=L\left(\left\{FRh\right\}\right)\right)\right)$$
24	19 23	eqtrd	$$⊢\phi \to I\left(⟨X,F,Y⟩\right)=\left(\iota h\in D|\left(M\left(N\left(\left\{Y\right\}\right)\right)=L\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\right)=L\left(\left\{FRh\right\}\right)\right)\right)$$