This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 · ( 𝐵 , 𝐴 ) ) )