Theorem stm1addi

Description: Sum of states whose meet is 1. (Contributed by NM, 11-Nov-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	stle.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	stle.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	stm1addi	$$⊢S\in \mathrm{States}\to \left(S\left(A\cap B\right)=1\to S\left(A\right)+S\left(B\right)=2\right)$$

Proof

Step	Hyp	Ref	Expression
1		stle.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		stle.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3	1 2	stm1i	$$⊢S\in \mathrm{States}\to \left(S\left(A\cap B\right)=1\to S\left(A\right)=1\right)$$
4	1 2	stm1ri	$$⊢S\in \mathrm{States}\to \left(S\left(A\cap B\right)=1\to S\left(B\right)=1\right)$$
5	3 4	jcad	$$⊢S\in \mathrm{States}\to \left(S\left(A\cap B\right)=1\to \left(S\left(A\right)=1\wedge S\left(B\right)=1\right)\right)$$
6		oveq12	$$⊢\left(S\left(A\right)=1\wedge S\left(B\right)=1\right)\to S\left(A\right)+S\left(B\right)=1+1$$
7		df-2	$$⊢2=1+1$$
8	6 7	syl6eqr	$$⊢\left(S\left(A\right)=1\wedge S\left(B\right)=1\right)\to S\left(A\right)+S\left(B\right)=2$$
9	5 8	syl6	$$⊢S\in \mathrm{States}\to \left(S\left(A\cap B\right)=1\to S\left(A\right)+S\left(B\right)=2\right)$$