Theorem stj

Description: The value of a state on a join. (Contributed by NM, 23-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	stj	$$⊢S\in \mathrm{States}\to \left(\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge A\subseteq \perp \left(B\right)\right)\to S\left(A{\vee }_{\mathscr{H}}B\right)=S\left(A\right)+S\left(B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		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)$$
2	1	simp3bi	$$⊢S\in \mathrm{States}\to \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)$$
3		sseq1	$$⊢x=A\to \left(x\subseteq \perp \left(y\right)\leftrightarrow A\subseteq \perp \left(y\right)\right)$$
4		fvoveq1	$$⊢x=A\to S\left(x{\vee }_{\mathscr{H}}y\right)=S\left(A{\vee }_{\mathscr{H}}y\right)$$
5		fveq2	$$⊢x=A\to S\left(x\right)=S\left(A\right)$$
6	5	oveq1d	$$⊢x=A\to S\left(x\right)+S\left(y\right)=S\left(A\right)+S\left(y\right)$$
7	4 6	eqeq12d	$$⊢x=A\to \left(S\left(x{\vee }_{\mathscr{H}}y\right)=S\left(x\right)+S\left(y\right)\leftrightarrow S\left(A{\vee }_{\mathscr{H}}y\right)=S\left(A\right)+S\left(y\right)\right)$$
8	3 7	imbi12d	$$⊢x=A\to \left(\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)\leftrightarrow \left(A\subseteq \perp \left(y\right)\to S\left(A{\vee }_{\mathscr{H}}y\right)=S\left(A\right)+S\left(y\right)\right)\right)$$
9		fveq2	$$⊢y=B\to \perp \left(y\right)=\perp \left(B\right)$$
10	9	sseq2d	$$⊢y=B\to \left(A\subseteq \perp \left(y\right)\leftrightarrow A\subseteq \perp \left(B\right)\right)$$
11		oveq2	$$⊢y=B\to A{\vee }_{\mathscr{H}}y=A{\vee }_{\mathscr{H}}B$$
12	11	fveq2d	$$⊢y=B\to S\left(A{\vee }_{\mathscr{H}}y\right)=S\left(A{\vee }_{\mathscr{H}}B\right)$$
13		fveq2	$$⊢y=B\to S\left(y\right)=S\left(B\right)$$
14	13	oveq2d	$$⊢y=B\to S\left(A\right)+S\left(y\right)=S\left(A\right)+S\left(B\right)$$
15	12 14	eqeq12d	$$⊢y=B\to \left(S\left(A{\vee }_{\mathscr{H}}y\right)=S\left(A\right)+S\left(y\right)\leftrightarrow S\left(A{\vee }_{\mathscr{H}}B\right)=S\left(A\right)+S\left(B\right)\right)$$
16	10 15	imbi12d	$$⊢y=B\to \left(\left(A\subseteq \perp \left(y\right)\to S\left(A{\vee }_{\mathscr{H}}y\right)=S\left(A\right)+S\left(y\right)\right)\leftrightarrow \left(A\subseteq \perp \left(B\right)\to S\left(A{\vee }_{\mathscr{H}}B\right)=S\left(A\right)+S\left(B\right)\right)\right)$$
17	8 16	rspc2v	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\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)\to \left(A\subseteq \perp \left(B\right)\to S\left(A{\vee }_{\mathscr{H}}B\right)=S\left(A\right)+S\left(B\right)\right)\right)$$
18	2 17	syl5com	$$⊢S\in \mathrm{States}\to \left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A\subseteq \perp \left(B\right)\to S\left(A{\vee }_{\mathscr{H}}B\right)=S\left(A\right)+S\left(B\right)\right)\right)$$
19	18	impd	$$⊢S\in \mathrm{States}\to \left(\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge A\subseteq \perp \left(B\right)\right)\to S\left(A{\vee }_{\mathscr{H}}B\right)=S\left(A\right)+S\left(B\right)\right)$$