Theorem frlmup2

Description: The evaluation map has the intended behavior on the unit vectors. (Contributed by Stefan O'Rear, 7-Feb-2015) (Proof shortened by AV, 21-Jul-2019)

	Ref	Expression
Hypotheses	frlmup.f	$$⊢F=R\mathrm{freeLMod}I$$
	frlmup.b	$$⊢B={\mathrm{Base}}_F$$
	frlmup.c	$$⊢C={\mathrm{Base}}_T$$
	frlmup.v	$$⊢\underset{\dot{}}{·}={\cdot }_T$$
	frlmup.e	$$⊢E=\left(x\in B⟼{\sum }_T\left(x{\underset{\dot{}}{·}}_{f}A\right)\right)$$
	frlmup.t	$$⊢\phi \to T\in \mathrm{LMod}$$
	frlmup.i	$$⊢\phi \to I\in X$$
	frlmup.r	$$⊢\phi \to R=\mathrm{Scalar}\left(T\right)$$
	frlmup.a	$$⊢\phi \to A:I⟶C$$
	frlmup.y	$$⊢\phi \to Y\in I$$
	frlmup.u	$$⊢U=R\mathrm{unitVec}I$$
Assertion	frlmup2	$$⊢\phi \to E\left(U\left(Y\right)\right)=A\left(Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		frlmup.f	$$⊢F=R\mathrm{freeLMod}I$$
2		frlmup.b	$$⊢B={\mathrm{Base}}_F$$
3		frlmup.c	$$⊢C={\mathrm{Base}}_T$$
4		frlmup.v	$$⊢\underset{\dot{}}{·}={\cdot }_T$$
5		frlmup.e	$$⊢E=\left(x\in B⟼{\sum }_T\left(x{\underset{\dot{}}{·}}_{f}A\right)\right)$$
6		frlmup.t	$$⊢\phi \to T\in \mathrm{LMod}$$
7		frlmup.i	$$⊢\phi \to I\in X$$
8		frlmup.r	$$⊢\phi \to R=\mathrm{Scalar}\left(T\right)$$
9		frlmup.a	$$⊢\phi \to A:I⟶C$$
10		frlmup.y	$$⊢\phi \to Y\in I$$
11		frlmup.u	$$⊢U=R\mathrm{unitVec}I$$
12		eqid	$$⊢\mathrm{Scalar}\left(T\right)=\mathrm{Scalar}\left(T\right)$$
13	12	lmodring	$$⊢T\in \mathrm{LMod}\to \mathrm{Scalar}\left(T\right)\in \mathrm{Ring}$$
14	6 13	syl	$$⊢\phi \to \mathrm{Scalar}\left(T\right)\in \mathrm{Ring}$$
15	8 14	eqeltrd	$$⊢\phi \to R\in \mathrm{Ring}$$
16	11 1 2	uvcff	$$⊢\left(R\in \mathrm{Ring}\wedge I\in X\right)\to U:I⟶B$$
17	15 7 16	syl2anc	$$⊢\phi \to U:I⟶B$$
18	17 10	ffvelrnd	$$⊢\phi \to U\left(Y\right)\in B$$
19		oveq1	$$⊢x=U\left(Y\right)\to x{\underset{\dot{}}{·}}_{f}A=U\left(Y\right){\underset{\dot{}}{·}}_{f}A$$
20	19	oveq2d	$$⊢x=U\left(Y\right)\to {\sum }_T\left(x{\underset{\dot{}}{·}}_{f}A\right)={\sum }_T\left(U\left(Y\right){\underset{\dot{}}{·}}_{f}A\right)$$
21		ovex	$$⊢{\sum }_T\left(U\left(Y\right){\underset{\dot{}}{·}}_{f}A\right)\in \mathrm{V}$$
22	20 5 21	fvmpt	$$⊢U\left(Y\right)\in B\to E\left(U\left(Y\right)\right)={\sum }_T\left(U\left(Y\right){\underset{\dot{}}{·}}_{f}A\right)$$
23	18 22	syl	$$⊢\phi \to E\left(U\left(Y\right)\right)={\sum }_T\left(U\left(Y\right){\underset{\dot{}}{·}}_{f}A\right)$$
24		eqid	$$⊢0_T=0_T$$
25		lmodcmn	$$⊢T\in \mathrm{LMod}\to T\in \mathrm{CMnd}$$
26		cmnmnd	$$⊢T\in \mathrm{CMnd}\to T\in \mathrm{Mnd}$$
27	6 25 26	3syl	$$⊢\phi \to T\in \mathrm{Mnd}$$
28		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(T\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(T\right)}$$
29		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
30	1 29 2	frlmbasf	$$⊢\left(I\in X\wedge U\left(Y\right)\in B\right)\to U\left(Y\right):I⟶{\mathrm{Base}}_R$$
31	7 18 30	syl2anc	$$⊢\phi \to U\left(Y\right):I⟶{\mathrm{Base}}_R$$
32	8	fveq2d	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(T\right)}$$
33	32	feq3d	$$⊢\phi \to \left(U\left(Y\right):I⟶{\mathrm{Base}}_R\leftrightarrow U\left(Y\right):I⟶{\mathrm{Base}}_{\mathrm{Scalar}\left(T\right)}\right)$$
34	31 33	mpbid	$$⊢\phi \to U\left(Y\right):I⟶{\mathrm{Base}}_{\mathrm{Scalar}\left(T\right)}$$
35	12 28 4 3 6 34 9 7	lcomf	$$⊢\phi \to \left(U\left(Y\right){\underset{\dot{}}{·}}_{f}A\right):I⟶C$$
36	31	ffnd	$$⊢\phi \to U\left(Y\right)FnI$$
37	36	adantr	$$⊢\left(\phi \wedge x\in \left(I\setminus \left\{Y\right\}\right)\right)\to U\left(Y\right)FnI$$
38	9	ffnd	$$⊢\phi \to AFnI$$
39	38	adantr	$$⊢\left(\phi \wedge x\in \left(I\setminus \left\{Y\right\}\right)\right)\to AFnI$$
40	7	adantr	$$⊢\left(\phi \wedge x\in \left(I\setminus \left\{Y\right\}\right)\right)\to I\in X$$
41		eldifi	$$⊢x\in \left(I\setminus \left\{Y\right\}\right)\to x\in I$$
42	41	adantl	$$⊢\left(\phi \wedge x\in \left(I\setminus \left\{Y\right\}\right)\right)\to x\in I$$
43		fnfvof	$$⊢\left(\left(U\left(Y\right)FnI\wedge AFnI\right)\wedge \left(I\in X\wedge x\in I\right)\right)\to \left(U\left(Y\right){\underset{\dot{}}{·}}_{f}A\right)\left(x\right)=U\left(Y\right)\left(x\right)\underset{\dot{}}{·}A\left(x\right)$$
44	37 39 40 42 43	syl22anc	$$⊢\left(\phi \wedge x\in \left(I\setminus \left\{Y\right\}\right)\right)\to \left(U\left(Y\right){\underset{\dot{}}{·}}_{f}A\right)\left(x\right)=U\left(Y\right)\left(x\right)\underset{\dot{}}{·}A\left(x\right)$$
45	15	adantr	$$⊢\left(\phi \wedge x\in \left(I\setminus \left\{Y\right\}\right)\right)\to R\in \mathrm{Ring}$$
46	10	adantr	$$⊢\left(\phi \wedge x\in \left(I\setminus \left\{Y\right\}\right)\right)\to Y\in I$$
47		eldifsni	$$⊢x\in \left(I\setminus \left\{Y\right\}\right)\to x\ne Y$$
48	47	necomd	$$⊢x\in \left(I\setminus \left\{Y\right\}\right)\to Y\ne x$$
49	48	adantl	$$⊢\left(\phi \wedge x\in \left(I\setminus \left\{Y\right\}\right)\right)\to Y\ne x$$
50		eqid	$$⊢0_R=0_R$$
51	11 45 40 46 42 49 50	uvcvv0	$$⊢\left(\phi \wedge x\in \left(I\setminus \left\{Y\right\}\right)\right)\to U\left(Y\right)\left(x\right)=0_R$$
52	8	fveq2d	$$⊢\phi \to 0_R=0_{\mathrm{Scalar}\left(T\right)}$$
53	52	adantr	$$⊢\left(\phi \wedge x\in \left(I\setminus \left\{Y\right\}\right)\right)\to 0_R=0_{\mathrm{Scalar}\left(T\right)}$$
54	51 53	eqtrd	$$⊢\left(\phi \wedge x\in \left(I\setminus \left\{Y\right\}\right)\right)\to U\left(Y\right)\left(x\right)=0_{\mathrm{Scalar}\left(T\right)}$$
55	54	oveq1d	$$⊢\left(\phi \wedge x\in \left(I\setminus \left\{Y\right\}\right)\right)\to U\left(Y\right)\left(x\right)\underset{\dot{}}{·}A\left(x\right)=0_{\mathrm{Scalar}\left(T\right)}\underset{\dot{}}{·}A\left(x\right)$$
56	6	adantr	$$⊢\left(\phi \wedge x\in \left(I\setminus \left\{Y\right\}\right)\right)\to T\in \mathrm{LMod}$$
57		ffvelrn	$$⊢\left(A:I⟶C\wedge x\in I\right)\to A\left(x\right)\in C$$
58	9 41 57	syl2an	$$⊢\left(\phi \wedge x\in \left(I\setminus \left\{Y\right\}\right)\right)\to A\left(x\right)\in C$$
59		eqid	$$⊢0_{\mathrm{Scalar}\left(T\right)}=0_{\mathrm{Scalar}\left(T\right)}$$
60	3 12 4 59 24	lmod0vs	$$⊢\left(T\in \mathrm{LMod}\wedge A\left(x\right)\in C\right)\to 0_{\mathrm{Scalar}\left(T\right)}\underset{\dot{}}{·}A\left(x\right)=0_T$$
61	56 58 60	syl2anc	$$⊢\left(\phi \wedge x\in \left(I\setminus \left\{Y\right\}\right)\right)\to 0_{\mathrm{Scalar}\left(T\right)}\underset{\dot{}}{·}A\left(x\right)=0_T$$
62	44 55 61	3eqtrd	$$⊢\left(\phi \wedge x\in \left(I\setminus \left\{Y\right\}\right)\right)\to \left(U\left(Y\right){\underset{\dot{}}{·}}_{f}A\right)\left(x\right)=0_T$$
63	35 62	suppss	$$⊢\phi \to \left(U\left(Y\right){\underset{\dot{}}{·}}_{f}A\right)\mathrm{supp}{0}_T\subseteq \left\{Y\right\}$$
64	3 24 27 7 10 35 63	gsumpt	$$⊢\phi \to {\sum }_T\left(U\left(Y\right){\underset{\dot{}}{·}}_{f}A\right)=\left(U\left(Y\right){\underset{\dot{}}{·}}_{f}A\right)\left(Y\right)$$
65		fnfvof	$$⊢\left(\left(U\left(Y\right)FnI\wedge AFnI\right)\wedge \left(I\in X\wedge Y\in I\right)\right)\to \left(U\left(Y\right){\underset{\dot{}}{·}}_{f}A\right)\left(Y\right)=U\left(Y\right)\left(Y\right)\underset{\dot{}}{·}A\left(Y\right)$$
66	36 38 7 10 65	syl22anc	$$⊢\phi \to \left(U\left(Y\right){\underset{\dot{}}{·}}_{f}A\right)\left(Y\right)=U\left(Y\right)\left(Y\right)\underset{\dot{}}{·}A\left(Y\right)$$
67		eqid	$$⊢1_R=1_R$$
68	11 15 7 10 67	uvcvv1	$$⊢\phi \to U\left(Y\right)\left(Y\right)=1_R$$
69	8	fveq2d	$$⊢\phi \to 1_R=1_{\mathrm{Scalar}\left(T\right)}$$
70	68 69	eqtrd	$$⊢\phi \to U\left(Y\right)\left(Y\right)=1_{\mathrm{Scalar}\left(T\right)}$$
71	70	oveq1d	$$⊢\phi \to U\left(Y\right)\left(Y\right)\underset{\dot{}}{·}A\left(Y\right)=1_{\mathrm{Scalar}\left(T\right)}\underset{\dot{}}{·}A\left(Y\right)$$
72	9 10	ffvelrnd	$$⊢\phi \to A\left(Y\right)\in C$$
73		eqid	$$⊢1_{\mathrm{Scalar}\left(T\right)}=1_{\mathrm{Scalar}\left(T\right)}$$
74	3 12 4 73	lmodvs1	$$⊢\left(T\in \mathrm{LMod}\wedge A\left(Y\right)\in C\right)\to 1_{\mathrm{Scalar}\left(T\right)}\underset{\dot{}}{·}A\left(Y\right)=A\left(Y\right)$$
75	6 72 74	syl2anc	$$⊢\phi \to 1_{\mathrm{Scalar}\left(T\right)}\underset{\dot{}}{·}A\left(Y\right)=A\left(Y\right)$$
76	66 71 75	3eqtrd	$$⊢\phi \to \left(U\left(Y\right){\underset{\dot{}}{·}}_{f}A\right)\left(Y\right)=A\left(Y\right)$$
77	23 64 76	3eqtrd	$$⊢\phi \to E\left(U\left(Y\right)\right)=A\left(Y\right)$$