Theorem frlmvplusgscavalb

Description: Addition combined with scalar multiplication in a free module at the coordinates. (Contributed by AV, 16-Jan-2023)

	Ref	Expression
Hypotheses	frlmplusgvalb.f	$$⊢F=R\mathrm{freeLMod}I$$
	frlmplusgvalb.b	$$⊢B={\mathrm{Base}}_F$$
	frlmplusgvalb.i	$$⊢\phi \to I\in W$$
	frlmplusgvalb.x	$$⊢\phi \to X\in B$$
	frlmplusgvalb.z	$$⊢\phi \to Z\in B$$
	frlmplusgvalb.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	frlmvscavalb.k	$$⊢K={\mathrm{Base}}_R$$
	frlmvscavalb.a	$$⊢\phi \to A\in K$$
	frlmvscavalb.v	$$⊢\underset{\dot{}}{\bullet }={\cdot }_F$$
	frlmvscavalb.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	frlmvplusgscavalb.y	$$⊢\phi \to Y\in B$$
	frlmvplusgscavalb.a	$$⊢\underset{\dot{}}{+}={+}_R$$
	frlmvplusgscavalb.p	$$⊢\underset{\dot{}}{✚}={+}_F$$
	frlmvplusgscavalb.c	$$⊢\phi \to C\in K$$
