MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rrxplusgvscavalb Structured version   Visualization version   GIF version

Theorem rrxplusgvscavalb 23988
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.)
Hypotheses
Ref Expression
rrxval.r 𝐻 = (ℝ^‘𝐼)
rrxbase.b 𝐵 = (Base‘𝐻)
rrxplusgvscavalb.r = ( ·𝑠𝐻)
rrxplusgvscavalb.i (𝜑𝐼𝑉)
rrxplusgvscavalb.a (𝜑𝐴 ∈ ℝ)
rrxplusgvscavalb.x (𝜑𝑋𝐵)
rrxplusgvscavalb.y (𝜑𝑌𝐵)
rrxplusgvscavalb.z (𝜑𝑍𝐵)
rrxplusgvscavalb.p = (+g𝐻)
rrxplusgvscavalb.c (𝜑𝐶 ∈ ℝ)
Assertion
Ref Expression
rrxplusgvscavalb (𝜑 → (𝑍 = ((𝐴 𝑋) (𝐶 𝑌)) ↔ ∀𝑖𝐼 (𝑍𝑖) = ((𝐴 · (𝑋𝑖)) + (𝐶 · (𝑌𝑖)))))
Distinct variable groups:   𝑖,𝐼   𝐴,𝑖   𝐶,𝑖   𝑖,𝑋   𝑖,𝑌   𝑖,𝑍   𝜑,𝑖
Allowed substitution hints:   𝐵(𝑖)   (𝑖)   (𝑖)   𝐻(𝑖)   𝑉(𝑖)

