Metamath Proof Explorer

Theorem strlem4

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

Ref Expression
Hypotheses strlem3.1 
|- S = ( x e. CH |-> ( ( normh ` ( ( projh ` x ) ` u ) ) ^ 2 ) )
strlem3.2 
|- ( ph <-> ( u e. ( A \ B ) /\ ( normh ` u ) = 1 ) )
strlem3.3 
|- A e. CH
strlem3.4 
|- B e. CH
Assertion strlem4 
|- ( ph -> ( S ` A ) = 1 )

Proof

Step Hyp Ref Expression
1 strlem3.1 
 |-  S = ( x e. CH |-> ( ( normh ` ( ( projh ` x ) ` u ) ) ^ 2 ) )
2 strlem3.2 
 |-  ( ph <-> ( u e. ( A \ B ) /\ ( normh ` u ) = 1 ) )
3 strlem3.3 
 |-  A e. CH
4 strlem3.4 
 |-  B e. CH
5 1 strlem2 
 |-  ( A e. CH -> ( S ` A ) = ( ( normh ` ( ( projh ` A ) ` u ) ) ^ 2 ) )
6 3 5 ax-mp 
 |-  ( S ` A ) = ( ( normh ` ( ( projh ` A ) ` u ) ) ^ 2 )
7 eldifi 
 |-  ( u e. ( A \ B ) -> u e. A )
8 pjid 
 |-  ( ( A e. CH /\ u e. A ) -> ( ( projh ` A ) ` u ) = u )
9 3 8 mpan 
 |-  ( u e. A -> ( ( projh ` A ) ` u ) = u )
10 9 fveq2d 
 |-  ( u e. A -> ( normh ` ( ( projh ` A ) ` u ) ) = ( normh ` u ) )
11 eqeq2 
 |-  ( ( normh ` u ) = 1 -> ( ( normh ` ( ( projh ` A ) ` u ) ) = ( normh ` u ) <-> ( normh ` ( ( projh ` A ) ` u ) ) = 1 ) )
12 10 11 syl5ib 
 |-  ( ( normh ` u ) = 1 -> ( u e. A -> ( normh ` ( ( projh ` A ) ` u ) ) = 1 ) )
13 7 12 mpan9 
 |-  ( ( u e. ( A \ B ) /\ ( normh ` u ) = 1 ) -> ( normh ` ( ( projh ` A ) ` u ) ) = 1 )
14 2 13 sylbi 
 |-  ( ph -> ( normh ` ( ( projh ` A ) ` u ) ) = 1 )
15 14 oveq1d 
 |-  ( ph -> ( ( normh ` ( ( projh ` A ) ` u ) ) ^ 2 ) = ( 1 ^ 2 ) )
16 sq1 
 |-  ( 1 ^ 2 ) = 1
17 15 16 eqtrdi 
 |-  ( ph -> ( ( normh ` ( ( projh ` A ) ` u ) ) ^ 2 ) = 1 )
18 6 17 eqtrid 
 |-  ( ph -> ( S ` A ) = 1 )