Metamath Proof Explorer


Theorem hlipass

Description: Associative law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007) (New usage is discouraged.)

Ref Expression
Hypotheses hlipass.1 𝑋 = ( BaseSet ‘ 𝑈 )
hlipass.4 𝑆 = ( ·𝑠OLD𝑈 )
hlipass.7 𝑃 = ( ·𝑖OLD𝑈 )
Assertion hlipass ( ( 𝑈 ∈ CHilOLD ∧ ( 𝐴 ∈ ℂ ∧ 𝐵𝑋𝐶𝑋 ) ) → ( ( 𝐴 𝑆 𝐵 ) 𝑃 𝐶 ) = ( 𝐴 · ( 𝐵 𝑃 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 hlipass.1 𝑋 = ( BaseSet ‘ 𝑈 )
2 hlipass.4 𝑆 = ( ·𝑠OLD𝑈 )
3 hlipass.7 𝑃 = ( ·𝑖OLD𝑈 )
4 hlph ( 𝑈 ∈ CHilOLD𝑈 ∈ CPreHilOLD )
5 1 2 3 dipass ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴 ∈ ℂ ∧ 𝐵𝑋𝐶𝑋 ) ) → ( ( 𝐴 𝑆 𝐵 ) 𝑃 𝐶 ) = ( 𝐴 · ( 𝐵 𝑃 𝐶 ) ) )
6 4 5 sylan ( ( 𝑈 ∈ CHilOLD ∧ ( 𝐴 ∈ ℂ ∧ 𝐵𝑋𝐶𝑋 ) ) → ( ( 𝐴 𝑆 𝐵 ) 𝑃 𝐶 ) = ( 𝐴 · ( 𝐵 𝑃 𝐶 ) ) )