Theorem lshpkrlem1

Description: Lemma for lshpkrex . The value of tentative functional G is zero iff its argument belongs to hyperplane U . (Contributed by NM, 14-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	lshpkrlem1	$$⊢\phi \to \left(X\in U\leftrightarrow G\left(X\right)=\underset{\dot{}}{0}\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		lveclmod	$$⊢W\in \mathrm{LVec}\to W\in \mathrm{LMod}$$
17	6 16	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
18	11	lmodfgrp	$$⊢W\in \mathrm{LMod}\to D\in \mathrm{Grp}$$
19	12 14	grpidcl	$$⊢D\in \mathrm{Grp}\to \underset{\dot{}}{0}\in K$$
20	17 18 19	3syl	$$⊢\phi \to \underset{\dot{}}{0}\in K$$
21	1 2 3 4 5 6 7 8 9 10 11 12 13	lshpsmreu	$$⊢\phi \to \exists !k\in K\exists b\in UX=b\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)$$
22		oveq1	$$⊢k=\underset{\dot{}}{0}\to k\underset{\dot{}}{·}Z=\underset{\dot{}}{0}\underset{\dot{}}{·}Z$$
23	22	oveq2d	$$⊢k=\underset{\dot{}}{0}\to b\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)=b\underset{\dot{}}{+}\left(\underset{\dot{}}{0}\underset{\dot{}}{·}Z\right)$$
24	23	eqeq2d	$$⊢k=\underset{\dot{}}{0}\to \left(X=b\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\leftrightarrow X=b\underset{\dot{}}{+}\left(\underset{\dot{}}{0}\underset{\dot{}}{·}Z\right)\right)$$
25	24	rexbidv	$$⊢k=\underset{\dot{}}{0}\to \left(\exists b\in UX=b\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\leftrightarrow \exists b\in UX=b\underset{\dot{}}{+}\left(\underset{\dot{}}{0}\underset{\dot{}}{·}Z\right)\right)$$
26	25	riota2	$$⊢\left(\underset{\dot{}}{0}\in K\wedge \exists !k\in K\exists b\in UX=b\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\right)\to \left(\exists b\in UX=b\underset{\dot{}}{+}\left(\underset{\dot{}}{0}\underset{\dot{}}{·}Z\right)\leftrightarrow \left(\iota k\in K|\exists b\in UX=b\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\right)=\underset{\dot{}}{0}\right)$$
27	20 21 26	syl2anc	$$⊢\phi \to \left(\exists b\in UX=b\underset{\dot{}}{+}\left(\underset{\dot{}}{0}\underset{\dot{}}{·}Z\right)\leftrightarrow \left(\iota k\in K|\exists b\in UX=b\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\right)=\underset{\dot{}}{0}\right)$$
28		simpr	$$⊢\left(\phi \wedge X\in U\right)\to X\in U$$
29		eqidd	$$⊢\left(\phi \wedge X\in U\right)\to X=X$$
30		eqeq2	$$⊢b=X\to \left(X=b\leftrightarrow X=X\right)$$
31	30	rspcev	$$⊢\left(X\in U\wedge X=X\right)\to \exists b\in UX=b$$
32	28 29 31	syl2anc	$$⊢\left(\phi \wedge X\in U\right)\to \exists b\in UX=b$$
33	32	ex	$$⊢\phi \to \left(X\in U\to \exists b\in UX=b\right)$$
34		eleq1a	$$⊢b\in U\to \left(X=b\to X\in U\right)$$
35	34	a1i	$$⊢\phi \to \left(b\in U\to \left(X=b\to X\in U\right)\right)$$
36	35	rexlimdv	$$⊢\phi \to \left(\exists b\in UX=b\to X\in U\right)$$
37	33 36	impbid	$$⊢\phi \to \left(X\in U\leftrightarrow \exists b\in UX=b\right)$$
38		eqid	$$⊢0_W=0_W$$
39	1 11 13 14 38	lmod0vs	$$⊢\left(W\in \mathrm{LMod}\wedge Z\in V\right)\to \underset{\dot{}}{0}\underset{\dot{}}{·}Z=0_W$$
40	17 8 39	syl2anc	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{·}Z=0_W$$
41	40	adantr	$$⊢\left(\phi \wedge b\in U\right)\to \underset{\dot{}}{0}\underset{\dot{}}{·}Z=0_W$$
42	41	oveq2d	$$⊢\left(\phi \wedge b\in U\right)\to b\underset{\dot{}}{+}\left(\underset{\dot{}}{0}\underset{\dot{}}{·}Z\right)=b\underset{\dot{}}{+}{0}_W$$
43	6	adantr	$$⊢\left(\phi \wedge b\in U\right)\to W\in \mathrm{LVec}$$
44	43 16	syl	$$⊢\left(\phi \wedge b\in U\right)\to W\in \mathrm{LMod}$$
45		eqid	$$⊢\mathrm{LSubSp}\left(W\right)=\mathrm{LSubSp}\left(W\right)$$
46	45 5 17 7	lshplss	$$⊢\phi \to U\in \mathrm{LSubSp}\left(W\right)$$
47	1 45	lssel	$$⊢\left(U\in \mathrm{LSubSp}\left(W\right)\wedge b\in U\right)\to b\in V$$
48	46 47	sylan	$$⊢\left(\phi \wedge b\in U\right)\to b\in V$$
49	1 2 38	lmod0vrid	$$⊢\left(W\in \mathrm{LMod}\wedge b\in V\right)\to b\underset{\dot{}}{+}{0}_W=b$$
50	44 48 49	syl2anc	$$⊢\left(\phi \wedge b\in U\right)\to b\underset{\dot{}}{+}{0}_W=b$$
51	42 50	eqtrd	$$⊢\left(\phi \wedge b\in U\right)\to b\underset{\dot{}}{+}\left(\underset{\dot{}}{0}\underset{\dot{}}{·}Z\right)=b$$
52	51	eqeq2d	$$⊢\left(\phi \wedge b\in U\right)\to \left(X=b\underset{\dot{}}{+}\left(\underset{\dot{}}{0}\underset{\dot{}}{·}Z\right)\leftrightarrow X=b\right)$$
53	52	bicomd	$$⊢\left(\phi \wedge b\in U\right)\to \left(X=b\leftrightarrow X=b\underset{\dot{}}{+}\left(\underset{\dot{}}{0}\underset{\dot{}}{·}Z\right)\right)$$
54	53	rexbidva	$$⊢\phi \to \left(\exists b\in UX=b\leftrightarrow \exists b\in UX=b\underset{\dot{}}{+}\left(\underset{\dot{}}{0}\underset{\dot{}}{·}Z\right)\right)$$
55	37 54	bitrd	$$⊢\phi \to \left(X\in U\leftrightarrow \exists b\in UX=b\underset{\dot{}}{+}\left(\underset{\dot{}}{0}\underset{\dot{}}{·}Z\right)\right)$$
56		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)$$
57	56	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)$$
58	57	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)$$
59		riotaex	$$⊢\left(\iota k\in K|\exists y\in UX=y\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\right)\in \mathrm{V}$$
60	58 15 59	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)$$
61		oveq1	$$⊢y=b\to y\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)=b\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)$$
62	61	eqeq2d	$$⊢y=b\to \left(X=y\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\leftrightarrow X=b\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\right)$$
63	62	cbvrexvw	$$⊢\exists y\in UX=y\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\leftrightarrow \exists b\in UX=b\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)$$
64	63	a1i	$$⊢k\in K\to \left(\exists y\in UX=y\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\leftrightarrow \exists b\in UX=b\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\right)$$
65	64	riotabiia	$$⊢\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 b\in UX=b\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\right)$$
66	60 65	eqtrdi	$$⊢X\in V\to G\left(X\right)=\left(\iota k\in K|\exists b\in UX=b\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\right)$$
67	9 66	syl	$$⊢\phi \to G\left(X\right)=\left(\iota k\in K|\exists b\in UX=b\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\right)$$
68	67	eqeq1d	$$⊢\phi \to \left(G\left(X\right)=\underset{\dot{}}{0}\leftrightarrow \left(\iota k\in K|\exists b\in UX=b\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}Z\right)\right)=\underset{\dot{}}{0}\right)$$
69	27 55 68	3bitr4d	$$⊢\phi \to \left(X\in U\leftrightarrow G\left(X\right)=\underset{\dot{}}{0}\right)$$