Theorem hdmap1val0

Description: Value of preliminary map from vectors to functionals at zero. (Restated mapdhval0 .) (Contributed by NM, 17-May-2015)

	Ref	Expression
Hypotheses	hdmap1val0.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmap1val0.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmap1val0.v	$$⊢V={\mathrm{Base}}_U$$
	hdmap1val0.o	$$⊢\underset{\dot{}}{0}=0_U$$
	hdmap1val0.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	hdmap1val0.d	$$⊢D={\mathrm{Base}}_C$$
	hdmap1val0.q	$$⊢Q=0_C$$
	hdmap1val0.s	$$⊢I=\mathrm{HDMap1}\left(K\right)\left(W\right)$$
	hdmap1val0.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmap1val0.f	$$⊢\phi \to F\in D$$
	hdmap1val0.x	$$⊢\phi \to X\in V$$
Assertion	hdmap1val0	$$⊢\phi \to I\left(⟨X,F,\underset{\dot{}}{0}⟩\right)=Q$$

Proof

Step	Hyp	Ref	Expression
1		hdmap1val0.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmap1val0.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hdmap1val0.v	$$⊢V={\mathrm{Base}}_U$$
4		hdmap1val0.o	$$⊢\underset{\dot{}}{0}=0_U$$
5		hdmap1val0.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
6		hdmap1val0.d	$$⊢D={\mathrm{Base}}_C$$
7		hdmap1val0.q	$$⊢Q=0_C$$
8		hdmap1val0.s	$$⊢I=\mathrm{HDMap1}\left(K\right)\left(W\right)$$
9		hdmap1val0.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
10		hdmap1val0.f	$$⊢\phi \to F\in D$$
11		hdmap1val0.x	$$⊢\phi \to X\in V$$
12		eqid	$$⊢{-}_U={-}_U$$
13		eqid	$$⊢\mathrm{LSpan}\left(U\right)=\mathrm{LSpan}\left(U\right)$$
14		eqid	$$⊢{-}_C={-}_C$$
15		eqid	$$⊢\mathrm{LSpan}\left(C\right)=\mathrm{LSpan}\left(C\right)$$
16		eqid	$$⊢\mathrm{mapd}\left(K\right)\left(W\right)=\mathrm{mapd}\left(K\right)\left(W\right)$$
17	1 2 9	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
18	3 4	lmod0vcl	$$⊢U\in \mathrm{LMod}\to \underset{\dot{}}{0}\in V$$
19	17 18	syl	$$⊢\phi \to \underset{\dot{}}{0}\in V$$
20	1 2 3 12 4 13 5 6 14 7 15 16 8 9 11 10 19	hdmap1val	$$⊢\phi \to I\left(⟨X,F,\underset{\dot{}}{0}⟩\right)=if\left(\underset{\dot{}}{0}=\underset{\dot{}}{0},Q,\left(\iota h\in D|\left(\mathrm{mapd}\left(K\right)\left(W\right)\left(\mathrm{LSpan}\left(U\right)\left(\left\{\underset{\dot{}}{0}\right\}\right)\right)=\mathrm{LSpan}\left(C\right)\left(\left\{h\right\}\right)\wedge \mathrm{mapd}\left(K\right)\left(W\right)\left(\mathrm{LSpan}\left(U\right)\left(\left\{X{-}_U\underset{\dot{}}{0}\right\}\right)\right)=\mathrm{LSpan}\left(C\right)\left(\left\{F{-}_{C}h\right\}\right)\right)\right)\right)$$
21		eqid	$$⊢\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
22	21	iftruei	$$⊢if\left(\underset{\dot{}}{0}=\underset{\dot{}}{0},Q,\left(\iota h\in D|\left(\mathrm{mapd}\left(K\right)\left(W\right)\left(\mathrm{LSpan}\left(U\right)\left(\left\{\underset{\dot{}}{0}\right\}\right)\right)=\mathrm{LSpan}\left(C\right)\left(\left\{h\right\}\right)\wedge \mathrm{mapd}\left(K\right)\left(W\right)\left(\mathrm{LSpan}\left(U\right)\left(\left\{X{-}_U\underset{\dot{}}{0}\right\}\right)\right)=\mathrm{LSpan}\left(C\right)\left(\left\{F{-}_{C}h\right\}\right)\right)\right)\right)=Q$$
23	20 22	eqtrdi	$$⊢\phi \to I\left(⟨X,F,\underset{\dot{}}{0}⟩\right)=Q$$