Theorem lshpkrlem2

Description: Lemma for lshpkrex . The value of tentative functional G is a scalar. (Contributed by NM, 16-Jul-2014)

	Ref	Expression
Hypotheses	lshpkrlem.v	$$⊢V={\mathrm{Base}}_W$$
	lshpkrlem.a	$$⊢\underset{\dot{}}{+}={+}_W$$
	lshpkrlem.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
	lshpkrlem.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(W\right)$$
	lshpkrlem.h	$$⊢H=\mathrm{LSHyp}\left(W\right)$$
	lshpkrlem.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lshpkrlem.u	$$⊢\phi \to U\in H$$
	lshpkrlem.z	$$⊢\phi \to Z\in V$$
	lshpkrlem.x	$$⊢\phi \to X\in V$$
	lshpkrlem.e	$$⊢\phi \to U\underset{\dot{}}{\oplus }N\left(\left\{Z\right\}\right)=V$$
	lshpkrlem.d	$$⊢D=\mathrm{Scalar}\left(W\right)$$
	lshpkrlem.k	$$⊢K={\mathrm{Base}}_D$$
	lshpkrlem.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	lshpkrlem.o	$$⊢\underset{\dot{}}{0}=0_D$$
	lshpkrlem.g	$$⊢G=\left(x\in V⟼\left(\iota k\in K|\exists y\in Ux=y\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\right)\right)$$
Assertion	lshpkrlem2	$$⊢\phi \to G\left(X\right)\in K$$

Proof

Step	Hyp	Ref	Expression
1		lshpkrlem.v	$$⊢V={\mathrm{Base}}_W$$
2		lshpkrlem.a	$$⊢\underset{\dot{}}{+}={+}_W$$
3		lshpkrlem.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
4		lshpkrlem.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(W\right)$$
5		lshpkrlem.h	$$⊢H=\mathrm{LSHyp}\left(W\right)$$
6		lshpkrlem.w	$$⊢\phi \to W\in \mathrm{LVec}$$
7		lshpkrlem.u	$$⊢\phi \to U\in H$$
8		lshpkrlem.z	$$⊢\phi \to Z\in V$$
9		lshpkrlem.x	$$⊢\phi \to X\in V$$
10		lshpkrlem.e	$$⊢\phi \to U\underset{\dot{}}{\oplus }N\left(\left\{Z\right\}\right)=V$$
11		lshpkrlem.d	$$⊢D=\mathrm{Scalar}\left(W\right)$$
12		lshpkrlem.k	$$⊢K={\mathrm{Base}}_D$$
13		lshpkrlem.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
14		lshpkrlem.o	$$⊢\underset{\dot{}}{0}=0_D$$
15		lshpkrlem.g	$$⊢G=\left(x\in V⟼\left(\iota k\in K|\exists y\in Ux=y\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\right)\right)$$
16		eqeq1	$$⊢x=X\to \left(x=y\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\leftrightarrow X=y\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\right)$$
17	16	rexbidv	$$⊢x=X\to \left(\exists y\in Ux=y\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\leftrightarrow \exists y\in UX=y\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\right)$$
18	17	riotabidv	$$⊢x=X\to \left(\iota k\in K|\exists y\in Ux=y\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\right)=\left(\iota k\in K|\exists y\in UX=y\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\right)$$
19		riotaex	$$⊢\left(\iota k\in K|\exists y\in UX=y\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\right)\in \mathrm{V}$$
20	18 15 19	fvmpt	$$⊢X\in V\to G\left(X\right)=\left(\iota k\in K|\exists y\in UX=y\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\right)$$
21	9 20	syl	$$⊢\phi \to G\left(X\right)=\left(\iota k\in K|\exists y\in UX=y\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\right)$$
22	1 2 3 4 5 6 7 8 9 10 11 12 13	lshpsmreu	$$⊢\phi \to \exists !k\in K\exists y\in UX=y\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)$$
23		riotacl	$$⊢\exists !k\in K\exists y\in UX=y\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\to \left(\iota k\in K|\exists y\in UX=y\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\right)\in K$$
24	22 23	syl	$$⊢\phi \to \left(\iota k\in K|\exists y\in UX=y\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\right)\in K$$
25	21 24	eqeltrd	$$⊢\phi \to G\left(X\right)\in K$$