Metamath Proof Explorer

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 ${⊢}{H}={{I}}^{}$
rrxbase.b ${⊢}{B}={\mathrm{Base}}_{{H}}$
rrxplusgvscavalb.r
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
rrxplusgvscavalb.c ${⊢}{\phi }\to {C}\in ℝ$
Assertion rrxplusgvscavalb

Proof

Step Hyp Ref Expression
1 rrxval.r ${⊢}{H}={{I}}^{}$
2 rrxbase.b ${⊢}{B}={\mathrm{Base}}_{{H}}$
3 rrxplusgvscavalb.r
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
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
15 12 fveq2d ${⊢}{\phi }\to {\cdot }_{{H}}={\cdot }_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}{I}\right)}$
16 3 15 syl5eq
17 16 oveqd
18 16 oveqd
19 14 17 18 oveq123d
20 19 eqeq2d
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 ${⊢}×={\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)↔\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{Z}\left({i}\right)={A}{X}\left({i}\right)+{C}{Y}\left({i}\right)\right)$
43 20 42 bitrd