# Metamath Proof Explorer

## 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}}_{ℋ}}\right)|\left({f}\left(ℋ\right)=1\wedge \forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq \perp \left({y}\right)\to {f}\left({x}{\vee }_{ℋ}{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 ${setvar}{f}$
2 cc0 ${class}0$
3 cicc ${class}\left[.\right]$
4 c1 ${class}1$
5 2 4 3 co ${class}\left[0,1\right]$
6 cmap ${class}{↑}_{𝑚}$
7 cch ${class}{\mathbf{C}}_{ℋ}$
8 5 7 6 co ${class}\left({\left[0,1\right]}^{{\mathbf{C}}_{ℋ}}\right)$
9 1 cv ${setvar}{f}$
10 chba ${class}ℋ$
11 10 9 cfv ${class}{f}\left(ℋ\right)$
12 11 4 wceq ${wff}{f}\left(ℋ\right)=1$
13 vx ${setvar}{x}$
14 vy ${setvar}{y}$
15 13 cv ${setvar}{x}$
16 cort ${class}\perp$
17 14 cv ${setvar}{y}$
18 17 16 cfv ${class}\perp \left({y}\right)$
19 15 18 wss ${wff}{x}\subseteq \perp \left({y}\right)$
20 chj ${class}{\vee }_{ℋ}$
21 15 17 20 co ${class}\left({x}{\vee }_{ℋ}{y}\right)$
22 21 9 cfv ${class}{f}\left({x}{\vee }_{ℋ}{y}\right)$
23 15 9 cfv ${class}{f}\left({x}\right)$
24 caddc ${class}+$
25 17 9 cfv ${class}{f}\left({y}\right)$
26 23 25 24 co ${class}\left({f}\left({x}\right)+{f}\left({y}\right)\right)$
27 22 26 wceq ${wff}{f}\left({x}{\vee }_{ℋ}{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 }_{ℋ}{y}\right)={f}\left({x}\right)+{f}\left({y}\right)\right)$
29 28 14 7 wral ${wff}\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq \perp \left({y}\right)\to {f}\left({x}{\vee }_{ℋ}{y}\right)={f}\left({x}\right)+{f}\left({y}\right)\right)$
30 29 13 7 wral ${wff}\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq \perp \left({y}\right)\to {f}\left({x}{\vee }_{ℋ}{y}\right)={f}\left({x}\right)+{f}\left({y}\right)\right)$
31 12 30 wa ${wff}\left({f}\left(ℋ\right)=1\wedge \forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq \perp \left({y}\right)\to {f}\left({x}{\vee }_{ℋ}{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}}_{ℋ}}\right)|\left({f}\left(ℋ\right)=1\wedge \forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq \perp \left({y}\right)\to {f}\left({x}{\vee }_{ℋ}{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}}_{ℋ}}\right)|\left({f}\left(ℋ\right)=1\wedge \forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq \perp \left({y}\right)\to {f}\left({x}{\vee }_{ℋ}{y}\right)={f}\left({x}\right)+{f}\left({y}\right)\right)\right)\right\}$