Theorem frlmvplusgvalc

Description: Coordinates of a sum with respect to a basis in a free module. (Contributed by AV, 16-Jan-2023)

	Ref	Expression
Hypotheses	frlmvplusgvalc.f	$$⊢F=R\mathrm{freeLMod}I$$
	frlmvplusgvalc.b	$$⊢B={\mathrm{Base}}_F$$
	frlmvplusgvalc.r	$$⊢\phi \to R\in V$$
	frlmvplusgvalc.i	$$⊢\phi \to I\in W$$
	frlmvplusgvalc.x	$$⊢\phi \to X\in B$$
	frlmvplusgvalc.y	$$⊢\phi \to Y\in B$$
	frlmvplusgvalc.j	$$⊢\phi \to J\in I$$
	frlmvplusgvalc.a	$$⊢\underset{\dot{}}{+}={+}_R$$
	frlmvplusgvalc.p	$$⊢\underset{\dot{}}{✚}={+}_F$$
Assertion	frlmvplusgvalc	$$⊢\phi \to \left(X\underset{\dot{}}{✚}Y\right)\left(J\right)=X\left(J\right)\underset{\dot{}}{+}Y\left(J\right)$$

Proof

Step	Hyp	Ref	Expression
1		frlmvplusgvalc.f	$$⊢F=R\mathrm{freeLMod}I$$
2		frlmvplusgvalc.b	$$⊢B={\mathrm{Base}}_F$$
3		frlmvplusgvalc.r	$$⊢\phi \to R\in V$$
4		frlmvplusgvalc.i	$$⊢\phi \to I\in W$$
5		frlmvplusgvalc.x	$$⊢\phi \to X\in B$$
6		frlmvplusgvalc.y	$$⊢\phi \to Y\in B$$
7		frlmvplusgvalc.j	$$⊢\phi \to J\in I$$
8		frlmvplusgvalc.a	$$⊢\underset{\dot{}}{+}={+}_R$$
9		frlmvplusgvalc.p	$$⊢\underset{\dot{}}{✚}={+}_F$$
10	1 2 3 4 5 6 8 9	frlmplusgval	$$⊢\phi \to X\underset{\dot{}}{✚}Y=X{\underset{\dot{}}{+}}_{f}Y$$
11	10	fveq1d	$$⊢\phi \to \left(X\underset{\dot{}}{✚}Y\right)\left(J\right)=\left(X{\underset{\dot{}}{+}}_{f}Y\right)\left(J\right)$$
12		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
13	1 12 2	frlmbasmap	$$⊢\left(I\in W\wedge X\in B\right)\to X\in \left({{\mathrm{Base}}_R}^I\right)$$
14	4 5 13	syl2anc	$$⊢\phi \to X\in \left({{\mathrm{Base}}_R}^I\right)$$
15		fvexd	$$⊢\phi \to {\mathrm{Base}}_R\in \mathrm{V}$$
16	15 4	elmapd	$$⊢\phi \to \left(X\in \left({{\mathrm{Base}}_R}^I\right)\leftrightarrow X:I⟶{\mathrm{Base}}_R\right)$$
17	14 16	mpbid	$$⊢\phi \to X:I⟶{\mathrm{Base}}_R$$
18	17	ffnd	$$⊢\phi \to XFnI$$
19	1 12 2	frlmbasmap	$$⊢\left(I\in W\wedge Y\in B\right)\to Y\in \left({{\mathrm{Base}}_R}^I\right)$$
20	4 6 19	syl2anc	$$⊢\phi \to Y\in \left({{\mathrm{Base}}_R}^I\right)$$
21	15 4	elmapd	$$⊢\phi \to \left(Y\in \left({{\mathrm{Base}}_R}^I\right)\leftrightarrow Y:I⟶{\mathrm{Base}}_R\right)$$
22	20 21	mpbid	$$⊢\phi \to Y:I⟶{\mathrm{Base}}_R$$
23	22	ffnd	$$⊢\phi \to YFnI$$
24		fnfvof	$$⊢\left(\left(XFnI\wedge YFnI\right)\wedge \left(I\in W\wedge J\in I\right)\right)\to \left(X{\underset{\dot{}}{+}}_{f}Y\right)\left(J\right)=X\left(J\right)\underset{\dot{}}{+}Y\left(J\right)$$
25	18 23 4 7 24	syl22anc	$$⊢\phi \to \left(X{\underset{\dot{}}{+}}_{f}Y\right)\left(J\right)=X\left(J\right)\underset{\dot{}}{+}Y\left(J\right)$$
26	11 25	eqtrd	$$⊢\phi \to \left(X\underset{\dot{}}{✚}Y\right)\left(J\right)=X\left(J\right)\underset{\dot{}}{+}Y\left(J\right)$$