Theorem hstosum

Description: Orthogonal sum property of a Hilbert-space-valued state. (Contributed by NM, 25-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	hstosum	⊢ ( ( ( 𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) ∧ ( 𝐵 ∈ Cℋ ∧ 𝐴 ⊆ ( ⊥ ‘ 𝐵 ) ) ) → ( 𝑆 ‘ ( 𝐴 ∨ℋ 𝐵 ) ) = ( ( 𝑆 ‘ 𝐴 ) +ℎ ( 𝑆 ‘ 𝐵 ) ) )

Proof

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