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 X=BaseSetU
hlipass.4 S=𝑠OLDU
hlipass.7 P=𝑖OLDU
Assertion hlipass UCHilOLDABXCXASBPC=ABPC

Proof

Step Hyp Ref Expression
1 hlipass.1 X=BaseSetU
2 hlipass.4 S=𝑠OLDU
3 hlipass.7 P=𝑖OLDU
4 hlph UCHilOLDUCPreHilOLD
5 1 2 3 dipass UCPreHilOLDABXCXASBPC=ABPC
6 4 5 sylan UCHilOLDABXCXASBPC=ABPC