Assertion	frlmvplusgscavalb	$$⊢\phi \to \left(Z=\left(A\underset{\dot{}}{\bullet }X\right)\underset{\dot{}}{✚}\left(C\underset{\dot{}}{\bullet }Y\right)\leftrightarrow \forall i\in IZ\left(i\right)=\left(A\underset{\dot{}}{·}X\left(i\right)\right)\underset{\dot{}}{+}\left(C\underset{\dot{}}{·}Y\left(i\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		frlmplusgvalb.f	$$⊢F=R\mathrm{freeLMod}I$$
2		frlmplusgvalb.b	$$⊢B={\mathrm{Base}}_F$$
3		frlmplusgvalb.i	$$⊢\phi \to I\in W$$
4		frlmplusgvalb.x	$$⊢\phi \to X\in B$$
5		frlmplusgvalb.z	$$⊢\phi \to Z\in B$$
6		frlmplusgvalb.r	$$⊢\phi \to R\in \mathrm{Ring}$$
7		frlmvscavalb.k	$$⊢K={\mathrm{Base}}_R$$
8		frlmvscavalb.a	$$⊢\phi \to A\in K$$
9		frlmvscavalb.v	$$⊢\underset{\dot{}}{\bullet }={\cdot }_F$$
10		frlmvscavalb.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
11		frlmvplusgscavalb.y	$$⊢\phi \to Y\in B$$
12		frlmvplusgscavalb.a	$$⊢\underset{\dot{}}{+}={+}_R$$
13		frlmvplusgscavalb.p	$$⊢\underset{\dot{}}{✚}={+}_F$$
14		frlmvplusgscavalb.c	$$⊢\phi \to C\in K$$
15	1	frlmlmod	$$⊢\left(R\in \mathrm{Ring}\wedge I\in W\right)\to F\in \mathrm{LMod}$$
16	6 3 15	syl2anc	$$⊢\phi \to F\in \mathrm{LMod}$$
17	8 7	eleqtrdi	$$⊢\phi \to A\in {\mathrm{Base}}_R$$
18	1	frlmsca	$$⊢\left(R\in \mathrm{Ring}\wedge I\in W\right)\to R=\mathrm{Scalar}\left(F\right)$$
19	6 3 18	syl2anc	$$⊢\phi \to R=\mathrm{Scalar}\left(F\right)$$
20	19	fveq2d	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(F\right)}$$
21	17 20	eleqtrd	$$⊢\phi \to A\in {\mathrm{Base}}_{\mathrm{Scalar}\left(F\right)}$$
22		eqid	$$⊢\mathrm{Scalar}\left(F\right)=\mathrm{Scalar}\left(F\right)$$
23		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(F\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(F\right)}$$
24	2 22 9 23	lmodvscl	$$⊢\left(F\in \mathrm{LMod}\wedge A\in {\mathrm{Base}}_{\mathrm{Scalar}\left(F\right)}\wedge X\in B\right)\to A\underset{\dot{}}{\bullet }X\in B$$
25	16 21 4 24	syl3anc	$$⊢\phi \to A\underset{\dot{}}{\bullet }X\in B$$
26	14 7	eleqtrdi	$$⊢\phi \to C\in {\mathrm{Base}}_R$$
27	26 20	eleqtrd	$$⊢\phi \to C\in {\mathrm{Base}}_{\mathrm{Scalar}\left(F\right)}$$
28	2 22 9 23	lmodvscl	$$⊢\left(F\in \mathrm{LMod}\wedge C\in {\mathrm{Base}}_{\mathrm{Scalar}\left(F\right)}\wedge Y\in B\right)\to C\underset{\dot{}}{\bullet }Y\in B$$
29	16 27 11 28	syl3anc	$$⊢\phi \to C\underset{\dot{}}{\bullet }Y\in B$$
30	1 2 3 25 5 6 29 12 13	frlmplusgvalb	$$⊢\phi \to \left(Z=\left(A\underset{\dot{}}{\bullet }X\right)\underset{\dot{}}{✚}\left(C\underset{\dot{}}{\bullet }Y\right)\leftrightarrow \forall i\in IZ\left(i\right)=\left(A\underset{\dot{}}{\bullet }X\right)\left(i\right)\underset{\dot{}}{+}\left(C\underset{\dot{}}{\bullet }Y\right)\left(i\right)\right)$$
31	3	adantr	$$⊢\left(\phi \wedge i\in I\right)\to I\in W$$
32	8	adantr	$$⊢\left(\phi \wedge i\in I\right)\to A\in K$$
33	4	adantr	$$⊢\left(\phi \wedge i\in I\right)\to X\in B$$
34		simpr	$$⊢\left(\phi \wedge i\in I\right)\to i\in I$$
35	1 2 7 31 32 33 34 9 10	frlmvscaval	$$⊢\left(\phi \wedge i\in I\right)\to \left(A\underset{\dot{}}{\bullet }X\right)\left(i\right)=A\underset{\dot{}}{·}X\left(i\right)$$
36	14	adantr	$$⊢\left(\phi \wedge i\in I\right)\to C\in K$$
37	11	adantr	$$⊢\left(\phi \wedge i\in I\right)\to Y\in B$$
38	1 2 7 31 36 37 34 9 10	frlmvscaval	$$⊢\left(\phi \wedge i\in I\right)\to \left(C\underset{\dot{}}{\bullet }Y\right)\left(i\right)=C\underset{\dot{}}{·}Y\left(i\right)$$
39	35 38	oveq12d	$$⊢\left(\phi \wedge i\in I\right)\to \left(A\underset{\dot{}}{\bullet }X\right)\left(i\right)\underset{\dot{}}{+}\left(C\underset{\dot{}}{\bullet }Y\right)\left(i\right)=\left(A\underset{\dot{}}{·}X\left(i\right)\right)\underset{\dot{}}{+}\left(C\underset{\dot{}}{·}Y\left(i\right)\right)$$
40	39	eqeq2d	$$⊢\left(\phi \wedge i\in I\right)\to \left(Z\left(i\right)=\left(A\underset{\dot{}}{\bullet }X\right)\left(i\right)\underset{\dot{}}{+}\left(C\underset{\dot{}}{\bullet }Y\right)\left(i\right)\leftrightarrow Z\left(i\right)=\left(A\underset{\dot{}}{·}X\left(i\right)\right)\underset{\dot{}}{+}\left(C\underset{\dot{}}{·}Y\left(i\right)\right)\right)$$
41	40	ralbidva	$$⊢\phi \to \left(\forall i\in IZ\left(i\right)=\left(A\underset{\dot{}}{\bullet }X\right)\left(i\right)\underset{\dot{}}{+}\left(C\underset{\dot{}}{\bullet }Y\right)\left(i\right)\leftrightarrow \forall i\in IZ\left(i\right)=\left(A\underset{\dot{}}{·}X\left(i\right)\right)\underset{\dot{}}{+}\left(C\underset{\dot{}}{·}Y\left(i\right)\right)\right)$$
42	30 41	bitrd	$$⊢\phi \to \left(Z=\left(A\underset{\dot{}}{\bullet }X\right)\underset{\dot{}}{✚}\left(C\underset{\dot{}}{\bullet }Y\right)\leftrightarrow \forall i\in IZ\left(i\right)=\left(A\underset{\dot{}}{·}X\left(i\right)\right)\underset{\dot{}}{+}\left(C\underset{\dot{}}{·}Y\left(i\right)\right)\right)$$