Theorem strlem6

Description: Lemma for strong state theorem. (Contributed by NM, 2-Nov-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	strlem3.1	$$⊢S=\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)}^2\right)$$
	strlem3.2	$$⊢\phi \leftrightarrow \left(u\in \left(A\setminus B\right)\wedge {norm}_{ℎ}\left(u\right)=1\right)$$
	strlem3.3	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	strlem3.4	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	strlem6	$$⊢\phi \to \neg \left(S\left(A\right)=1\to S\left(B\right)=1\right)$$

Proof

Step	Hyp	Ref	Expression
1		strlem3.1	$$⊢S=\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)}^2\right)$$
2		strlem3.2	$$⊢\phi \leftrightarrow \left(u\in \left(A\setminus B\right)\wedge {norm}_{ℎ}\left(u\right)=1\right)$$
3		strlem3.3	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
4		strlem3.4	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
5	1 2 3 4	strlem4	$$⊢\phi \to S\left(A\right)=1$$
6	1 2 3 4	strlem3	$$⊢\phi \to S\in \mathrm{States}$$
7		stcl	$$⊢S\in \mathrm{States}\to \left(B\in {\mathbf{C}}_{\mathscr{H}}\to S\left(B\right)\in ℝ\right)$$
8	6 4 7	mpisyl	$$⊢\phi \to S\left(B\right)\in ℝ$$
9	1 2 3 4	strlem5	$$⊢\phi \to S\left(B\right)<1$$
10	8 9	ltned	$$⊢\phi \to S\left(B\right)\ne 1$$
11	10	neneqd	$$⊢\phi \to \neg S\left(B\right)=1$$
12	5 11	jcnd	$$⊢\phi \to \neg \left(S\left(A\right)=1\to S\left(B\right)=1\right)$$