Metamath Proof Explorer


Theorem hlipdir

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

Ref Expression
Hypotheses hlipdir.1 X=BaseSetU
hlipdir.2 G=+vU
hlipdir.7 P=𝑖OLDU
Assertion hlipdir UCHilOLDAXBXCXAGBPC=APC+BPC

Proof

Step Hyp Ref Expression
1 hlipdir.1 X=BaseSetU
2 hlipdir.2 G=+vU
3 hlipdir.7 P=𝑖OLDU
4 hlph UCHilOLDUCPreHilOLD
5 1 2 3 dipdir UCPreHilOLDAXBXCXAGBPC=APC+BPC
6 4 5 sylan UCHilOLDAXBXCXAGBPC=APC+BPC