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 = ( x e. CH |-> ( ( normh ` ( ( projh ` x ) ` u ) ) ^ 2 ) )
Assertion strlem2 
|- ( C e. CH -> ( S ` C ) = ( ( normh ` ( ( projh ` C ) ` u ) ) ^ 2 ) )

Proof

Step Hyp Ref Expression
1 strlem2.1 
 |-  S = ( x e. CH |-> ( ( normh ` ( ( projh ` x ) ` u ) ) ^ 2 ) )
2 fveq2 
 |-  ( x = C -> ( projh ` x ) = ( projh ` C ) )
3 2 fveq1d 
 |-  ( x = C -> ( ( projh ` x ) ` u ) = ( ( projh ` C ) ` u ) )
4 3 fveq2d 
 |-  ( x = C -> ( normh ` ( ( projh ` x ) ` u ) ) = ( normh ` ( ( projh ` C ) ` u ) ) )
5 4 oveq1d 
 |-  ( x = C -> ( ( normh ` ( ( projh ` x ) ` u ) ) ^ 2 ) = ( ( normh ` ( ( projh ` C ) ` u ) ) ^ 2 ) )
6 ovex 
 |-  ( ( normh ` ( ( projh ` C ) ` u ) ) ^ 2 ) e. _V
7 5 1 6 fvmpt 
 |-  ( C e. CH -> ( S ` C ) = ( ( normh ` ( ( projh ` C ) ` u ) ) ^ 2 ) )