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	eqtrid	⊢ ( 𝜑 → ✚ = ( +_g ‘ ( toℂPreHil ‘ ( ℝ_fld freeLMod 𝐼 ) ) ) )
15	12	fveq2d	⊢ ( 𝜑 → ( ·_𝑠 ‘ 𝐻 ) = ( ·_𝑠 ‘ ( toℂPreHil ‘ ( ℝ_fld freeLMod 𝐼 ) ) ) )
16	3 15	eqtrid	⊢ ( 𝜑 → ∙ = ( ·_𝑠 ‘ ( 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		resrng	⊢ ℝ_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	⊢ ( 𝜑 → ( 𝑍 = ( ( 𝐴 ∙ 𝑋 ) ✚ ( 𝐶 ∙ 𝑌 ) ) ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑍 ‘ 𝑖 ) = ( ( 𝐴 · ( 𝑋 ‘ 𝑖 ) ) + ( 𝐶 · ( 𝑌 ‘ 𝑖 ) ) ) ) )

Metamath Proof Explorer

Theorem rrxplusgvscavalb

Proof