Database
COMPLEX HILBERT SPACE EXPLORER (DEPRECATED)
States on a Hilbert lattice and Godowski's equation
States on a Hilbert lattice
hstorth
Metamath Proof Explorer
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 )