Theorem strlem4

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	strlem4	$$⊢\phi \to S\left(A\right)=1$$

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