# Metamath Proof Explorer

## Theorem sticl

Description: [ 0 , 1 ] closure of the value of a state. (Contributed by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion sticl ${⊢}{S}\in \mathrm{States}\to \left({A}\in {\mathbf{C}}_{ℋ}\to {S}\left({A}\right)\in \left[0,1\right]\right)$

### Proof

Step Hyp Ref Expression
1 isst ${⊢}{S}\in \mathrm{States}↔\left({S}:{\mathbf{C}}_{ℋ}⟶\left[0,1\right]\wedge {S}\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 {S}\left({x}{\vee }_{ℋ}{y}\right)={S}\left({x}\right)+{S}\left({y}\right)\right)\right)$
2 1 simp1bi ${⊢}{S}\in \mathrm{States}\to {S}:{\mathbf{C}}_{ℋ}⟶\left[0,1\right]$
3 ffvelrn ${⊢}\left({S}:{\mathbf{C}}_{ℋ}⟶\left[0,1\right]\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to {S}\left({A}\right)\in \left[0,1\right]$
4 3 ex ${⊢}{S}:{\mathbf{C}}_{ℋ}⟶\left[0,1\right]\to \left({A}\in {\mathbf{C}}_{ℋ}\to {S}\left({A}\right)\in \left[0,1\right]\right)$
5 2 4 syl ${⊢}{S}\in \mathrm{States}\to \left({A}\in {\mathbf{C}}_{ℋ}\to {S}\left({A}\right)\in \left[0,1\right]\right)$