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

Metamath Proof Explorer

Theorem cphassir

Description: "Associative" law for the second 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 cphassir ( ( ( 𝑊 ∈ ℂ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 simp2 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
9 simp3 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐵 ∈ 𝑋 )
10 3 1 4 5 2 cphassr ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( i ∈ 𝐾 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 , ( i · 𝐵 ) ) = ( ( ∗ ‘ i ) · ( 𝐴 , 𝐵 ) ) )
11 6 7 8 9 10 syl13anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 , ( i · 𝐵 ) ) = ( ( ∗ ‘ i ) · ( 𝐴 , 𝐵 ) ) )
12 cji ⊢ ( ∗ ‘ i ) = - i
13 12 oveq1i ⊢ ( ( ∗ ‘ i ) · ( 𝐴 , 𝐵 ) ) = ( - i · ( 𝐴 , 𝐵 ) )
14 11 13 eqtrdi ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 , ( i · 𝐵 ) ) = ( - i · ( 𝐴 , 𝐵 ) ) )