Metamath Proof Explorer

Theorem pjnmopi

Description: The operator norm of a projector on a nonzero closed subspace is one. Part of Theorem 26.1 of Halmos p. 43. (Contributed by NM, 9-Apr-2006) (New usage is discouraged.)

Ref Expression
Hypothesis pjhmop.1 
|- H e. CH
Assertion pjnmopi 
|- ( H =/= 0H -> ( normop ` ( projh ` H ) ) = 1 )

Proof

Step Hyp Ref Expression
1 pjhmop.1 
 |-  H e. CH
2 1 pjfi 
 |-  ( projh ` H ) : ~H --> ~H
3 nmopval 
 |-  ( ( projh ` H ) : ~H --> ~H -> ( normop ` ( projh ` H ) ) = sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( ( projh ` H ) ` y ) ) ) } , RR* , < ) )
4 2 3 ax-mp 
 |-  ( normop ` ( projh ` H ) ) = sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( ( projh ` H ) ` y ) ) ) } , RR* , < )
5 vex 
 |-  z e. _V
6 eqeq1 
 |-  ( x = z -> ( x = ( normh ` ( ( projh ` H ) ` y ) ) <-> z = ( normh ` ( ( projh ` H ) ` y ) ) ) )
7 6 anbi2d 
 |-  ( x = z -> ( ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( ( projh ` H ) ` y ) ) ) <-> ( ( normh ` y ) <_ 1 /\ z = ( normh ` ( ( projh ` H ) ` y ) ) ) ) )
8 7 rexbidv 
 |-  ( x = z -> ( E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( ( projh ` H ) ` y ) ) ) <-> E. y e. ~H ( ( normh ` y ) <_ 1 /\ z = ( normh ` ( ( projh ` H ) ` y ) ) ) ) )
9 5 8 elab 
 |-  ( z e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( ( projh ` H ) ` y ) ) ) } <-> E. y e. ~H ( ( normh ` y ) <_ 1 /\ z = ( normh ` ( ( projh ` H ) ` y ) ) ) )
10 pjnorm 
 |-  ( ( H e. CH /\ y e. ~H ) -> ( normh ` ( ( projh ` H ) ` y ) ) <_ ( normh ` y ) )
11 1 10 mpan 
 |-  ( y e. ~H -> ( normh ` ( ( projh ` H ) ` y ) ) <_ ( normh ` y ) )
