Theorem hstel2

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

	Ref	Expression
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		ishst	$$⊢S\in \mathrm{CHStates}\leftrightarrow \left(S:{\mathbf{C}}_{\mathscr{H}}⟶\mathscr{H}\wedge {norm}_{ℎ}\left(S\left(\mathscr{H}\right)\right)=1\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq \perp \left(y\right)\to \left(S\left(x\right){\cdot }_{\mathrm{ih}}S\left(y\right)=0\wedge S\left(x{\vee }_{\mathscr{H}}y\right)=S\left(x\right){+}_{ℎ}S\left(y\right)\right)\right)\right)$$
2	1	simp3bi	$$⊢S\in \mathrm{CHStates}\to \forall x\in {\mathbf{C}}_{\mathscr{H}}\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq \perp \left(y\right)\to \left(S\left(x\right){\cdot }_{\mathrm{ih}}S\left(y\right)=0\wedge S\left(x{\vee }_{\mathscr{H}}y\right)=S\left(x\right){+}_{ℎ}S\left(y\right)\right)\right)$$
3	2	ad2antrr	$$⊢\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 \forall x\in {\mathbf{C}}_{\mathscr{H}}\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq \perp \left(y\right)\to \left(S\left(x\right){\cdot }_{\mathrm{ih}}S\left(y\right)=0\wedge S\left(x{\vee }_{\mathscr{H}}y\right)=S\left(x\right){+}_{ℎ}S\left(y\right)\right)\right)$$
4		sseq1	$$⊢x=A\to \left(x\subseteq \perp \left(y\right)\leftrightarrow A\subseteq \perp \left(y\right)\right)$$
5		fveq2	$$⊢x=A\to S\left(x\right)=S\left(A\right)$$
6	5	oveq1d	$$⊢x=A\to S\left(x\right){\cdot }_{\mathrm{ih}}S\left(y\right)=S\left(A\right){\cdot }_{\mathrm{ih}}S\left(y\right)$$
7	6	eqeq1d	$$⊢x=A\to \left(S\left(x\right){\cdot }_{\mathrm{ih}}S\left(y\right)=0\leftrightarrow S\left(A\right){\cdot }_{\mathrm{ih}}S\left(y\right)=0\right)$$
8		fvoveq1	$$⊢x=A\to S\left(x{\vee }_{\mathscr{H}}y\right)=S\left(A{\vee }_{\mathscr{H}}y\right)$$
9	5	oveq1d	$$⊢x=A\to S\left(x\right){+}_{ℎ}S\left(y\right)=S\left(A\right){+}_{ℎ}S\left(y\right)$$
10	8 9	eqeq12d	$$⊢x=A\to \left(S\left(x{\vee }_{\mathscr{H}}y\right)=S\left(x\right){+}_{ℎ}S\left(y\right)\leftrightarrow S\left(A{\vee }_{\mathscr{H}}y\right)=S\left(A\right){+}_{ℎ}S\left(y\right)\right)$$
11	7 10	anbi12d	$$⊢x=A\to \left(\left(S\left(x\right){\cdot }_{\mathrm{ih}}S\left(y\right)=0\wedge S\left(x{\vee }_{\mathscr{H}}y\right)=S\left(x\right){+}_{ℎ}S\left(y\right)\right)\leftrightarrow \left(S\left(A\right){\cdot }_{\mathrm{ih}}S\left(y\right)=0\wedge S\left(A{\vee }_{\mathscr{H}}y\right)=S\left(A\right){+}_{ℎ}S\left(y\right)\right)\right)$$
12	4 11	imbi12d	$$⊢x=A\to \left(\left(x\subseteq \perp \left(y\right)\to \left(S\left(x\right){\cdot }_{\mathrm{ih}}S\left(y\right)=0\wedge S\left(x{\vee }_{\mathscr{H}}y\right)=S\left(x\right){+}_{ℎ}S\left(y\right)\right)\right)\leftrightarrow \left(A\subseteq \perp \left(y\right)\to \left(S\left(A\right){\cdot }_{\mathrm{ih}}S\left(y\right)=0\wedge S\left(A{\vee }_{\mathscr{H}}y\right)=S\left(A\right){+}_{ℎ}S\left(y\right)\right)\right)\right)$$
13		fveq2	$$⊢y=B\to \perp \left(y\right)=\perp \left(B\right)$$
14	13	sseq2d	$$⊢y=B\to \left(A\subseteq \perp \left(y\right)\leftrightarrow A\subseteq \perp \left(B\right)\right)$$
15		fveq2	$$⊢y=B\to S\left(y\right)=S\left(B\right)$$
16	15	oveq2d	$$⊢y=B\to S\left(A\right){\cdot }_{\mathrm{ih}}S\left(y\right)=S\left(A\right){\cdot }_{\mathrm{ih}}S\left(B\right)$$
17	16	eqeq1d	$$⊢y=B\to \left(S\left(A\right){\cdot }_{\mathrm{ih}}S\left(y\right)=0\leftrightarrow S\left(A\right){\cdot }_{\mathrm{ih}}S\left(B\right)=0\right)$$
18		oveq2	$$⊢y=B\to A{\vee }_{\mathscr{H}}y=A{\vee }_{\mathscr{H}}B$$
19	18	fveq2d	$$⊢y=B\to S\left(A{\vee }_{\mathscr{H}}y\right)=S\left(A{\vee }_{\mathscr{H}}B\right)$$
20	15	oveq2d	$$⊢y=B\to S\left(A\right){+}_{ℎ}S\left(y\right)=S\left(A\right){+}_{ℎ}S\left(B\right)$$
21	19 20	eqeq12d	$$⊢y=B\to \left(S\left(A{\vee }_{\mathscr{H}}y\right)=S\left(A\right){+}_{ℎ}S\left(y\right)\leftrightarrow S\left(A{\vee }_{\mathscr{H}}B\right)=S\left(A\right){+}_{ℎ}S\left(B\right)\right)$$
22	17 21	anbi12d	$$⊢y=B\to \left(\left(S\left(A\right){\cdot }_{\mathrm{ih}}S\left(y\right)=0\wedge S\left(A{\vee }_{\mathscr{H}}y\right)=S\left(A\right){+}_{ℎ}S\left(y\right)\right)\leftrightarrow \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)\right)$$
23	14 22	imbi12d	$$⊢y=B\to \left(\left(A\subseteq \perp \left(y\right)\to \left(S\left(A\right){\cdot }_{\mathrm{ih}}S\left(y\right)=0\wedge S\left(A{\vee }_{\mathscr{H}}y\right)=S\left(A\right){+}_{ℎ}S\left(y\right)\right)\right)\leftrightarrow \left(A\subseteq \perp \left(B\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)\right)\right)$$
24	12 23	rspc2v	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\forall x\in {\mathbf{C}}_{\mathscr{H}}\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq \perp \left(y\right)\to \left(S\left(x\right){\cdot }_{\mathrm{ih}}S\left(y\right)=0\wedge S\left(x{\vee }_{\mathscr{H}}y\right)=S\left(x\right){+}_{ℎ}S\left(y\right)\right)\right)\to \left(A\subseteq \perp \left(B\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)\right)\right)$$
25	24	com23	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A\subseteq \perp \left(B\right)\to \left(\forall x\in {\mathbf{C}}_{\mathscr{H}}\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq \perp \left(y\right)\to \left(S\left(x\right){\cdot }_{\mathrm{ih}}S\left(y\right)=0\wedge S\left(x{\vee }_{\mathscr{H}}y\right)=S\left(x\right){+}_{ℎ}S\left(y\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)\right)\right)$$
26	25	impr	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \left(B\in {\mathbf{C}}_{\mathscr{H}}\wedge A\subseteq \perp \left(B\right)\right)\right)\to \left(\forall x\in {\mathbf{C}}_{\mathscr{H}}\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq \perp \left(y\right)\to \left(S\left(x\right){\cdot }_{\mathrm{ih}}S\left(y\right)=0\wedge S\left(x{\vee }_{\mathscr{H}}y\right)=S\left(x\right){+}_{ℎ}S\left(y\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)\right)$$
27	26	adantll	$$⊢\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(\forall x\in {\mathbf{C}}_{\mathscr{H}}\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq \perp \left(y\right)\to \left(S\left(x\right){\cdot }_{\mathrm{ih}}S\left(y\right)=0\wedge S\left(x{\vee }_{\mathscr{H}}y\right)=S\left(x\right){+}_{ℎ}S\left(y\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)\right)$$
28	3 27	mpd	$$⊢\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)$$