Theorem rrxplusgvscavalb

Description: The result of the addition combined with scalar multiplication in a generalized Euclidean space is defined by its coordinate-wise operations. (Contributed by AV, 21-Jan-2023)

	Ref	Expression
Hypotheses	rrxval.r
	rrxbase.b	$$⊢B={\mathrm{Base}}_H$$
	rrxplusgvscavalb.r	$$⊢\underset{\dot{}}{\bullet }={\cdot }_H$$
	rrxplusgvscavalb.i	$$⊢\phi \to I\in V$$
	rrxplusgvscavalb.a	$$⊢\phi \to A\in ℝ$$
	rrxplusgvscavalb.x	$$⊢\phi \to X\in B$$
	rrxplusgvscavalb.y	$$⊢\phi \to Y\in B$$
	rrxplusgvscavalb.z	$$⊢\phi \to Z\in B$$
	rrxplusgvscavalb.p	$$⊢\underset{\dot{}}{✚}={+}_H$$
	rrxplusgvscavalb.c	$$⊢\phi \to C\in ℝ$$
Assertion	rrxplusgvscavalb	$$⊢\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)=AX\left(i\right)+CY\left(i\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		rrxval.r
2		rrxbase.b	$$⊢B={\mathrm{Base}}_H$$
3		rrxplusgvscavalb.r	$$⊢\underset{\dot{}}{\bullet }={\cdot }_H$$
4		rrxplusgvscavalb.i	$$⊢\phi \to I\in V$$
5		rrxplusgvscavalb.a	$$⊢\phi \to A\in ℝ$$
6		rrxplusgvscavalb.x	$$⊢\phi \to X\in B$$
7		rrxplusgvscavalb.y	$$⊢\phi \to Y\in B$$
8		rrxplusgvscavalb.z	$$⊢\phi \to Z\in B$$
9		rrxplusgvscavalb.p	$$⊢\underset{\dot{}}{✚}={+}_H$$
10		rrxplusgvscavalb.c	$$⊢\phi \to C\in ℝ$$
11	1	rrxval	$$⊢I\in V\to H=\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)$$
12	4 11	syl	$$⊢\phi \to H=\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)$$
13	12	fveq2d	$$⊢\phi \to {+}_H={+}_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
14	9 13	syl5eq	$$⊢\phi \to \underset{\dot{}}{✚}={+}_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
15	12	fveq2d	$$⊢\phi \to {\cdot }_H={\cdot }_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
16	3 15	syl5eq	$$⊢\phi \to \underset{\dot{}}{\bullet }={\cdot }_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
17	16	oveqd	$$⊢\phi \to A\underset{\dot{}}{\bullet }X=A{\cdot }_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}X$$
18	16	oveqd	$$⊢\phi \to C\underset{\dot{}}{\bullet }Y=C{\cdot }_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}Y$$
19	14 17 18	oveq123d	$$⊢\phi \to \left(A\underset{\dot{}}{\bullet }X\right)\underset{\dot{}}{✚}\left(C\underset{\dot{}}{\bullet }Y\right)=\left(A{\cdot }_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}X\right){+}_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}\left(C{\cdot }_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}Y\right)$$
20	19	eqeq2d	$$⊢\phi \to \left(Z=\left(A\underset{\dot{}}{\bullet }X\right)\underset{\dot{}}{✚}\left(C\underset{\dot{}}{\bullet }Y\right)\leftrightarrow Z=\left(A{\cdot }_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}X\right){+}_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}\left(C{\cdot }_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}Y\right)\right)$$
21		eqid	$$⊢{ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I={ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I$$
22		eqid	$$⊢{\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}={\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
23	12	fveq2d	$$⊢\phi \to {\mathrm{Base}}_H={\mathrm{Base}}_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
24		eqid	$$⊢\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)=\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)$$
25	24 22	tcphbas	$$⊢{\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}={\mathrm{Base}}_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
26	23 2 25	3eqtr4g	$$⊢\phi \to B={\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
27	6 26	eleqtrd	$$⊢\phi \to X\in {\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
28	8 26	eleqtrd	$$⊢\phi \to Z\in {\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
29		recrng	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{*-Ring}$$
30		srngring	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{*-Ring}\to {ℝ}_{\mathrm{fld}}\in \mathrm{Ring}$$
31	29 30	mp1i	$$⊢\phi \to {ℝ}_{\mathrm{fld}}\in \mathrm{Ring}$$
32		rebase	$$⊢ℝ={\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}$$
33		eqid	$$⊢{\cdot }_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}={\cdot }_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
34	24 33	tcphvsca	$$⊢{\cdot }_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}={\cdot }_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
35	34	eqcomi	$$⊢{\cdot }_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}={\cdot }_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
36		remulr	$$⊢\times ={\cdot }_{{ℝ}_{\mathrm{fld}}}$$
37	7 26	eleqtrd	$$⊢\phi \to Y\in {\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
38		replusg	$$⊢+={+}_{{ℝ}_{\mathrm{fld}}}$$
39		eqid	$$⊢{+}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}={+}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
40	24 39	tchplusg	$$⊢{+}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}={+}_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
41	40	eqcomi	$$⊢{+}_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}={+}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
42	21 22 4 27 28 31 32 5 35 36 37 38 41 10	frlmvplusgscavalb	$$⊢\phi \to \left(Z=\left(A{\cdot }_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}X\right){+}_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}\left(C{\cdot }_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}Y\right)\leftrightarrow \forall i\in IZ\left(i\right)=AX\left(i\right)+CY\left(i\right)\right)$$
43	20 42	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)=AX\left(i\right)+CY\left(i\right)\right)$$