Theorem dochfl1

Description: The value of the explicit functional G is 1 at the X that determines it. (Contributed by NM, 27-Oct-2014)

	Ref	Expression
Hypotheses	dochfl1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dochfl1.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
	dochfl1.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dochfl1.v	$$⊢V={\mathrm{Base}}_U$$
	dochfl1.a	$$⊢\underset{\dot{}}{+}={+}_U$$
	dochfl1.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
	dochfl1.z	$$⊢\underset{\dot{}}{0}=0_U$$
	dochfl1.d	$$⊢D=\mathrm{Scalar}\left(U\right)$$
	dochfl1.r	$$⊢R={\mathrm{Base}}_D$$
	dochfl1.i	$$⊢\underset{\dot{}}{1}=1_D$$
	dochfl1.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	dochfl1.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	dochfl1.g	$$⊢G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}X\right)\right)\right)$$
Assertion	dochfl1	$$⊢\phi \to G\left(X\right)=\underset{\dot{}}{1}$$

Proof

Step	Hyp	Ref	Expression
1		dochfl1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dochfl1.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		dochfl1.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		dochfl1.v	$$⊢V={\mathrm{Base}}_U$$
5		dochfl1.a	$$⊢\underset{\dot{}}{+}={+}_U$$
6		dochfl1.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
7		dochfl1.z	$$⊢\underset{\dot{}}{0}=0_U$$
8		dochfl1.d	$$⊢D=\mathrm{Scalar}\left(U\right)$$
9		dochfl1.r	$$⊢R={\mathrm{Base}}_D$$
10		dochfl1.i	$$⊢\underset{\dot{}}{1}=1_D$$
11		dochfl1.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
12		dochfl1.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
13		dochfl1.g	$$⊢G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}X\right)\right)\right)$$
14	12	eldifad	$$⊢\phi \to X\in V$$
15		eqeq1	$$⊢v=X\to \left(v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}X\right)\leftrightarrow X=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}X\right)\right)$$
16	15	rexbidv	$$⊢v=X\to \left(\exists w\in \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}X\right)\leftrightarrow \exists w\in \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)X=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}X\right)\right)$$
17	16	riotabidv	$$⊢v=X\to \left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}X\right)\right)=\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)X=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}X\right)\right)$$
18		riotaex	$$⊢\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)X=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}X\right)\right)\in \mathrm{V}$$
19	17 13 18	fvmpt	$$⊢X\in V\to G\left(X\right)=\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)X=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}X\right)\right)$$
20	14 19	syl	$$⊢\phi \to G\left(X\right)=\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)X=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}X\right)\right)$$
21	1 3 11	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
22	14	snssd	$$⊢\phi \to \left\{X\right\}\subseteq V$$
23		eqid	$$⊢\mathrm{LSubSp}\left(U\right)=\mathrm{LSubSp}\left(U\right)$$
24	1 3 4 23 2	dochlss	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left\{X\right\}\subseteq V\right)\to \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\in \mathrm{LSubSp}\left(U\right)$$
25	11 22 24	syl2anc	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\in \mathrm{LSubSp}\left(U\right)$$
26	7 23	lss0cl	$$⊢\left(U\in \mathrm{LMod}\wedge \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\in \mathrm{LSubSp}\left(U\right)\right)\to \underset{\dot{}}{0}\in \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$
27	21 25 26	syl2anc	$$⊢\phi \to \underset{\dot{}}{0}\in \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$
28	4 8 6 10	lmodvs1	$$⊢\left(U\in \mathrm{LMod}\wedge X\in V\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}X=X$$
29	21 14 28	syl2anc	$$⊢\phi \to \underset{\dot{}}{1}\underset{\dot{}}{·}X=X$$
30	29	oveq2d	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}X\right)=\underset{\dot{}}{0}\underset{\dot{}}{+}X$$
31	4 5 7	lmod0vlid	$$⊢\left(U\in \mathrm{LMod}\wedge X\in V\right)\to \underset{\dot{}}{0}\underset{\dot{}}{+}X=X$$
32	21 14 31	syl2anc	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{+}X=X$$
33	30 32	eqtr2d	$$⊢\phi \to X=\underset{\dot{}}{0}\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}X\right)$$
34		oveq1	$$⊢w=\underset{\dot{}}{0}\to w\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}X\right)=\underset{\dot{}}{0}\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}X\right)$$
35	34	rspceeqv	$$⊢\left(\underset{\dot{}}{0}\in \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\wedge X=\underset{\dot{}}{0}\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}X\right)\right)\to \exists w\in \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)X=w\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}X\right)$$
36	27 33 35	syl2anc	$$⊢\phi \to \exists w\in \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)X=w\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}X\right)$$
37	8	lmodring	$$⊢U\in \mathrm{LMod}\to D\in \mathrm{Ring}$$
38	9 10	ringidcl	$$⊢D\in \mathrm{Ring}\to \underset{\dot{}}{1}\in R$$
39	21 37 38	3syl	$$⊢\phi \to \underset{\dot{}}{1}\in R$$
40		eqid	$$⊢\mathrm{LSpan}\left(U\right)=\mathrm{LSpan}\left(U\right)$$
41		eqid	$$⊢\mathrm{LSSum}\left(U\right)=\mathrm{LSSum}\left(U\right)$$
42		eqid	$$⊢\mathrm{LSHyp}\left(U\right)=\mathrm{LSHyp}\left(U\right)$$
43	1 3 11	dvhlvec	$$⊢\phi \to U\in \mathrm{LVec}$$
44	1 2 3 4 7 42 11 12	dochsnshp	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\in \mathrm{LSHyp}\left(U\right)$$
45	1 2 3 4 7 40 41 11 12	dochexmidat	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\mathrm{LSSum}\left(U\right)\mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)=V$$
46	4 5 40 41 42 43 44 14 14 45 8 9 6	lshpsmreu	$$⊢\phi \to \exists !k\in R\exists w\in \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)X=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}X\right)$$
47		oveq1	$$⊢k=\underset{\dot{}}{1}\to k\underset{\dot{}}{·}X=\underset{\dot{}}{1}\underset{\dot{}}{·}X$$
48	47	oveq2d	$$⊢k=\underset{\dot{}}{1}\to w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}X\right)=w\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}X\right)$$
49	48	eqeq2d	$$⊢k=\underset{\dot{}}{1}\to \left(X=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}X\right)\leftrightarrow X=w\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}X\right)\right)$$
50	49	rexbidv	$$⊢k=\underset{\dot{}}{1}\to \left(\exists w\in \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)X=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}X\right)\leftrightarrow \exists w\in \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)X=w\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}X\right)\right)$$
51	50	riota2	$$⊢\left(\underset{\dot{}}{1}\in R\wedge \exists !k\in R\exists w\in \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)X=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}X\right)\right)\to \left(\exists w\in \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)X=w\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}X\right)\leftrightarrow \left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)X=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}X\right)\right)=\underset{\dot{}}{1}\right)$$
52	39 46 51	syl2anc	$$⊢\phi \to \left(\exists w\in \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)X=w\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}X\right)\leftrightarrow \left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)X=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}X\right)\right)=\underset{\dot{}}{1}\right)$$
53	36 52	mpbid	$$⊢\phi \to \left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)X=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}X\right)\right)=\underset{\dot{}}{1}$$
54	20 53	eqtrd	$$⊢\phi \to G\left(X\right)=\underset{\dot{}}{1}$$