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 ( ( ( 𝑆 ∈ CHStates ∧ 𝐴C ) ∧ ( 𝐵C𝐴 ⊆ ( ⊥ ‘ 𝐵 ) ) ) → ( ( 𝑆𝐴 ) ·ih ( 𝑆𝐵 ) ) = 0 )

Proof

Step Hyp Ref Expression
1 hstel2 ( ( ( 𝑆 ∈ CHStates ∧ 𝐴C ) ∧ ( 𝐵C𝐴 ⊆ ( ⊥ ‘ 𝐵 ) ) ) → ( ( ( 𝑆𝐴 ) ·ih ( 𝑆𝐵 ) ) = 0 ∧ ( 𝑆 ‘ ( 𝐴 𝐵 ) ) = ( ( 𝑆𝐴 ) + ( 𝑆𝐵 ) ) ) )
2 1 simpld ( ( ( 𝑆 ∈ CHStates ∧ 𝐴C ) ∧ ( 𝐵C𝐴 ⊆ ( ⊥ ‘ 𝐵 ) ) ) → ( ( 𝑆𝐴 ) ·ih ( 𝑆𝐵 ) ) = 0 )