Theorem ishst

Description: Property of a complex Hilbert-space-valued state. Definition of CH-states in Mayet3 p. 9. (Contributed by NM, 25-Jun-2006) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		ax-hilex	$$⊢\mathscr{H}\in \mathrm{V}$$
2		chex	$$⊢{\mathbf{C}}_{\mathscr{H}}\in \mathrm{V}$$
3	1 2	elmap	$$⊢S\in \left({\mathscr{H}}^{{\mathbf{C}}_{\mathscr{H}}}\right)\leftrightarrow S:{\mathbf{C}}_{\mathscr{H}}⟶\mathscr{H}$$
4	3	anbi1i	$$⊢\left(S\in \left({\mathscr{H}}^{{\mathbf{C}}_{\mathscr{H}}}\right)\wedge \left({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)\right)\leftrightarrow \left(S:{\mathbf{C}}_{\mathscr{H}}⟶\mathscr{H}\wedge \left({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)\right)$$
5		fveq1	$$⊢f=S\to f\left(\mathscr{H}\right)=S\left(\mathscr{H}\right)$$
6	5	fveqeq2d	$$⊢f=S\to \left({norm}_{ℎ}\left(f\left(\mathscr{H}\right)\right)=1\leftrightarrow {norm}_{ℎ}\left(S\left(\mathscr{H}\right)\right)=1\right)$$
7		fveq1	$$⊢f=S\to f\left(x\right)=S\left(x\right)$$
8		fveq1	$$⊢f=S\to f\left(y\right)=S\left(y\right)$$
9	7 8	oveq12d	$$⊢f=S\to f\left(x\right){\cdot }_{\mathrm{ih}}f\left(y\right)=S\left(x\right){\cdot }_{\mathrm{ih}}S\left(y\right)$$
10	9	eqeq1d	$$⊢f=S\to \left(f\left(x\right){\cdot }_{\mathrm{ih}}f\left(y\right)=0\leftrightarrow S\left(x\right){\cdot }_{\mathrm{ih}}S\left(y\right)=0\right)$$
11		fveq1	$$⊢f=S\to f\left(x{\vee }_{\mathscr{H}}y\right)=S\left(x{\vee }_{\mathscr{H}}y\right)$$
12	7 8	oveq12d	$$⊢f=S\to f\left(x\right){+}_{ℎ}f\left(y\right)=S\left(x\right){+}_{ℎ}S\left(y\right)$$
13	11 12	eqeq12d	$$⊢f=S\to \left(f\left(x{\vee }_{\mathscr{H}}y\right)=f\left(x\right){+}_{ℎ}f\left(y\right)\leftrightarrow S\left(x{\vee }_{\mathscr{H}}y\right)=S\left(x\right){+}_{ℎ}S\left(y\right)\right)$$
14	10 13	anbi12d	$$⊢f=S\to \left(\left(f\left(x\right){\cdot }_{\mathrm{ih}}f\left(y\right)=0\wedge f\left(x{\vee }_{\mathscr{H}}y\right)=f\left(x\right){+}_{ℎ}f\left(y\right)\right)\leftrightarrow \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)$$
15	14	imbi2d	$$⊢f=S\to \left(\left(x\subseteq \perp \left(y\right)\to \left(f\left(x\right){\cdot }_{\mathrm{ih}}f\left(y\right)=0\wedge f\left(x{\vee }_{\mathscr{H}}y\right)=f\left(x\right){+}_{ℎ}f\left(y\right)\right)\right)\leftrightarrow \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)$$
16	15	2ralbidv	$$⊢f=S\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(f\left(x\right){\cdot }_{\mathrm{ih}}f\left(y\right)=0\wedge f\left(x{\vee }_{\mathscr{H}}y\right)=f\left(x\right){+}_{ℎ}f\left(y\right)\right)\right)\leftrightarrow \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)$$
17	6 16	anbi12d	$$⊢f=S\to \left(\left({norm}_{ℎ}\left(f\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(f\left(x\right){\cdot }_{\mathrm{ih}}f\left(y\right)=0\wedge f\left(x{\vee }_{\mathscr{H}}y\right)=f\left(x\right){+}_{ℎ}f\left(y\right)\right)\right)\right)\leftrightarrow \left({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)\right)$$
18		df-hst	$$⊢\mathrm{CHStates}=\left\{f\in \left({\mathscr{H}}^{{\mathbf{C}}_{\mathscr{H}}}\right)|\left({norm}_{ℎ}\left(f\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(f\left(x\right){\cdot }_{\mathrm{ih}}f\left(y\right)=0\wedge f\left(x{\vee }_{\mathscr{H}}y\right)=f\left(x\right){+}_{ℎ}f\left(y\right)\right)\right)\right)\right\}$$
19	17 18	elrab2	$$⊢S\in \mathrm{CHStates}\leftrightarrow \left(S\in \left({\mathscr{H}}^{{\mathbf{C}}_{\mathscr{H}}}\right)\wedge \left({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)\right)$$
20		3anass	$$⊢\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)\leftrightarrow \left(S:{\mathbf{C}}_{\mathscr{H}}⟶\mathscr{H}\wedge \left({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)\right)$$
21	4 19 20	3bitr4i	$$⊢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)$$