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}\leftrightarrow \left(S:{\mathbf{C}}_{\mathscr{H}}⟶\left[0,1\right]\wedge S\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 S\left(x{\vee }_{\mathscr{H}}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}}_{\mathscr{H}}\in \mathrm{V}$$
3	1 2	elmap	$$⊢S\in \left({\left[0,1\right]}^{{\mathbf{C}}_{\mathscr{H}}}\right)\leftrightarrow S:{\mathbf{C}}_{\mathscr{H}}⟶\left[0,1\right]$$
4	3	anbi1i	$$⊢\left(S\in \left({\left[0,1\right]}^{{\mathbf{C}}_{\mathscr{H}}}\right)\wedge \left(S\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 S\left(x{\vee }_{\mathscr{H}}y\right)=S\left(x\right)+S\left(y\right)\right)\right)\right)\leftrightarrow \left(S:{\mathbf{C}}_{\mathscr{H}}⟶\left[0,1\right]\wedge \left(S\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 S\left(x{\vee }_{\mathscr{H}}y\right)=S\left(x\right)+S\left(y\right)\right)\right)\right)$$
5		fveq1	$$⊢f=S\to f\left(\mathscr{H}\right)=S\left(\mathscr{H}\right)$$
6	5	eqeq1d	$$⊢f=S\to \left(f\left(\mathscr{H}\right)=1\leftrightarrow S\left(\mathscr{H}\right)=1\right)$$
7		fveq1	$$⊢f=S\to f\left(x{\vee }_{\mathscr{H}}y\right)=S\left(x{\vee }_{\mathscr{H}}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 }_{\mathscr{H}}y\right)=f\left(x\right)+f\left(y\right)\leftrightarrow S\left(x{\vee }_{\mathscr{H}}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 }_{\mathscr{H}}y\right)=f\left(x\right)+f\left(y\right)\right)\leftrightarrow \left(x\subseteq \perp \left(y\right)\to S\left(x{\vee }_{\mathscr{H}}y\right)=S\left(x\right)+S\left(y\right)\right)\right)$$
13	12	2ralbidv	$$⊢f=S\to \left(\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)\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq \perp \left(y\right)\to S\left(x{\vee }_{\mathscr{H}}y\right)=S\left(x\right)+S\left(y\right)\right)\right)$$
14	6 13	anbi12d	$$⊢f=S\to \left(\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)\leftrightarrow \left(S\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 S\left(x{\vee }_{\mathscr{H}}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}}_{\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\}$$
16	14 15	elrab2	$$⊢S\in \mathrm{States}\leftrightarrow \left(S\in \left({\left[0,1\right]}^{{\mathbf{C}}_{\mathscr{H}}}\right)\wedge \left(S\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 S\left(x{\vee }_{\mathscr{H}}y\right)=S\left(x\right)+S\left(y\right)\right)\right)\right)$$
17		3anass	$$⊢\left(S:{\mathbf{C}}_{\mathscr{H}}⟶\left[0,1\right]\wedge S\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 S\left(x{\vee }_{\mathscr{H}}y\right)=S\left(x\right)+S\left(y\right)\right)\right)\leftrightarrow \left(S:{\mathbf{C}}_{\mathscr{H}}⟶\left[0,1\right]\wedge \left(S\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 S\left(x{\vee }_{\mathscr{H}}y\right)=S\left(x\right)+S\left(y\right)\right)\right)\right)$$
18	4 16 17	3bitr4i	$$⊢S\in \mathrm{States}\leftrightarrow \left(S:{\mathbf{C}}_{\mathscr{H}}⟶\left[0,1\right]\wedge S\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 S\left(x{\vee }_{\mathscr{H}}y\right)=S\left(x\right)+S\left(y\right)\right)\right)$$