Definition df-st

Description: Define the set of states on a Hilbert lattice. Definition of Kalmbach p. 266. (Contributed by NM, 23-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	df-st	$$⊢\mathrm{States}=\left\{f\in \left({\left[0,1\right]}^{{\mathbf{C}}_{\mathscr{H}}}\right)|\left(f\left(\mathscr{H}\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 f\left(x{\vee }_{\mathscr{H}}y\right)=f\left(x\right)+f\left(y\right)\right)\right)\right\}$$

Detailed syntax breakdown

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