Metamath Proof Explorer


Theorem hstrlem4

Description: Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 hstrlem3.1
 |-  S = ( x e. CH |-> ( ( projh ` x ) ` u ) )
2 hstrlem3.2
 |-  ( ph <-> ( u e. ( A \ B ) /\ ( normh ` u ) = 1 ) )
3 hstrlem3.3
 |-  A e. CH
4 hstrlem3.4
 |-  B e. CH
5 1 hstrlem2
 |-  ( A e. CH -> ( S ` A ) = ( ( projh ` A ) ` u ) )
6 3 5 ax-mp
 |-  ( S ` A ) = ( ( projh ` A ) ` u )
7 6 fveq2i
 |-  ( normh ` ( S ` A ) ) = ( normh ` ( ( projh ` A ) ` u ) )
8 eldifi
 |-  ( u e. ( A \ B ) -> u e. A )
9 pjid
 |-  ( ( A e. CH /\ u e. A ) -> ( ( projh ` A ) ` u ) = u )
10 3 9 mpan
 |-  ( u e. A -> ( ( projh ` A ) ` u ) = u )
11 10 fveq2d
 |-  ( u e. A -> ( normh ` ( ( projh ` A ) ` u ) ) = ( normh ` u ) )
12 eqeq2
 |-  ( ( normh ` u ) = 1 -> ( ( normh ` ( ( projh ` A ) ` u ) ) = ( normh ` u ) <-> ( normh ` ( ( projh ` A ) ` u ) ) = 1 ) )
13 11 12 syl5ib
 |-  ( ( normh ` u ) = 1 -> ( u e. A -> ( normh ` ( ( projh ` A ) ` u ) ) = 1 ) )
14 8 13 mpan9
 |-  ( ( u e. ( A \ B ) /\ ( normh ` u ) = 1 ) -> ( normh ` ( ( projh ` A ) ` u ) ) = 1 )
15 2 14 sylbi
 |-  ( ph -> ( normh ` ( ( projh ` A ) ` u ) ) = 1 )
16 7 15 syl5eq
 |-  ( ph -> ( normh ` ( S ` A ) ) = 1 )