Theorem lshpkrlem3

Description: Lemma for lshpkrex . Defining property of GX . (Contributed by NM, 15-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	lshpkrlem3	$$⊢\phi \to \exists z\in UX=z\underset{\dot{}}{+}\left(G\left(X\right)\underset{\dot{}}{·}Z\right)$$

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	1 2 3 4 5 6 7 8 9 10 11 12 13	lshpsmreu	$$⊢\phi \to \exists !l\in K\exists z\in UX=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)$$
17		riotasbc	$$⊢\exists !l\in K\exists z\in UX=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)\to \underset{\dot{}}{[}\left(\iota l\in K|\exists z\in UX=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)\right)/l\underset{\dot{}}{]}\exists z\in UX=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)$$
18	16 17	syl	$$⊢\phi \to \underset{\dot{}}{[}\left(\iota l\in K|\exists z\in UX=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)\right)/l\underset{\dot{}}{]}\exists z\in UX=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)$$
19		eqeq1	$$⊢x=X\to \left(x=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)\leftrightarrow X=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)\right)$$
20	19	rexbidv	$$⊢x=X\to \left(\exists z\in Ux=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)\leftrightarrow \exists z\in UX=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)\right)$$
21	20	riotabidv	$$⊢x=X\to \left(\iota l\in K|\exists z\in Ux=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)\right)=\left(\iota l\in K|\exists z\in UX=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)\right)$$
22		oveq1	$$⊢k=l\to k\underset{\dot{}}{·}Z=l\underset{\dot{}}{·}Z$$
23	22	oveq2d	$$⊢k=l\to y\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)=y\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)$$
24	23	eqeq2d	$$⊢k=l\to \left(x=y\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\leftrightarrow x=y\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)\right)$$
25	24	rexbidv	$$⊢k=l\to \left(\exists y\in Ux=y\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\leftrightarrow \exists y\in Ux=y\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)\right)$$
26		oveq1	$$⊢y=z\to y\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)$$
27	26	eqeq2d	$$⊢y=z\to \left(x=y\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)\leftrightarrow x=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)\right)$$
28	27	cbvrexvw	$$⊢\exists y\in Ux=y\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)\leftrightarrow \exists z\in Ux=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)$$
29	25 28	bitrdi	$$⊢k=l\to \left(\exists y\in Ux=y\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\leftrightarrow \exists z\in Ux=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)\right)$$
30	29	cbvriotavw	$$⊢\left(\iota k\in K|\exists y\in Ux=y\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\right)=\left(\iota l\in K|\exists z\in Ux=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)\right)$$
31	30	mpteq2i	$$⊢\left(x\in V⟼\left(\iota k\in K|\exists y\in Ux=y\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\right)\right)=\left(x\in V⟼\left(\iota l\in K|\exists z\in Ux=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)\right)\right)$$
32	15 31	eqtri	$$⊢G=\left(x\in V⟼\left(\iota l\in K|\exists z\in Ux=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)\right)\right)$$
33		riotaex	$$⊢\left(\iota l\in K|\exists z\in UX=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)\right)\in \mathrm{V}$$
34	21 32 33	fvmpt	$$⊢X\in V\to G\left(X\right)=\left(\iota l\in K|\exists z\in UX=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)\right)$$
35		dfsbcq	$$⊢G\left(X\right)=\left(\iota l\in K|\exists z\in UX=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)\right)\to \left(\underset{\dot{}}{[}G\left(X\right)/l\underset{\dot{}}{]}\exists z\in UX=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)\leftrightarrow \underset{\dot{}}{[}\left(\iota l\in K|\exists z\in UX=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)\right)/l\underset{\dot{}}{]}\exists z\in UX=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)\right)$$
36	9 34 35	3syl	$$⊢\phi \to \left(\underset{\dot{}}{[}G\left(X\right)/l\underset{\dot{}}{]}\exists z\in UX=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)\leftrightarrow \underset{\dot{}}{[}\left(\iota l\in K|\exists z\in UX=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)\right)/l\underset{\dot{}}{]}\exists z\in UX=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)\right)$$
37	18 36	mpbird	$$⊢\phi \to \underset{\dot{}}{[}G\left(X\right)/l\underset{\dot{}}{]}\exists z\in UX=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)$$
38		fvex	$$⊢G\left(X\right)\in \mathrm{V}$$
39		oveq1	$$⊢l=G\left(X\right)\to l\underset{\dot{}}{·}Z=G\left(X\right)\underset{\dot{}}{·}Z$$
40	39	oveq2d	$$⊢l=G\left(X\right)\to z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)=z\underset{\dot{}}{+}\left(G\left(X\right)\underset{\dot{}}{·}Z\right)$$
41	40	eqeq2d	$$⊢l=G\left(X\right)\to \left(X=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)\leftrightarrow X=z\underset{\dot{}}{+}\left(G\left(X\right)\underset{\dot{}}{·}Z\right)\right)$$
42	41	rexbidv	$$⊢l=G\left(X\right)\to \left(\exists z\in UX=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)\leftrightarrow \exists z\in UX=z\underset{\dot{}}{+}\left(G\left(X\right)\underset{\dot{}}{·}Z\right)\right)$$
43	38 42	sbcie	$$⊢\underset{\dot{}}{[}G\left(X\right)/l\underset{\dot{}}{]}\exists z\in UX=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Z\right)\leftrightarrow \exists z\in UX=z\underset{\dot{}}{+}\left(G\left(X\right)\underset{\dot{}}{·}Z\right)$$
44	37 43	sylib	$$⊢\phi \to \exists z\in UX=z\underset{\dot{}}{+}\left(G\left(X\right)\underset{\dot{}}{·}Z\right)$$