Metamath Proof Explorer

Theorem strlem5

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 strlem5 
|- ( ph -> ( S ` B ) < 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 
 |-  ( B e. CH -> ( S ` B ) = ( ( normh ` ( ( projh ` B ) ` u ) ) ^ 2 ) )
6 4 5 ax-mp 
 |-  ( S ` B ) = ( ( normh ` ( ( projh ` B ) ` u ) ) ^ 2 )
7 eldif 
 |-  ( u e. ( A \ B ) <-> ( u e. A /\ -. u e. B ) )
8 3 cheli 
 |-  ( u e. A -> u e. ~H )
9 pjnel 
 |-  ( ( B e. CH /\ u e. ~H ) -> ( -. u e. B <-> ( normh ` ( ( projh ` B ) ` u ) ) < ( normh ` u ) ) )
10 4 9 mpan 
 |-  ( u e. ~H -> ( -. u e. B <-> ( normh ` ( ( projh ` B ) ` u ) ) < ( normh ` u ) ) )
11 10 biimpa 
 |-  ( ( u e. ~H /\ -. u e. B ) -> ( normh ` ( ( projh ` B ) ` u ) ) < ( normh ` u ) )
12 8 11 sylan 
 |-  ( ( u e. A /\ -. u e. B ) -> ( normh ` ( ( projh ` B ) ` u ) ) < ( normh ` u ) )
13 7 12 sylbi 
 |-  ( u e. ( A \ B ) -> ( normh ` ( ( projh ` B ) ` u ) ) < ( normh ` u ) )
14 breq2 
 |-  ( ( normh ` u ) = 1 -> ( ( normh ` ( ( projh ` B ) ` u ) ) < ( normh ` u ) <-> ( normh ` ( ( projh ` B ) ` u ) ) < 1 ) )
15 13 14 syl5ib 
 |-  ( ( normh ` u ) = 1 -> ( u e. ( A \ B ) -> ( normh ` ( ( projh ` B ) ` u ) ) < 1 ) )
16 15 impcom 
 |-  ( ( u e. ( A \ B ) /\ ( normh ` u ) = 1 ) -> ( normh ` ( ( projh ` B ) ` u ) ) < 1 )
17 eldifi 
 |-  ( u e. ( A \ B ) -> u e. A )
18 4 pjhcli 
 |-  ( u e. ~H -> ( ( projh ` B ) ` u ) e. ~H )
19 normcl 
 |-  ( ( ( projh ` B ) ` u ) e. ~H -> ( normh ` ( ( projh ` B ) ` u ) ) e. RR )
20 18 19 syl 
 |-  ( u e. ~H -> ( normh ` ( ( projh ` B ) ` u ) ) e. RR )
21 normge0 
 |-  ( ( ( projh ` B ) ` u ) e. ~H -> 0 <_ ( normh ` ( ( projh ` B ) ` u ) ) )
22 18 21 syl 
 |-  ( u e. ~H -> 0 <_ ( normh ` ( ( projh ` B ) ` u ) ) )
23 1re 
 |-  1 e. RR
24 0le1 
 |-  0 <_ 1
25 lt2sq 
 |-  ( ( ( ( normh ` ( ( projh ` B ) ` u ) ) e. RR /\ 0 <_ ( normh ` ( ( projh ` B ) ` u ) ) ) /\ ( 1 e. RR /\ 0 <_ 1 ) ) -> ( ( normh ` ( ( projh ` B ) ` u ) ) < 1 <-> ( ( normh ` ( ( projh ` B ) ` u ) ) ^ 2 ) < ( 1 ^ 2 ) ) )
26 23 24 25 mpanr12 
 |-  ( ( ( normh ` ( ( projh ` B ) ` u ) ) e. RR /\ 0 <_ ( normh ` ( ( projh ` B ) ` u ) ) ) -> ( ( normh ` ( ( projh ` B ) ` u ) ) < 1 <-> ( ( normh ` ( ( projh ` B ) ` u ) ) ^ 2 ) < ( 1 ^ 2 ) ) )
27 20 22 26 syl2anc 
 |-  ( u e. ~H -> ( ( normh ` ( ( projh ` B ) ` u ) ) < 1 <-> ( ( normh ` ( ( projh ` B ) ` u ) ) ^ 2 ) < ( 1 ^ 2 ) ) )
28 17 8 27 3syl 
 |-  ( u e. ( A \ B ) -> ( ( normh ` ( ( projh ` B ) ` u ) ) < 1 <-> ( ( normh ` ( ( projh ` B ) ` u ) ) ^ 2 ) < ( 1 ^ 2 ) ) )
29 28 adantr 
 |-  ( ( u e. ( A \ B ) /\ ( normh ` u ) = 1 ) -> ( ( normh ` ( ( projh ` B ) ` u ) ) < 1 <-> ( ( normh ` ( ( projh ` B ) ` u ) ) ^ 2 ) < ( 1 ^ 2 ) ) )
30 16 29 mpbid 
 |-  ( ( u e. ( A \ B ) /\ ( normh ` u ) = 1 ) -> ( ( normh ` ( ( projh ` B ) ` u ) ) ^ 2 ) < ( 1 ^ 2 ) )
31 6 30 eqbrtrid 
 |-  ( ( u e. ( A \ B ) /\ ( normh ` u ) = 1 ) -> ( S ` B ) < ( 1 ^ 2 ) )
32 sq1 
 |-  ( 1 ^ 2 ) = 1
33 31 32 breqtrdi 
 |-  ( ( u e. ( A \ B ) /\ ( normh ` u ) = 1 ) -> ( S ` B ) < 1 )
34 2 33 sylbi 
 |-  ( ph -> ( S ` B ) < 1 )