# Metamath Proof Explorer

## 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 ${⊢}\left(\left({S}\in \mathrm{CHStates}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\wedge \left({B}\in {\mathbf{C}}_{ℋ}\wedge {A}\subseteq \perp \left({B}\right)\right)\right)\to {S}\left({A}{\vee }_{ℋ}{B}\right)={S}\left({A}\right){+}_{ℎ}{S}\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 hstel2 ${⊢}\left(\left({S}\in \mathrm{CHStates}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\wedge \left({B}\in {\mathbf{C}}_{ℋ}\wedge {A}\subseteq \perp \left({B}\right)\right)\right)\to \left({S}\left({A}\right){\cdot }_{\mathrm{ih}}{S}\left({B}\right)=0\wedge {S}\left({A}{\vee }_{ℋ}{B}\right)={S}\left({A}\right){+}_{ℎ}{S}\left({B}\right)\right)$
2 1 simprd ${⊢}\left(\left({S}\in \mathrm{CHStates}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\wedge \left({B}\in {\mathbf{C}}_{ℋ}\wedge {A}\subseteq \perp \left({B}\right)\right)\right)\to {S}\left({A}{\vee }_{ℋ}{B}\right)={S}\left({A}\right){+}_{ℎ}{S}\left({B}\right)$