Theorem hstrlem4

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	hstrlem4	$$⊢\phi \to {norm}_{ℎ}\left(S\left(A\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	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to S\left(A\right)={\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)$$
6	3 5	ax-mp	$$⊢S\left(A\right)={\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)$$
7	6	fveq2i	$$⊢{norm}_{ℎ}\left(S\left(A\right)\right)={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)$$
8		eldifi	$$⊢u\in \left(A\setminus B\right)\to u\in A$$
9		pjid	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge u\in A\right)\to {\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)=u$$
10	3 9	mpan	$$⊢u\in A\to {\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)=u$$
11	10	fveq2d	$$⊢u\in A\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)={norm}_{ℎ}\left(u\right)$$
12		eqeq2	$$⊢{norm}_{ℎ}\left(u\right)=1\to \left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)={norm}_{ℎ}\left(u\right)\leftrightarrow {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)=1\right)$$
13	11 12	imbitrid	$$⊢{norm}_{ℎ}\left(u\right)=1\to \left(u\in A\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)=1\right)$$
14	8 13	mpan9	$$⊢\left(u\in \left(A\setminus B\right)\wedge {norm}_{ℎ}\left(u\right)=1\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)=1$$
15	2 14	sylbi	$$⊢\phi \to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)=1$$
16	7 15	eqtrid	$$⊢\phi \to {norm}_{ℎ}\left(S\left(A\right)\right)=1$$