Theorem hstrlem5

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	hstrlem5	$$⊢\phi \to {norm}_{ℎ}\left(S\left(B\right)\right)<1$$

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	hstrlem2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}\to S\left(B\right)={\mathrm{proj}}_{ℎ}\left(B\right)\left(u\right)$$
6	5	fveq2d	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}\to {norm}_{ℎ}\left(S\left(B\right)\right)={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(u\right)\right)$$
7	4 6	ax-mp	$$⊢{norm}_{ℎ}\left(S\left(B\right)\right)={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(u\right)\right)$$
8		eldif	$$⊢u\in \left(A\setminus B\right)\leftrightarrow \left(u\in A\wedge \neg u\in B\right)$$
9	3	cheli	$$⊢u\in A\to u\in \mathscr{H}$$
10		pjnel	$$⊢\left(B\in {\mathbf{C}}_{\mathscr{H}}\wedge u\in \mathscr{H}\right)\to \left(\neg u\in B\leftrightarrow {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(u\right)\right)<{norm}_{ℎ}\left(u\right)\right)$$
11	4 10	mpan	$$⊢u\in \mathscr{H}\to \left(\neg u\in B\leftrightarrow {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(u\right)\right)<{norm}_{ℎ}\left(u\right)\right)$$
12	11	biimpa	$$⊢\left(u\in \mathscr{H}\wedge \neg u\in B\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(u\right)\right)<{norm}_{ℎ}\left(u\right)$$
13	9 12	sylan	$$⊢\left(u\in A\wedge \neg u\in B\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(u\right)\right)<{norm}_{ℎ}\left(u\right)$$
14	8 13	sylbi	$$⊢u\in \left(A\setminus B\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(u\right)\right)<{norm}_{ℎ}\left(u\right)$$
15		breq2	$$⊢{norm}_{ℎ}\left(u\right)=1\to \left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(u\right)\right)<{norm}_{ℎ}\left(u\right)\leftrightarrow {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(u\right)\right)<1\right)$$
16	14 15	imbitrid	$$⊢{norm}_{ℎ}\left(u\right)=1\to \left(u\in \left(A\setminus B\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(u\right)\right)<1\right)$$
17	16	impcom	$$⊢\left(u\in \left(A\setminus B\right)\wedge {norm}_{ℎ}\left(u\right)=1\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(u\right)\right)<1$$
18	7 17	eqbrtrid	$$⊢\left(u\in \left(A\setminus B\right)\wedge {norm}_{ℎ}\left(u\right)=1\right)\to {norm}_{ℎ}\left(S\left(B\right)\right)<1$$
19	2 18	sylbi	$$⊢\phi \to {norm}_{ℎ}\left(S\left(B\right)\right)<1$$