Metamath Proof Explorer

Theorem strlem3a

Description: Lemma for strong state theorem: the function S , that maps a closed subspace to the square of the norm of its projection onto a unit vector, is a state. (Contributed by NM, 28-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypothesis strlem3a.1 
|- S = ( x e. CH |-> ( ( normh ` ( ( projh ` x ) ` u ) ) ^ 2 ) )
Assertion strlem3a 
|- ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> S e. States )

Proof

Step Hyp Ref Expression
1 strlem3a.1 
 |-  S = ( x e. CH |-> ( ( normh ` ( ( projh ` x ) ` u ) ) ^ 2 ) )
2 id 
 |-  ( x e. CH -> x e. CH )
3 simpl 
 |-  ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> u e. ~H )
4 pjhcl 
 |-  ( ( x e. CH /\ u e. ~H ) -> ( ( projh ` x ) ` u ) e. ~H )
5 2 3 4 syl2anr 
 |-  ( ( ( u e. ~H /\ ( normh ` u ) = 1 ) /\ x e. CH ) -> ( ( projh ` x ) ` u ) e. ~H )
6 normcl 
 |-  ( ( ( projh ` x ) ` u ) e. ~H -> ( normh ` ( ( projh ` x ) ` u ) ) e. RR )
7 5 6 syl 
 |-  ( ( ( u e. ~H /\ ( normh ` u ) = 1 ) /\ x e. CH ) -> ( normh ` ( ( projh ` x ) ` u ) ) e. RR )
8 7 resqcld 
 |-  ( ( ( u e. ~H /\ ( normh ` u ) = 1 ) /\ x e. CH ) -> ( ( normh ` ( ( projh ` x ) ` u ) ) ^ 2 ) e. RR )
9 7 sqge0d 
 |-  ( ( ( u e. ~H /\ ( normh ` u ) = 1 ) /\ x e. CH ) -> 0 <_ ( ( normh ` ( ( projh ` x ) ` u ) ) ^ 2 ) )
10 normge0 
 |-  ( ( ( projh ` x ) ` u ) e. ~H -> 0 <_ ( normh ` ( ( projh ` x ) ` u ) ) )
11 5 10 syl 
 |-  ( ( ( u e. ~H /\ ( normh ` u ) = 1 ) /\ x e. CH ) -> 0 <_ ( normh ` ( ( projh ` x ) ` u ) ) )
12 pjnorm 
 |-  ( ( x e. CH /\ u e. ~H ) -> ( normh ` ( ( projh ` x ) ` u ) ) <_ ( normh ` u ) )
13 2 3 12 syl2anr 
 |-  ( ( ( u e. ~H /\ ( normh ` u ) = 1 ) /\ x e. CH ) -> ( normh ` ( ( projh ` x ) ` u ) ) <_ ( normh ` u ) )
14 simplr 
 |-  ( ( ( u e. ~H /\ ( normh ` u ) = 1 ) /\ x e. CH ) -> ( normh ` u ) = 1 )
15 13 14 breqtrd 
 |-  ( ( ( u e. ~H /\ ( normh ` u ) = 1 ) /\ x e. CH ) -> ( normh ` ( ( projh ` x ) ` u ) ) <_ 1 )
16 2nn0 
 |-  2 e. NN0
17 exple1 
 |-  ( ( ( ( normh ` ( ( projh ` x ) ` u ) ) e. RR /\ 0 <_ ( normh ` ( ( projh ` x ) ` u ) ) /\ ( normh ` ( ( projh ` x ) ` u ) ) <_ 1 ) /\ 2 e. NN0 ) -> ( ( normh ` ( ( projh ` x ) ` u ) ) ^ 2 ) <_ 1 )
18 16 17 mpan2 
 |-  ( ( ( normh ` ( ( projh ` x ) ` u ) ) e. RR /\ 0 <_ ( normh ` ( ( projh ` x ) ` u ) ) /\ ( normh ` ( ( projh ` x ) ` u ) ) <_ 1 ) -> ( ( normh ` ( ( projh ` x ) ` u ) ) ^ 2 ) <_ 1 )
19 7 11 15 18 syl3anc 
 |-  ( ( ( u e. ~H /\ ( normh ` u ) = 1 ) /\ x e. CH ) -> ( ( normh ` ( ( projh ` x ) ` u ) ) ^ 2 ) <_ 1 )
20 elicc01 
 |-  ( ( ( normh ` ( ( projh ` x ) ` u ) ) ^ 2 ) e. ( 0 [,] 1 ) <-> ( ( ( normh ` ( ( projh ` x ) ` u ) ) ^ 2 ) e. RR /\ 0 <_ ( ( normh ` ( ( projh ` x ) ` u ) ) ^ 2 ) /\ ( ( normh ` ( ( projh ` x ) ` u ) ) ^ 2 ) <_ 1 ) )
21 8 9 19 20 syl3anbrc 
 |-  ( ( ( u e. ~H /\ ( normh ` u ) = 1 ) /\ x e. CH ) -> ( ( normh ` ( ( projh ` x ) ` u ) ) ^ 2 ) e. ( 0 [,] 1 ) )
22 21 1 fmptd 
 |-  ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> S : CH --> ( 0 [,] 1 ) )
23 helch 
 |-  ~H e. CH
24 1 strlem2 
 |-  ( ~H e. CH -> ( S ` ~H ) = ( ( normh ` ( ( projh ` ~H ) ` u ) ) ^ 2 ) )
25 23 24 ax-mp 
 |-  ( S ` ~H ) = ( ( normh ` ( ( projh ` ~H ) ` u ) ) ^ 2 )
26 pjch1 
 |-  ( u e. ~H -> ( ( projh ` ~H ) ` u ) = u )
27 26 fveq2d 
 |-  ( u e. ~H -> ( normh ` ( ( projh ` ~H ) ` u ) ) = ( normh ` u ) )
28 27 oveq1d 
 |-  ( u e. ~H -> ( ( normh ` ( ( projh ` ~H ) ` u ) ) ^ 2 ) = ( ( normh ` u ) ^ 2 ) )
29 oveq1 
 |-  ( ( normh ` u ) = 1 -> ( ( normh ` u ) ^ 2 ) = ( 1 ^ 2 ) )
30 sq1 
 |-  ( 1 ^ 2 ) = 1
31 29 30 eqtrdi 
 |-  ( ( normh ` u ) = 1 -> ( ( normh ` u ) ^ 2 ) = 1 )
32 28 31 sylan9eq 
 |-  ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> ( ( normh ` ( ( projh ` ~H ) ` u ) ) ^ 2 ) = 1 )
33 25 32 eqtrid 
 |-  ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> ( S ` ~H ) = 1 )
34 pjcjt2 
 |-  ( ( z e. CH /\ w e. CH /\ u e. ~H ) -> ( z C_ ( _|_ ` w ) -> ( ( projh ` ( z vH w ) ) ` u ) = ( ( ( projh ` z ) ` u ) +h ( ( projh ` w ) ` u ) ) ) )
35 34 imp 
 |-  ( ( ( z e. CH /\ w e. CH /\ u e. ~H ) /\ z C_ ( _|_ ` w ) ) -> ( ( projh ` ( z vH w ) ) ` u ) = ( ( ( projh ` z ) ` u ) +h ( ( projh ` w ) ` u ) ) )
36 35 fveq2d 
 |-  ( ( ( z e. CH /\ w e. CH /\ u e. ~H ) /\ z C_ ( _|_ ` w ) ) -> ( normh ` ( ( projh ` ( z vH w ) ) ` u ) ) = ( normh ` ( ( ( projh ` z ) ` u ) +h ( ( projh ` w ) ` u ) ) ) )
37 36 oveq1d 
 |-  ( ( ( z e. CH /\ w e. CH /\ u e. ~H ) /\ z C_ ( _|_ ` w ) ) -> ( ( normh ` ( ( projh ` ( z vH w ) ) ` u ) ) ^ 2 ) = ( ( normh ` ( ( ( projh ` z ) ` u ) +h ( ( projh ` w ) ` u ) ) ) ^ 2 ) )
38 pjopyth 
 |-  ( ( z e. CH /\ w e. CH /\ u e. ~H ) -> ( z C_ ( _|_ ` w ) -> ( ( normh ` ( ( ( projh ` z ) ` u ) +h ( ( projh ` w ) ` u ) ) ) ^ 2 ) = ( ( ( normh ` ( ( projh ` z ) ` u ) ) ^ 2 ) + ( ( normh ` ( ( projh ` w ) ` u ) ) ^ 2 ) ) ) )
39 38 imp 
 |-  ( ( ( z e. CH /\ w e. CH /\ u e. ~H ) /\ z C_ ( _|_ ` w ) ) -> ( ( normh ` ( ( ( projh ` z ) ` u ) +h ( ( projh ` w ) ` u ) ) ) ^ 2 ) = ( ( ( normh ` ( ( projh ` z ) ` u ) ) ^ 2 ) + ( ( normh ` ( ( projh ` w ) ` u ) ) ^ 2 ) ) )
40 37 39 eqtrd 
 |-  ( ( ( z e. CH /\ w e. CH /\ u e. ~H ) /\ z C_ ( _|_ ` w ) ) -> ( ( normh ` ( ( projh ` ( z vH w ) ) ` u ) ) ^ 2 ) = ( ( ( normh ` ( ( projh ` z ) ` u ) ) ^ 2 ) + ( ( normh ` ( ( projh ` w ) ` u ) ) ^ 2 ) ) )
41 chjcl 
 |-  ( ( z e. CH /\ w e. CH ) -> ( z vH w ) e. CH )
42 41 3adant3 
 |-  ( ( z e. CH /\ w e. CH /\ u e. ~H ) -> ( z vH w ) e. CH )
43 42 adantr 
 |-  ( ( ( z e. CH /\ w e. CH /\ u e. ~H ) /\ z C_ ( _|_ ` w ) ) -> ( z vH w ) e. CH )
44 1 strlem2 
 |-  ( ( z vH w ) e. CH -> ( S ` ( z vH w ) ) = ( ( normh ` ( ( projh ` ( z vH w ) ) ` u ) ) ^ 2 ) )
45 43 44 syl 
 |-  ( ( ( z e. CH /\ w e. CH /\ u e. ~H ) /\ z C_ ( _|_ ` w ) ) -> ( S ` ( z vH w ) ) = ( ( normh ` ( ( projh ` ( z vH w ) ) ` u ) ) ^ 2 ) )
46 3simpa 
 |-  ( ( z e. CH /\ w e. CH /\ u e. ~H ) -> ( z e. CH /\ w e. CH ) )
47 46 adantr 
 |-  ( ( ( z e. CH /\ w e. CH /\ u e. ~H ) /\ z C_ ( _|_ ` w ) ) -> ( z e. CH /\ w e. CH ) )
48 1 strlem2 
 |-  ( z e. CH -> ( S ` z ) = ( ( normh ` ( ( projh ` z ) ` u ) ) ^ 2 ) )
49 1 strlem2 
 |-  ( w e. CH -> ( S ` w ) = ( ( normh ` ( ( projh ` w ) ` u ) ) ^ 2 ) )
50 48 49 oveqan12d 
 |-  ( ( z e. CH /\ w e. CH ) -> ( ( S ` z ) + ( S ` w ) ) = ( ( ( normh ` ( ( projh ` z ) ` u ) ) ^ 2 ) + ( ( normh ` ( ( projh ` w ) ` u ) ) ^ 2 ) ) )
51 47 50 syl 
 |-  ( ( ( z e. CH /\ w e. CH /\ u e. ~H ) /\ z C_ ( _|_ ` w ) ) -> ( ( S ` z ) + ( S ` w ) ) = ( ( ( normh ` ( ( projh ` z ) ` u ) ) ^ 2 ) + ( ( normh ` ( ( projh ` w ) ` u ) ) ^ 2 ) ) )
52 40 45 51 3eqtr4d 
 |-  ( ( ( z e. CH /\ w e. CH /\ u e. ~H ) /\ z C_ ( _|_ ` w ) ) -> ( S ` ( z vH w ) ) = ( ( S ` z ) + ( S ` w ) ) )
53 52 3exp1 
 |-  ( z e. CH -> ( w e. CH -> ( u e. ~H -> ( z C_ ( _|_ ` w ) -> ( S ` ( z vH w ) ) = ( ( S ` z ) + ( S ` w ) ) ) ) ) )
54 53 com3r 
 |-  ( u e. ~H -> ( z e. CH -> ( w e. CH -> ( z C_ ( _|_ ` w ) -> ( S ` ( z vH w ) ) = ( ( S ` z ) + ( S ` w ) ) ) ) ) )
55 54 adantr 
 |-  ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> ( z e. CH -> ( w e. CH -> ( z C_ ( _|_ ` w ) -> ( S ` ( z vH w ) ) = ( ( S ` z ) + ( S ` w ) ) ) ) ) )
56 55 ralrimdv 
 |-  ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> ( z e. CH -> A. w e. CH ( z C_ ( _|_ ` w ) -> ( S ` ( z vH w ) ) = ( ( S ` z ) + ( S ` w ) ) ) ) )
57 56 ralrimiv 
 |-  ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> A. z e. CH A. w e. CH ( z C_ ( _|_ ` w ) -> ( S ` ( z vH w ) ) = ( ( S ` z ) + ( S ` w ) ) ) )
58 isst 
 |-  ( S e. States <-> ( S : CH --> ( 0 [,] 1 ) /\ ( S ` ~H ) = 1 /\ A. z e. CH A. w e. CH ( z C_ ( _|_ ` w ) -> ( S ` ( z vH w ) ) = ( ( S ` z ) + ( S ` w ) ) ) ) )
59 22 33 57 58 syl3anbrc 
 |-  ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> S e. States )