Proof of Theorem rrxplusgvscavalb
StepHypRef Expression
1 rrxplusgvscavalb.p . . . . 5 = (+g𝐻)
2 rrxplusgvscavalb.i . . . . . . 7 (𝜑𝐼𝑉)
3 rrxval.r . . . . . . . 8 𝐻 = (ℝ^‘𝐼)
43rrxval 23980 . . . . . . 7 (𝐼𝑉𝐻 = (toℂPreHil‘(ℝfld freeLMod 𝐼)))
52, 4syl 17 . . . . . 6 (𝜑𝐻 = (toℂPreHil‘(ℝfld freeLMod 𝐼)))
65fveq2d 6655 . . . . 5 (𝜑 → (+g𝐻) = (+g‘(toℂPreHil‘(ℝfld freeLMod 𝐼))))
71, 6syl5eq 2871 . . . 4 (𝜑 = (+g‘(toℂPreHil‘(ℝfld freeLMod 𝐼))))
8 rrxplusgvscavalb.r . . . . . 6 = ( ·𝑠𝐻)
95fveq2d 6655 . . . . . 6 (𝜑 → ( ·𝑠𝐻) = ( ·𝑠 ‘(toℂPreHil‘(ℝfld freeLMod 𝐼))))
108, 9syl5eq 2871 . . . . 5 (𝜑 = ( ·𝑠 ‘(toℂPreHil‘(ℝfld freeLMod 𝐼))))
1110oveqd 7155 . . . 4 (𝜑 → (𝐴 𝑋) = (𝐴( ·𝑠 ‘(toℂPreHil‘(ℝfld freeLMod 𝐼)))𝑋))
1210oveqd 7155 . . . 4 (𝜑 → (𝐶 𝑌) = (𝐶( ·𝑠 ‘(toℂPreHil‘(ℝfld freeLMod 𝐼)))𝑌))
137, 11, 12oveq123d 7159 . . 3 (𝜑 → ((𝐴 𝑋) (𝐶 𝑌)) = ((𝐴( ·𝑠 ‘(toℂPreHil‘(ℝfld freeLMod 𝐼)))𝑋)(+g‘(toℂPreHil‘(ℝfld freeLMod 𝐼)))(𝐶( ·𝑠 ‘(toℂPreHil‘(ℝfld freeLMod 𝐼)))𝑌)))
1413eqeq2d 2835 . 2 (𝜑 → (𝑍 = ((𝐴 𝑋) (𝐶 𝑌)) ↔ 𝑍 = ((𝐴( ·𝑠 ‘(toℂPreHil‘(ℝfld freeLMod 𝐼)))𝑋)(+g‘(toℂPreHil‘(ℝfld freeLMod 𝐼)))(𝐶( ·𝑠 ‘(toℂPreHil‘(ℝfld freeLMod 𝐼)))𝑌))))
15 eqid 2824 . . 3 (ℝfld freeLMod 𝐼) = (ℝfld freeLMod 𝐼)
16 eqid 2824 . . 3 (Base‘(ℝfld freeLMod 𝐼)) = (Base‘(ℝfld freeLMod 𝐼))
17 rrxplusgvscavalb.x . . . 4 (𝜑𝑋𝐵)
185fveq2d 6655 . . . . 5 (𝜑 → (Base‘𝐻) = (Base‘(toℂPreHil‘(ℝfld freeLMod 𝐼))))
19 rrxbase.b . . . . 5 𝐵 = (Base‘𝐻)
20 eqid 2824 . . . . . 6 (toℂPreHil‘(ℝfld freeLMod 𝐼)) = (toℂPreHil‘(ℝfld freeLMod 𝐼))
2120, 16tcphbas 23812 . . . . 5 (Base‘(ℝfld freeLMod 𝐼)) = (Base‘(toℂPreHil‘(ℝfld freeLMod 𝐼)))
2218, 19, 213eqtr4g 2884 . . . 4 (𝜑𝐵 = (Base‘(ℝfld freeLMod 𝐼)))
2317, 22eleqtrd 2918 . . 3 (𝜑𝑋 ∈ (Base‘(ℝfld freeLMod 𝐼)))
24 rrxplusgvscavalb.z . . . 4 (𝜑𝑍𝐵)
2524, 22eleqtrd 2918 . . 3 (𝜑𝑍 ∈ (Base‘(ℝfld freeLMod 𝐼)))
26 recrng 20751 . . . 4 fld ∈ *-Ring
27 srngring 19609 . . . 4 (ℝfld ∈ *-Ring → ℝfld ∈ Ring)
2826, 27mp1i 13 . . 3 (𝜑 → ℝfld ∈ Ring)
29 rebase 20736 . . 3 ℝ = (Base‘ℝfld)
30 rrxplusgvscavalb.a . . 3 (𝜑𝐴 ∈ ℝ)
31 eqid 2824 . . . . 5 ( ·𝑠 ‘(ℝfld freeLMod 𝐼)) = ( ·𝑠 ‘(ℝfld freeLMod 𝐼))
3220, 31tcphvsca 23817 . . . 4 ( ·𝑠 ‘(ℝfld freeLMod 𝐼)) = ( ·𝑠 ‘(toℂPreHil‘(ℝfld freeLMod 𝐼)))
3332eqcomi 2833 . . 3 ( ·𝑠 ‘(toℂPreHil‘(ℝfld freeLMod 𝐼))) = ( ·𝑠 ‘(ℝfld freeLMod 𝐼))
34 remulr 20741 . . 3 · = (.r‘ℝfld)
35 rrxplusgvscavalb.y . . . 4 (𝜑𝑌𝐵)
3635, 22eleqtrd 2918 . . 3 (𝜑𝑌 ∈ (Base‘(ℝfld freeLMod 𝐼)))
37 replusg 20740 . . 3 + = (+g‘ℝfld)
38 eqid 2824 . . . . 5 (+g‘(ℝfld freeLMod 𝐼)) = (+g‘(ℝfld freeLMod 𝐼))
3920, 38tchplusg 23813 . . . 4 (+g‘(ℝfld freeLMod 𝐼)) = (+g‘(toℂPreHil‘(ℝfld freeLMod 𝐼)))
4039eqcomi 2833 . . 3 (+g‘(toℂPreHil‘(ℝfld freeLMod 𝐼))) = (+g‘(ℝfld freeLMod 𝐼))
41 rrxplusgvscavalb.c . . 3 (𝜑𝐶 ∈ ℝ)
4215, 16, 2, 23, 25, 28, 29, 30, 33, 34, 36, 37, 40, 41frlmvplusgscavalb 20901 . 2 (𝜑 → (𝑍 = ((𝐴( ·𝑠 ‘(toℂPreHil‘(ℝfld freeLMod 𝐼)))𝑋)(+g‘(toℂPreHil‘(ℝfld freeLMod 𝐼)))(𝐶( ·𝑠 ‘(toℂPreHil‘(ℝfld freeLMod 𝐼)))𝑌)) ↔ ∀𝑖𝐼 (𝑍𝑖) = ((𝐴 · (𝑋𝑖)) + (𝐶 · (𝑌𝑖)))))
4314, 42bitrd 282 1 (𝜑 → (𝑍 = ((𝐴 𝑋) (𝐶 𝑌)) ↔ ∀𝑖𝐼 (𝑍𝑖) = ((𝐴 · (𝑋𝑖)) + (𝐶 · (𝑌𝑖)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209   = wceq 1538  wcel 2115  wral 3132  cfv 6336  (class class class)co 7138  cr 10521   + caddc 10525   · cmul 10527  Basecbs 16472  +gcplusg 16554   ·𝑠 cvsca 16558  Ringcrg 19286  *-Ringcsr 19601  fldcrefld 20734   freeLMod cfrlm 20876  toℂPreHilctcph 23761  ℝ^crrx 23976
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5171  ax-sep 5184  ax-nul 5191  ax-pow 5247  ax-pr 5311  ax-un 7444  ax-cnex 10578  ax-resscn 10579  ax-1cn 10580  ax-icn 10581  ax-addcl 10582  ax-addrcl 10583  ax-mulcl 10584  ax-mulrcl 10585  ax-mulcom 10586  ax-addass 10587  ax-mulass 10588  ax-distr 10589  ax-i2m1 10590  ax-1ne0 10591  ax-1rid 10592  ax-rnegex 10593  ax-rrecex 10594  ax-cnre 10595  ax-pre-lttri 10596  ax-pre-lttrn 10597  ax-pre-ltadd 10598  ax-pre-mulgt0 10599  ax-pre-sup 10600  ax-addf 10601  ax-mulf 10602
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3014  df-nel 3118  df-ral 3137  df-rex 3138  df-reu 3139  df-rmo 3140  df-rab 3141  df-v 3481  df-sbc 3758  df-csb 3866  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-pss 3937  df-nul 4275  df-if 4449  df-pw 4522  df-sn 4549  df-pr 4551  df-tp 4553  df-op 4555  df-uni 4820  df-int 4858  df-iun 4902  df-br 5048  df-opab 5110  df-mpt 5128  df-tr 5154  df-id 5441  df-eprel 5446  df-po 5455  df-so 5456  df-fr 5495  df-we 5497  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-pred 6129  df-ord 6175  df-on 6176  df-lim 6177  df-suc 6178  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-riota 7096  df-ov 7141  df-oprab 7142  df-mpo 7143  df-of 7392  df-om 7564  df-1st 7672  df-2nd 7673  df-supp 7814  df-tpos 7875  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-1o 8085  df-oadd 8089  df-er 8272  df-map 8391  df-ixp 8445  df-en 8493  df-dom 8494  df-sdom 8495  df-fin 8496  df-fsupp 8818  df-sup 8890  df-pnf 10662  df-mnf 10663  df-xr 10664  df-ltxr 10665  df-le 10666  df-sub 10857  df-neg 10858  df-div 11283  df-nn 11624  df-2 11686  df-3 11687  df-4 11688  df-5 11689  df-6 11690  df-7 11691  df-8 11692  df-9 11693  df-n0 11884  df-z 11968  df-dec 12085  df-uz 12230  df-rp 12376  df-fz 12884  df-seq 13363  df-exp 13424  df-cj 14447  df-re 14448  df-im 14449  df-sqrt 14583  df-abs 14584  df-struct 16474  df-ndx 16475  df-slot 16476  df-base 16478  df-sets 16479  df-ress 16480  df-plusg 16567  df-mulr 16568  df-starv 16569  df-sca 16570  df-vsca 16571  df-ip 16572  df-tset 16573  df-ple 16574  df-ds 16576  df-unif 16577  df-hom 16578  df-cco 16579  df-0g 16704  df-prds 16710  df-pws 16712  df-mgm 17841  df-sgrp 17890  df-mnd 17901  df-mhm 17945  df-grp 18095  df-minusg 18096  df-sbg 18097  df-subg 18265  df-ghm 18345  df-cmn 18897  df-mgp 19229  df-ur 19241  df-ring 19288  df-cring 19289  df-oppr 19362  df-dvdsr 19380  df-unit 19381  df-invr 19411  df-dvr 19422  df-rnghom 19456  df-drng 19490  df-field 19491  df-subrg 19519  df-staf 19602  df-srng 19603  df-lmod 19622  df-lss 19690  df-sra 19930  df-rgmod 19931  df-cnfld 20532  df-refld 20735  df-dsmm 20862  df-frlm 20877  df-tng 23180  df-tcph 23763  df-rrx 23978
This theorem is referenced by:  rrxlinesc  44979  rrxlinec  44980
  Copyright terms: Public domain W3C validator