# Metamath Proof Explorer

## 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}}_{ℋ}⟼{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({x}\right)\left({u}\right)\right)}^{2}\right)$
Assertion strlem2 ${⊢}{C}\in {\mathbf{C}}_{ℋ}\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}}_{ℋ}⟼{{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}}_{ℋ}\to {S}\left({C}\right)={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({C}\right)\left({u}\right)\right)}^{2}$