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

Metamath Proof Explorer

Theorem cphass

Description: Associative law for inner product. Equation I2 of Ponnusamy p. 363. See ipass , his5 . (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses cphipcj.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
cphipcj.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
cphass.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
cphass.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
cphass.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
Assertion cphass ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 · 𝐵 ) , 𝐶 ) = ( 𝐴 · ( 𝐵 , 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 cphipcj.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
2 cphipcj.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
3 cphass.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4 cphass.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
5 cphass.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
6 cphphl ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil )
7 eqid ⊢ ( .r ‘ 𝐹 ) = ( .r ‘ 𝐹 )
8 3 1 2 4 5 7 ipass ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 · 𝐵 ) , 𝐶 ) = ( 𝐴 ( .r ‘ 𝐹 ) ( 𝐵 , 𝐶 ) ) )
9 6 8 sylan ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 · 𝐵 ) , 𝐶 ) = ( 𝐴 ( .r ‘ 𝐹 ) ( 𝐵 , 𝐶 ) ) )
10 cphclm ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ ℂMod )
11 3 clmmul ⊢ ( 𝑊 ∈ ℂMod → · = ( .r ‘ 𝐹 ) )
12 10 11 syl ⊢ ( 𝑊 ∈ ℂPreHil → · = ( .r ‘ 𝐹 ) )
13 12 adantr ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → · = ( .r ‘ 𝐹 ) )
14 13 oveqd ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐴 · ( 𝐵 , 𝐶 ) ) = ( 𝐴 ( .r ‘ 𝐹 ) ( 𝐵 , 𝐶 ) ) )
15 9 14 eqtr4d ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 · 𝐵 ) , 𝐶 ) = ( 𝐴 · ( 𝐵 , 𝐶 ) ) )