12 1 pjhcli 
 |-  ( y e. ~H -> ( ( projh ` H ) ` y ) e. ~H )
13 normcl 
 |-  ( ( ( projh ` H ) ` y ) e. ~H -> ( normh ` ( ( projh ` H ) ` y ) ) e. RR )
14 12 13 syl 
 |-  ( y e. ~H -> ( normh ` ( ( projh ` H ) ` y ) ) e. RR )
15 normcl 
 |-  ( y e. ~H -> ( normh ` y ) e. RR )
16 1re 
 |-  1 e. RR
17 letr 
 |-  ( ( ( normh ` ( ( projh ` H ) ` y ) ) e. RR /\ ( normh ` y ) e. RR /\ 1 e. RR ) -> ( ( ( normh ` ( ( projh ` H ) ` y ) ) <_ ( normh ` y ) /\ ( normh ` y ) <_ 1 ) -> ( normh ` ( ( projh ` H ) ` y ) ) <_ 1 ) )
18 16 17 mp3an3 
 |-  ( ( ( normh ` ( ( projh ` H ) ` y ) ) e. RR /\ ( normh ` y ) e. RR ) -> ( ( ( normh ` ( ( projh ` H ) ` y ) ) <_ ( normh ` y ) /\ ( normh ` y ) <_ 1 ) -> ( normh ` ( ( projh ` H ) ` y ) ) <_ 1 ) )
19 14 15 18 syl2anc 
 |-  ( y e. ~H -> ( ( ( normh ` ( ( projh ` H ) ` y ) ) <_ ( normh ` y ) /\ ( normh ` y ) <_ 1 ) -> ( normh ` ( ( projh ` H ) ` y ) ) <_ 1 ) )
20 11 19 mpand 
 |-  ( y e. ~H -> ( ( normh ` y ) <_ 1 -> ( normh ` ( ( projh ` H ) ` y ) ) <_ 1 ) )
21 20 imp 
 |-  ( ( y e. ~H /\ ( normh ` y ) <_ 1 ) -> ( normh ` ( ( projh ` H ) ` y ) ) <_ 1 )
22 breq1 
 |-  ( z = ( normh ` ( ( projh ` H ) ` y ) ) -> ( z <_ 1 <-> ( normh ` ( ( projh ` H ) ` y ) ) <_ 1 ) )
23 22 biimparc 
 |-  ( ( ( normh ` ( ( projh ` H ) ` y ) ) <_ 1 /\ z = ( normh ` ( ( projh ` H ) ` y ) ) ) -> z <_ 1 )
24 21 23 sylan 
 |-  ( ( ( y e. ~H /\ ( normh ` y ) <_ 1 ) /\ z = ( normh ` ( ( projh ` H ) ` y ) ) ) -> z <_ 1 )
25 24 expl 
 |-  ( y e. ~H -> ( ( ( normh ` y ) <_ 1 /\ z = ( normh ` ( ( projh ` H ) ` y ) ) ) -> z <_ 1 ) )
26 25 rexlimiv 
 |-  ( E. y e. ~H ( ( normh ` y ) <_ 1 /\ z = ( normh ` ( ( projh ` H ) ` y ) ) ) -> z <_ 1 )
27 9 26 sylbi 
 |-  ( z e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( ( projh ` H ) ` y ) ) ) } -> z <_ 1 )
28 27 rgen 
 |-  A. z e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( ( projh ` H ) ` y ) ) ) } z <_ 1
29 1 cheli 
 |-  ( y e. H -> y e. ~H )
30 29 adantr 
 |-  ( ( y e. H /\ ( normh ` y ) = 1 ) -> y e. ~H )
31 29 15 syl 
 |-  ( y e. H -> ( normh ` y ) e. RR )
32 eqle 
 |-  ( ( ( normh ` y ) e. RR /\ ( normh ` y ) = 1 ) -> ( normh ` y ) <_ 1 )
33 31 32 sylan 
 |-  ( ( y e. H /\ ( normh ` y ) = 1 ) -> ( normh ` y ) <_ 1 )
34 pjid 
 |-  ( ( H e. CH /\ y e. H ) -> ( ( projh ` H ) ` y ) = y )
35 1 34 mpan 
 |-  ( y e. H -> ( ( projh ` H ) ` y ) = y )
36 35 fveq2d 
 |-  ( y e. H -> ( normh ` ( ( projh ` H ) ` y ) ) = ( normh ` y ) )
37 36 adantr 
 |-  ( ( y e. H /\ ( normh ` y ) = 1 ) -> ( normh ` ( ( projh ` H ) ` y ) ) = ( normh ` y ) )
38 simpr 
 |-  ( ( y e. H /\ ( normh ` y ) = 1 ) -> ( normh ` y ) = 1 )
39 37 38 eqtr2d 
 |-  ( ( y e. H /\ ( normh ` y ) = 1 ) -> 1 = ( normh ` ( ( projh ` H ) ` y ) ) )
40 30 33 39 jca32 
 |-  ( ( y e. H /\ ( normh ` y ) = 1 ) -> ( y e. ~H /\ ( ( normh ` y ) <_ 1 /\ 1 = ( normh ` ( ( projh ` H ) ` y ) ) ) ) )
41 40 reximi2 
 |-  ( E. y e. H ( normh ` y ) = 1 -> E. y e. ~H ( ( normh ` y ) <_ 1 /\ 1 = ( normh ` ( ( projh ` H ) ` y ) ) ) )
42 1 chne0i 
 |-  ( H =/= 0H <-> E. y e. H y =/= 0h )
43 1 chshii 
 |-  H e. SH
44 43 norm1exi 
 |-  ( E. y e. H y =/= 0h <-> E. y e. H ( normh ` y ) = 1 )
