Theorem cphassi

Description: Associative law for the first argument of an inner product with scalar _ i . (Contributed by AV, 17-Oct-2021)

	Ref	Expression
Hypotheses	cphassi.x	⊢ 𝑋 = ( Base ‘ 𝑊 )
	cphassi.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
	cphassi.i	⊢ , = ( ·𝑖 ‘ 𝑊 )
	cphassi.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	cphassi.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion	cphassi	⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( i · 𝐵 ) , 𝐴 ) = ( i · ( 𝐵 , 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cphassi.x	⊢ 𝑋 = ( Base ‘ 𝑊 )
2		cphassi.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
3		cphassi.i	⊢ , = ( ·𝑖 ‘ 𝑊 )
4		cphassi.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
5		cphassi.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
6		simp1l	⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝑊 ∈ ℂPreHil )
7		simp1r	⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → i ∈ 𝐾 )
8		simp3	⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐵 ∈ 𝑋 )
9		simp2	⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
10	3 1 4 5 2	cphass	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( i ∈ 𝐾 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( i · 𝐵 ) , 𝐴 ) = ( i · ( 𝐵 , 𝐴 ) ) )
11	6 7 8 9 10	syl13anc	⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( i · 𝐵 ) , 𝐴 ) = ( i · ( 𝐵 , 𝐴 ) ) )