rrxvsca

Description: The scalar product over generalized Euclidean spaces is the componentwise real number multiplication. (Contributed by Thierry Arnoux, 18-Jan-2023)

	Ref	Expression
Hypotheses	rrxval.r	⊢ 𝐻 = ( ℝ^ ‘ 𝐼 )
	rrxbase.b	⊢ 𝐵 = ( Base ‘ 𝐻 )
	rrxvsca.r	⊢ ∙ = ( ·_𝑠 ‘ 𝐻 )
	rrxvsca.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	rrxvsca.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐼 )
	rrxvsca.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	rrxvsca.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐻 ) )
Assertion	rrxvsca	⊢ ( 𝜑 → ( ( 𝐴 ∙ 𝑋 ) ‘ 𝐽 ) = ( 𝐴 · ( 𝑋 ‘ 𝐽 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rrxval.r	⊢ 𝐻 = ( ℝ^ ‘ 𝐼 )
2		rrxbase.b	⊢ 𝐵 = ( Base ‘ 𝐻 )
3		rrxvsca.r	⊢ ∙ = ( ·_𝑠 ‘ 𝐻 )
4		rrxvsca.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
5		rrxvsca.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐼 )
6		rrxvsca.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
7		rrxvsca.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐻 ) )
8	1	rrxval	⊢ ( 𝐼 ∈ 𝑉 → 𝐻 = ( toℂPreHil ‘ ( ℝ_fld freeLMod 𝐼 ) ) )
9	4 8	syl	⊢ ( 𝜑 → 𝐻 = ( toℂPreHil ‘ ( ℝ_fld freeLMod 𝐼 ) ) )
10	9	fveq2d	⊢ ( 𝜑 → ( ·_𝑠 ‘ 𝐻 ) = ( ·_𝑠 ‘ ( toℂPreHil ‘ ( ℝ_fld freeLMod 𝐼 ) ) ) )
11	3 10	eqtrid	⊢ ( 𝜑 → ∙ = ( ·_𝑠 ‘ ( toℂPreHil ‘ ( ℝ_fld freeLMod 𝐼 ) ) ) )
12	11	oveqd	⊢ ( 𝜑 → ( 𝐴 ∙ 𝑋 ) = ( 𝐴 ( ·_𝑠 ‘ ( toℂPreHil ‘ ( ℝ_fld freeLMod 𝐼 ) ) ) 𝑋 ) )
13	12	fveq1d	⊢ ( 𝜑 → ( ( 𝐴 ∙ 𝑋 ) ‘ 𝐽 ) = ( ( 𝐴 ( ·_𝑠 ‘ ( toℂPreHil ‘ ( ℝ_fld freeLMod 𝐼 ) ) ) 𝑋 ) ‘ 𝐽 ) )
14		eqid	⊢ ( ℝ_fld freeLMod 𝐼 ) = ( ℝ_fld freeLMod 𝐼 )
15		eqid	⊢ ( Base ‘ ( ℝ_fld freeLMod 𝐼 ) ) = ( Base ‘ ( ℝ_fld freeLMod 𝐼 ) )
16		rebase	⊢ ℝ = ( Base ‘ ℝ_fld )
17	9	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝐻 ) = ( Base ‘ ( toℂPreHil ‘ ( ℝ_fld freeLMod 𝐼 ) ) ) )
18		eqid	⊢ ( toℂPreHil ‘ ( ℝ_fld freeLMod 𝐼 ) ) = ( toℂPreHil ‘ ( ℝ_fld freeLMod 𝐼 ) )
19	18 15	tcphbas	⊢ ( Base ‘ ( ℝ_fld freeLMod 𝐼 ) ) = ( Base ‘ ( toℂPreHil ‘ ( ℝ_fld freeLMod 𝐼 ) ) )
20	17 19	eqtr4di	⊢ ( 𝜑 → ( Base ‘ 𝐻 ) = ( Base ‘ ( ℝ_fld freeLMod 𝐼 ) ) )
21	7 20	eleqtrd	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( ℝ_fld freeLMod 𝐼 ) ) )
22		eqid	⊢ ( ·_𝑠 ‘ ( ℝ_fld freeLMod 𝐼 ) ) = ( ·_𝑠 ‘ ( ℝ_fld freeLMod 𝐼 ) )
23	18 22	tcphvsca	⊢ ( ·_𝑠 ‘ ( ℝ_fld freeLMod 𝐼 ) ) = ( ·_𝑠 ‘ ( toℂPreHil ‘ ( ℝ_fld freeLMod 𝐼 ) ) )
24	23	eqcomi	⊢ ( ·_𝑠 ‘ ( toℂPreHil ‘ ( ℝ_fld freeLMod 𝐼 ) ) ) = ( ·_𝑠 ‘ ( ℝ_fld freeLMod 𝐼 ) )
25		remulr	⊢ · = ( ._r ‘ ℝ_fld )
26	14 15 16 4 6 21 5 24 25	frlmvscaval	⊢ ( 𝜑 → ( ( 𝐴 ( ·_𝑠 ‘ ( toℂPreHil ‘ ( ℝ_fld freeLMod 𝐼 ) ) ) 𝑋 ) ‘ 𝐽 ) = ( 𝐴 · ( 𝑋 ‘ 𝐽 ) ) )
27	13 26	eqtrd	⊢ ( 𝜑 → ( ( 𝐴 ∙ 𝑋 ) ‘ 𝐽 ) = ( 𝐴 · ( 𝑋 ‘ 𝐽 ) ) )

Metamath Proof Explorer

Theorem rrxvsca

Proof