45 42 44 bitri 
 |-  ( H =/= 0H <-> E. y e. H ( normh ` y ) = 1 )
46 1ex 
 |-  1 e. _V
47 eqeq1 
 |-  ( x = 1 -> ( x = ( normh ` ( ( projh ` H ) ` y ) ) <-> 1 = ( normh ` ( ( projh ` H ) ` y ) ) ) )
48 47 anbi2d 
 |-  ( x = 1 -> ( ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( ( projh ` H ) ` y ) ) ) <-> ( ( normh ` y ) <_ 1 /\ 1 = ( normh ` ( ( projh ` H ) ` y ) ) ) ) )
49 48 rexbidv 
 |-  ( x = 1 -> ( E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( ( projh ` H ) ` y ) ) ) <-> E. y e. ~H ( ( normh ` y ) <_ 1 /\ 1 = ( normh ` ( ( projh ` H ) ` y ) ) ) ) )
50 46 49 elab 
 |-  ( 1 e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( ( projh ` H ) ` y ) ) ) } <-> E. y e. ~H ( ( normh ` y ) <_ 1 /\ 1 = ( normh ` ( ( projh ` H ) ` y ) ) ) )
51 41 45 50 3imtr4i 
 |-  ( H =/= 0H -> 1 e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( ( projh ` H ) ` y ) ) ) } )
52 breq2 
 |-  ( w = 1 -> ( z < w <-> z < 1 ) )
53 52 rspcev 
 |-  ( ( 1 e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( ( projh ` H ) ` y ) ) ) } /\ z < 1 ) -> E. w e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( ( projh ` H ) ` y ) ) ) } z < w )
54 51 53 sylan 
 |-  ( ( H =/= 0H /\ z < 1 ) -> E. w e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( ( projh ` H ) ` y ) ) ) } z < w )
55 54 ex 
 |-  ( H =/= 0H -> ( z < 1 -> E. w e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( ( projh ` H ) ` y ) ) ) } z < w ) )
56 55 ralrimivw 
 |-  ( H =/= 0H -> A. z e. RR ( z < 1 -> E. w e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( ( projh ` H ) ` y ) ) ) } z < w ) )
57 nmopsetretHIL 
 |-  ( ( projh ` H ) : ~H --> ~H -> { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( ( projh ` H ) ` y ) ) ) } C_ RR )
58 2 57 ax-mp 
 |-  { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( ( projh ` H ) ` y ) ) ) } C_ RR
59 ressxr 
 |-  RR C_ RR*
60 58 59 sstri 
 |-  { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( ( projh ` H ) ` y ) ) ) } C_ RR*
61 1xr 
 |-  1 e. RR*
62 supxr2 
 |-  ( ( ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( ( projh ` H ) ` y ) ) ) } C_ RR* /\ 1 e. RR* ) /\ ( A. z e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( ( projh ` H ) ` y ) ) ) } z <_ 1 /\ A. z e. RR ( z < 1 -> E. w e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( ( projh ` H ) ` y ) ) ) } z < w ) ) ) -> sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( ( projh ` H ) ` y ) ) ) } , RR* , < ) = 1 )
63 60 61 62 mpanl12 
 |-  ( ( A. z e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( ( projh ` H ) ` y ) ) ) } z <_ 1 /\ A. z e. RR ( z < 1 -> E. w e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( ( projh ` H ) ` y ) ) ) } z < w ) ) -> sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( ( projh ` H ) ` y ) ) ) } , RR* , < ) = 1 )
64 28 56 63 sylancr 
 |-  ( H =/= 0H -> sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( ( projh ` H ) ` y ) ) ) } , RR* , < ) = 1 )
65 4 64 eqtrid 
 |-  ( H =/= 0H -> ( normop ` ( projh ` H ) ) = 1 )