Metamath Proof Explorer


Theorem hstorth

Description: Orthogonality property of a Hilbert-space-valued state. This is a key feature distinguishing it from a real-valued state. (Contributed by NM, 25-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion hstorth SCHStatesACBCABSAihSB=0

Proof

Step Hyp Ref Expression
1 hstel2 SCHStatesACBCABSAihSB=0SAB=SA+SB
2 1 simpld SCHStatesACBCABSAihSB=0