Theorem hvmapidN

Description: The value of the vector to functional map, at the vector, is one. (Contributed by NM, 23-Mar-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hvmapid.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hvmapid.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hvmapid.v	$$⊢V={\mathrm{Base}}_U$$
	hvmapid.z	$$⊢\underset{\dot{}}{0}=0_U$$
	hvmapid.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
	hvmapid.i	$$⊢\underset{\dot{}}{1}=1_S$$
	hvmapid.m	$$⊢M=\mathrm{HVMap}\left(K\right)\left(W\right)$$
	hvmapid.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hvmapid.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
Assertion	hvmapidN	$$⊢\phi \to M\left(X\right)\left(X\right)=\underset{\dot{}}{1}$$

Proof

Step	Hyp	Ref	Expression
1		hvmapid.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hvmapid.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hvmapid.v	$$⊢V={\mathrm{Base}}_U$$
4		hvmapid.z	$$⊢\underset{\dot{}}{0}=0_U$$
5		hvmapid.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
6		hvmapid.i	$$⊢\underset{\dot{}}{1}=1_S$$
7		hvmapid.m	$$⊢M=\mathrm{HVMap}\left(K\right)\left(W\right)$$
8		hvmapid.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
9		hvmapid.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
10		eqid	$$⊢\mathrm{ocH}\left(K\right)\left(W\right)=\mathrm{ocH}\left(K\right)\left(W\right)$$
11		eqid	$$⊢{+}_U={+}_U$$
12		eqid	$$⊢{\cdot }_U={\cdot }_U$$
13		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
14	1 2 10 3 11 12 4 5 13 7 8 9	hvmapval	$$⊢\phi \to M\left(X\right)=\left(v\in V⟼\left(\iota j\in {\mathrm{Base}}_S|\exists t\in \mathrm{ocH}\left(K\right)\left(W\right)\left(\left\{X\right\}\right)v=t{+}_U\left(j{\cdot }_{U}X\right)\right)\right)$$
15	14	fveq1d	$$⊢\phi \to M\left(X\right)\left(X\right)=\left(v\in V⟼\left(\iota j\in {\mathrm{Base}}_S|\exists t\in \mathrm{ocH}\left(K\right)\left(W\right)\left(\left\{X\right\}\right)v=t{+}_U\left(j{\cdot }_{U}X\right)\right)\right)\left(X\right)$$
16		eqid	$$⊢\left(v\in V⟼\left(\iota j\in {\mathrm{Base}}_S|\exists t\in \mathrm{ocH}\left(K\right)\left(W\right)\left(\left\{X\right\}\right)v=t{+}_U\left(j{\cdot }_{U}X\right)\right)\right)=\left(v\in V⟼\left(\iota j\in {\mathrm{Base}}_S|\exists t\in \mathrm{ocH}\left(K\right)\left(W\right)\left(\left\{X\right\}\right)v=t{+}_U\left(j{\cdot }_{U}X\right)\right)\right)$$
17	1 10 2 3 11 12 4 5 13 6 8 9 16	dochfl1	$$⊢\phi \to \left(v\in V⟼\left(\iota j\in {\mathrm{Base}}_S|\exists t\in \mathrm{ocH}\left(K\right)\left(W\right)\left(\left\{X\right\}\right)v=t{+}_U\left(j{\cdot }_{U}X\right)\right)\right)\left(X\right)=\underset{\dot{}}{1}$$
18	15 17	eqtrd	$$⊢\phi \to M\left(X\right)\left(X\right)=\underset{\dot{}}{1}$$