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 ⊢ 𝐻 = ( ℝ^ ‘ 𝐼 )
rrxbase.b ⊢ 𝐵 = ( Base ‘ 𝐻 )
rrxplusgvscavalb.r ⊢ ∙ = ( ·𝑠 ‘ 𝐻 )
rrxplusgvscavalb.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
rrxplusgvscavalb.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
rrxplusgvscavalb.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
rrxplusgvscavalb.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
rrxplusgvscavalb.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
rrxplusgvscavalb.p ⊢ ✚ = ( +g ‘ 𝐻 )
rrxplusgvscavalb.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
Assertion rrxplusgvscavalb ( 𝜑 → ( 𝑍 = ( ( 𝐴 ∙ 𝑋 ) ✚ ( 𝐶 ∙ 𝑌 ) ) ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑍 ‘ 𝑖 ) = ( ( 𝐴 · ( 𝑋 ‘ 𝑖 ) ) + ( 𝐶 · ( 𝑌 ‘ 𝑖 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 rrxval.r ⊢ 𝐻 = ( ℝ^ ‘ 𝐼 )
2 rrxbase.b ⊢ 𝐵 = ( Base ‘ 𝐻 )
3 rrxplusgvscavalb.r ⊢ ∙ = ( ·𝑠 ‘ 𝐻 )
4 rrxplusgvscavalb.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
5 rrxplusgvscavalb.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
6 rrxplusgvscavalb.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7 rrxplusgvscavalb.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
8 rrxplusgvscavalb.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
9 rrxplusgvscavalb.p ⊢ ✚ = ( +g ‘ 𝐻 )
10 rrxplusgvscavalb.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
11 1 rrxval ⊢ ( 𝐼 ∈ 𝑉 → 𝐻 = ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) )
12 4 11 syl ⊢ ( 𝜑 → 𝐻 = ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) )
13 12 fveq2d ⊢ ( 𝜑 → ( +g ‘ 𝐻 ) = ( +g ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) )
14 9 13 syl5eq ⊢ ( 𝜑 → ✚ = ( +g ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) )
15 12 fveq2d ⊢ ( 𝜑 → ( ·𝑠 ‘ 𝐻 ) = ( ·𝑠 ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) )
16 3 15 syl5eq ⊢ ( 𝜑 → ∙ = ( ·𝑠 ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) )
17 16 oveqd ⊢ ( 𝜑 → ( 𝐴 ∙ 𝑋 ) = ( 𝐴 ( ·𝑠 ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) 𝑋 ) )
18 16 oveqd ⊢ ( 𝜑 → ( 𝐶 ∙ 𝑌 ) = ( 𝐶 ( ·𝑠 ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) 𝑌 ) )
19 14 17 18 oveq123d ⊢ ( 𝜑 → ( ( 𝐴 ∙ 𝑋 ) ✚ ( 𝐶 ∙ 𝑌 ) ) = ( ( 𝐴 ( ·𝑠 ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) 𝑋 ) ( +g ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) ( 𝐶 ( ·𝑠 ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) 𝑌 ) ) )
20 19 eqeq2d ⊢ ( 𝜑 → ( 𝑍 = ( ( 𝐴 ∙ 𝑋 ) ✚ ( 𝐶 ∙ 𝑌 ) ) ↔ 𝑍 = ( ( 𝐴 ( ·𝑠 ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) 𝑋 ) ( +g ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) ( 𝐶 ( ·𝑠 ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) 𝑌 ) ) ) )
21 eqid ⊢ ( ℝfld freeLMod 𝐼 ) = ( ℝfld freeLMod 𝐼 )
22 eqid ⊢ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) = ( Base ‘ ( ℝfld freeLMod 𝐼 ) )
23 12 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝐻 ) = ( Base ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) )
24 eqid ⊢ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) = ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) )
25 24 22 tcphbas ⊢ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) = ( Base ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) )
26 23 2 25 3eqtr4g ⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) )
27 6 26 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) )
28 8 26 eleqtrd ⊢ ( 𝜑 → 𝑍 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) )
29 recrng ⊢ ℝfld ∈ *-Ring
30 srngring ⊢ ( ℝfld ∈ *-Ring → ℝfld ∈ Ring )
31 29 30 mp1i ⊢ ( 𝜑 → ℝfld ∈ Ring )
32 rebase ⊢ ℝ = ( Base ‘ ℝfld )
33 eqid ⊢ ( ·𝑠 ‘ ( ℝfld freeLMod 𝐼 ) ) = ( ·𝑠 ‘ ( ℝfld freeLMod 𝐼 ) )
34 24 33 tcphvsca ⊢ ( ·𝑠 ‘ ( ℝfld freeLMod 𝐼 ) ) = ( ·𝑠 ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) )
35 34 eqcomi ⊢ ( ·𝑠 ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) = ( ·𝑠 ‘ ( ℝfld freeLMod 𝐼 ) )
36 remulr ⊢ · = ( .r ‘ ℝfld )
37 7 26 eleqtrd ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) )
38 replusg ⊢ + = ( +g ‘ ℝfld )
39 eqid ⊢ ( +g ‘ ( ℝfld freeLMod 𝐼 ) ) = ( +g ‘ ( ℝfld freeLMod 𝐼 ) )
40 24 39 tchplusg ⊢ ( +g ‘ ( ℝfld freeLMod 𝐼 ) ) = ( +g ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) )
41 40 eqcomi ⊢ ( +g ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) = ( +g ‘ ( ℝfld freeLMod 𝐼 ) )
42 21 22 4 27 28 31 32 5 35 36 37 38 41 10 frlmvplusgscavalb ⊢ ( 𝜑 → ( 𝑍 = ( ( 𝐴 ( ·𝑠 ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) 𝑋 ) ( +g ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) ( 𝐶 ( ·𝑠 ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) 𝑌 ) ) ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑍 ‘ 𝑖 ) = ( ( 𝐴 · ( 𝑋 ‘ 𝑖 ) ) + ( 𝐶 · ( 𝑌 ‘ 𝑖 ) ) ) ) )
43 20 42 bitrd ⊢ ( 𝜑 → ( 𝑍 = ( ( 𝐴 ∙ 𝑋 ) ✚ ( 𝐶 ∙ 𝑌 ) ) ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑍 ‘ 𝑖 ) = ( ( 𝐴 · ( 𝑋 ‘ 𝑖 ) ) + ( 𝐶 · ( 𝑌 ‘ 𝑖 ) ) ) ) )