Theorem strlem2

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

	Ref	Expression
Hypothesis	strlem2.1	$$⊢S=\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)}^2\right)$$
Assertion	strlem2	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}\to S\left(C\right)={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(C\right)\left(u\right)\right)}^2$$

Proof

Step	Hyp	Ref	Expression
1		strlem2.1	$$⊢S=\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)}^2\right)$$
2		fveq2	$$⊢x=C\to {\mathrm{proj}}_{ℎ}\left(x\right)={\mathrm{proj}}_{ℎ}\left(C\right)$$
3	2	fveq1d	$$⊢x=C\to {\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)={\mathrm{proj}}_{ℎ}\left(C\right)\left(u\right)$$
4	3	fveq2d	$$⊢x=C\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(C\right)\left(u\right)\right)$$
5	4	oveq1d	$$⊢x=C\to {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(C\right)\left(u\right)\right)}^2$$
6		ovex	$$⊢{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(C\right)\left(u\right)\right)}^2\in \mathrm{V}$$
7	5 1 6	fvmpt	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}\to S\left(C\right)={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(C\right)\left(u\right)\right)}^2$$