# Metamath Proof Explorer

## Theorem isst

Description: Property of a state. (Contributed by NM, 23-Oct-1999) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 ovex ${⊢}\left[0,1\right]\in \mathrm{V}$
2 chex ${⊢}{\mathbf{C}}_{ℋ}\in \mathrm{V}$
3 1 2 elmap ${⊢}{S}\in \left({\left[0,1\right]}^{{\mathbf{C}}_{ℋ}}\right)↔{S}:{\mathbf{C}}_{ℋ}⟶\left[0,1\right]$
4 3 anbi1i ${⊢}\left({S}\in \left({\left[0,1\right]}^{{\mathbf{C}}_{ℋ}}\right)\wedge \left({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)\right)↔\left({S}:{\mathbf{C}}_{ℋ}⟶\left[0,1\right]\wedge \left({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)\right)$
5 fveq1 ${⊢}{f}={S}\to {f}\left(ℋ\right)={S}\left(ℋ\right)$
6 5 eqeq1d ${⊢}{f}={S}\to \left({f}\left(ℋ\right)=1↔{S}\left(ℋ\right)=1\right)$
7 fveq1 ${⊢}{f}={S}\to {f}\left({x}{\vee }_{ℋ}{y}\right)={S}\left({x}{\vee }_{ℋ}{y}\right)$
8 fveq1 ${⊢}{f}={S}\to {f}\left({x}\right)={S}\left({x}\right)$
9 fveq1 ${⊢}{f}={S}\to {f}\left({y}\right)={S}\left({y}\right)$
10 8 9 oveq12d ${⊢}{f}={S}\to {f}\left({x}\right)+{f}\left({y}\right)={S}\left({x}\right)+{S}\left({y}\right)$
11 7 10 eqeq12d ${⊢}{f}={S}\to \left({f}\left({x}{\vee }_{ℋ}{y}\right)={f}\left({x}\right)+{f}\left({y}\right)↔{S}\left({x}{\vee }_{ℋ}{y}\right)={S}\left({x}\right)+{S}\left({y}\right)\right)$
12 11 imbi2d ${⊢}{f}={S}\to \left(\left({x}\subseteq \perp \left({y}\right)\to {f}\left({x}{\vee }_{ℋ}{y}\right)={f}\left({x}\right)+{f}\left({y}\right)\right)↔\left({x}\subseteq \perp \left({y}\right)\to {S}\left({x}{\vee }_{ℋ}{y}\right)={S}\left({x}\right)+{S}\left({y}\right)\right)\right)$
13 12 2ralbidv ${⊢}{f}={S}\to \left(\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)↔\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)$
14 6 13 anbi12d ${⊢}{f}={S}\to \left(\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)↔\left({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)\right)$
15 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\}$
16 14 15 elrab2 ${⊢}{S}\in \mathrm{States}↔\left({S}\in \left({\left[0,1\right]}^{{\mathbf{C}}_{ℋ}}\right)\wedge \left({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)\right)$
17 3anass ${⊢}\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)↔\left({S}:{\mathbf{C}}_{ℋ}⟶\left[0,1\right]\wedge \left({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)\right)$
18 4 16 17 3bitr4i ${⊢}{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)$