Definition df-hst

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chst	$$class\mathrm{CHStates}$$
1		vf	$$setvarf$$
2		chba	$$class\mathscr{H}$$
3		cmap	$$class{\uparrow }_{𝑚}$$
4		cch	$$class{\mathbf{C}}_{\mathscr{H}}$$
5	2 4 3	co	$$class\left({\mathscr{H}}^{{\mathbf{C}}_{\mathscr{H}}}\right)$$
6		cno	$$class{norm}_{ℎ}$$
7	1	cv	$$setvarf$$
8	2 7	cfv	$$classf\left(\mathscr{H}\right)$$
9	8 6	cfv	$$class{norm}_{ℎ}\left(f\left(\mathscr{H}\right)\right)$$
10		c1	$$class1$$
11	9 10	wceq	$$wff{norm}_{ℎ}\left(f\left(\mathscr{H}\right)\right)=1$$
12		vx	$$setvarx$$
13		vy	$$setvary$$
14	12	cv	$$setvarx$$
15		cort	$$class\perp$$
16	13	cv	$$setvary$$
17	16 15	cfv	$$class\perp \left(y\right)$$
18	14 17	wss	$$wffx\subseteq \perp \left(y\right)$$
19	14 7	cfv	$$classf\left(x\right)$$
20		csp	$$class{\cdot }_{\mathrm{ih}}$$
21	16 7	cfv	$$classf\left(y\right)$$
22	19 21 20	co	$$class\left(f\left(x\right){\cdot }_{\mathrm{ih}}f\left(y\right)\right)$$
23		cc0	$$class0$$
24	22 23	wceq	$$wfff\left(x\right){\cdot }_{\mathrm{ih}}f\left(y\right)=0$$
25		chj	$$class{\vee }_{\mathscr{H}}$$
26	14 16 25	co	$$class\left(x{\vee }_{\mathscr{H}}y\right)$$
27	26 7	cfv	$$classf\left(x{\vee }_{\mathscr{H}}y\right)$$
28		cva	$$class{+}_{ℎ}$$
29	19 21 28	co	$$class\left(f\left(x\right){+}_{ℎ}f\left(y\right)\right)$$
30	27 29	wceq	$$wfff\left(x{\vee }_{\mathscr{H}}y\right)=f\left(x\right){+}_{ℎ}f\left(y\right)$$
31	24 30	wa	$$wff\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)$$
32	18 31	wi	$$wff\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)$$
33	32 13 4	wral	$$wff\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)$$
34	33 12 4	wral	$$wff\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)$$
35	11 34	wa	$$wff\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)$$
36	35 1 5	crab	$$class\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\}$$
37	0 36	wceq	$$wff\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\}$$