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