Theorem hstrlem6

Description: Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		hstrlem3.1	$$⊢S=\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)$$
2		hstrlem3.2	$$⊢\phi \leftrightarrow \left(u\in \left(A\setminus B\right)\wedge {norm}_{ℎ}\left(u\right)=1\right)$$
3		hstrlem3.3	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
4		hstrlem3.4	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
5	1 2 3 4	hstrlem4	$$⊢\phi \to {norm}_{ℎ}\left(S\left(A\right)\right)=1$$
6	1 2 3 4	hstrlem3	$$⊢\phi \to S\in \mathrm{CHStates}$$
7		hstcl	$$⊢\left(S\in \mathrm{CHStates}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to S\left(B\right)\in \mathscr{H}$$
8	6 4 7	sylancl	$$⊢\phi \to S\left(B\right)\in \mathscr{H}$$
9		normcl	$$⊢S\left(B\right)\in \mathscr{H}\to {norm}_{ℎ}\left(S\left(B\right)\right)\in ℝ$$
10	8 9	syl	$$⊢\phi \to {norm}_{ℎ}\left(S\left(B\right)\right)\in ℝ$$
11	1 2 3 4	hstrlem5	$$⊢\phi \to {norm}_{ℎ}\left(S\left(B\right)\right)<1$$
12	10 11	ltned	$$⊢\phi \to {norm}_{ℎ}\left(S\left(B\right)\right)\ne 1$$
13	12	neneqd	$$⊢\phi \to \neg {norm}_{ℎ}\left(S\left(B\right)\right)=1$$
14	5 13	jcnd	$$⊢\phi \to \neg \left({norm}_{ℎ}\left(S\left(A\right)\right)=1\to {norm}_{ℎ}\left(S\left(B\right)\right)=1\right)$$