Theorem hvmapval

Description: Value of map from nonzero vectors to nonzero functionals in the closed kernel dual space. (Contributed by NM, 23-Mar-2015)

	Ref	Expression
Hypotheses	hvmapval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hvmapval.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hvmapval.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
	hvmapval.v	$$⊢V={\mathrm{Base}}_U$$
	hvmapval.p	$$⊢\underset{\dot{}}{+}={+}_U$$
	hvmapval.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
	hvmapval.z	$$⊢\underset{\dot{}}{0}=0_U$$
	hvmapval.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
	hvmapval.r	$$⊢R={\mathrm{Base}}_S$$
	hvmapval.m	$$⊢M=\mathrm{HVMap}\left(K\right)\left(W\right)$$
	hvmapval.k	$$⊢\phi \to \left(K\in A\wedge W\in H\right)$$
	hvmapval.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
Assertion	hvmapval	$$⊢\phi \to M\left(X\right)=\left(v\in V⟼\left(\iota j\in R|\exists t\in O\left(\left\{X\right\}\right)v=t\underset{\dot{}}{+}\left(j\underset{\dot{}}{·}X\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		hvmapval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hvmapval.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hvmapval.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
4		hvmapval.v	$$⊢V={\mathrm{Base}}_U$$
5		hvmapval.p	$$⊢\underset{\dot{}}{+}={+}_U$$
6		hvmapval.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
7		hvmapval.z	$$⊢\underset{\dot{}}{0}=0_U$$
8		hvmapval.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
9		hvmapval.r	$$⊢R={\mathrm{Base}}_S$$
10		hvmapval.m	$$⊢M=\mathrm{HVMap}\left(K\right)\left(W\right)$$
11		hvmapval.k	$$⊢\phi \to \left(K\in A\wedge W\in H\right)$$
12		hvmapval.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
13	1 2 3 4 5 6 7 8 9 10 11	hvmapfval	$$⊢\phi \to M=\left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼\left(v\in V⟼\left(\iota j\in R|\exists t\in O\left(\left\{x\right\}\right)v=t\underset{\dot{}}{+}\left(j\underset{\dot{}}{·}x\right)\right)\right)\right)$$
14	13	fveq1d	$$⊢\phi \to M\left(X\right)=\left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼\left(v\in V⟼\left(\iota j\in R|\exists t\in O\left(\left\{x\right\}\right)v=t\underset{\dot{}}{+}\left(j\underset{\dot{}}{·}x\right)\right)\right)\right)\left(X\right)$$
15	4	fvexi	$$⊢V\in \mathrm{V}$$
16	15	mptex	$$⊢\left(v\in V⟼\left(\iota j\in R|\exists t\in O\left(\left\{X\right\}\right)v=t\underset{\dot{}}{+}\left(j\underset{\dot{}}{·}X\right)\right)\right)\in \mathrm{V}$$
17		sneq	$$⊢x=X\to \left\{x\right\}=\left\{X\right\}$$
18	17	fveq2d	$$⊢x=X\to O\left(\left\{x\right\}\right)=O\left(\left\{X\right\}\right)$$
19		oveq2	$$⊢x=X\to j\underset{\dot{}}{·}x=j\underset{\dot{}}{·}X$$
20	19	oveq2d	$$⊢x=X\to t\underset{\dot{}}{+}\left(j\underset{\dot{}}{·}x\right)=t\underset{\dot{}}{+}\left(j\underset{\dot{}}{·}X\right)$$
21	20	eqeq2d	$$⊢x=X\to \left(v=t\underset{\dot{}}{+}\left(j\underset{\dot{}}{·}x\right)\leftrightarrow v=t\underset{\dot{}}{+}\left(j\underset{\dot{}}{·}X\right)\right)$$
22	18 21	rexeqbidv	$$⊢x=X\to \left(\exists t\in O\left(\left\{x\right\}\right)v=t\underset{\dot{}}{+}\left(j\underset{\dot{}}{·}x\right)\leftrightarrow \exists t\in O\left(\left\{X\right\}\right)v=t\underset{\dot{}}{+}\left(j\underset{\dot{}}{·}X\right)\right)$$
23	22	riotabidv	$$⊢x=X\to \left(\iota j\in R|\exists t\in O\left(\left\{x\right\}\right)v=t\underset{\dot{}}{+}\left(j\underset{\dot{}}{·}x\right)\right)=\left(\iota j\in R|\exists t\in O\left(\left\{X\right\}\right)v=t\underset{\dot{}}{+}\left(j\underset{\dot{}}{·}X\right)\right)$$
24	23	mpteq2dv	$$⊢x=X\to \left(v\in V⟼\left(\iota j\in R|\exists t\in O\left(\left\{x\right\}\right)v=t\underset{\dot{}}{+}\left(j\underset{\dot{}}{·}x\right)\right)\right)=\left(v\in V⟼\left(\iota j\in R|\exists t\in O\left(\left\{X\right\}\right)v=t\underset{\dot{}}{+}\left(j\underset{\dot{}}{·}X\right)\right)\right)$$
25		eqid	$$⊢\left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼\left(v\in V⟼\left(\iota j\in R|\exists t\in O\left(\left\{x\right\}\right)v=t\underset{\dot{}}{+}\left(j\underset{\dot{}}{·}x\right)\right)\right)\right)=\left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼\left(v\in V⟼\left(\iota j\in R|\exists t\in O\left(\left\{x\right\}\right)v=t\underset{\dot{}}{+}\left(j\underset{\dot{}}{·}x\right)\right)\right)\right)$$
26	24 25	fvmptg	$$⊢\left(X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge \left(v\in V⟼\left(\iota j\in R|\exists t\in O\left(\left\{X\right\}\right)v=t\underset{\dot{}}{+}\left(j\underset{\dot{}}{·}X\right)\right)\right)\in \mathrm{V}\right)\to \left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼\left(v\in V⟼\left(\iota j\in R|\exists t\in O\left(\left\{x\right\}\right)v=t\underset{\dot{}}{+}\left(j\underset{\dot{}}{·}x\right)\right)\right)\right)\left(X\right)=\left(v\in V⟼\left(\iota j\in R|\exists t\in O\left(\left\{X\right\}\right)v=t\underset{\dot{}}{+}\left(j\underset{\dot{}}{·}X\right)\right)\right)$$
27	12 16 26	sylancl	$$⊢\phi \to \left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼\left(v\in V⟼\left(\iota j\in R|\exists t\in O\left(\left\{x\right\}\right)v=t\underset{\dot{}}{+}\left(j\underset{\dot{}}{·}x\right)\right)\right)\right)\left(X\right)=\left(v\in V⟼\left(\iota j\in R|\exists t\in O\left(\left\{X\right\}\right)v=t\underset{\dot{}}{+}\left(j\underset{\dot{}}{·}X\right)\right)\right)$$
28	14 27	eqtrd	$$⊢\phi \to M\left(X\right)=\left(v\in V⟼\left(\iota j\in R|\exists t\in O\left(\left\{X\right\}\right)v=t\underset{\dot{}}{+}\left(j\underset{\dot{}}{·}X\right)\right)\right)$$