Metamath Proof Explorer

Theorem pjssposi

Description: Projector ordering can be expressed by the subset relationship between their projection subspaces. (i)<->(iii) of Theorem 29.2 of Halmos p. 48. (Contributed by NM, 2-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypotheses pjco.1 
|- G e. CH
pjco.2 
|- H e. CH
Assertion pjssposi 
|- ( A. x e. ~H 0 <_ ( ( ( ( projh ` H ) -op ( projh ` G ) ) ` x ) .ih x ) <-> G C_ H )

Proof

Step Hyp Ref Expression
1 pjco.1 
 |-  G e. CH
2 pjco.2 
 |-  H e. CH
3 2 pjhcli 
 |-  ( x e. ~H -> ( ( projh ` H ) ` x ) e. ~H )
4 normcl 
 |-  ( ( ( projh ` H ) ` x ) e. ~H -> ( normh ` ( ( projh ` H ) ` x ) ) e. RR )
5 3 4 syl 
 |-  ( x e. ~H -> ( normh ` ( ( projh ` H ) ` x ) ) e. RR )
6 5 resqcld 
 |-  ( x e. ~H -> ( ( normh ` ( ( projh ` H ) ` x ) ) ^ 2 ) e. RR )
7 1 pjhcli 
 |-  ( x e. ~H -> ( ( projh ` G ) ` x ) e. ~H )
8 normcl 
 |-  ( ( ( projh ` G ) ` x ) e. ~H -> ( normh ` ( ( projh ` G ) ` x ) ) e. RR )
9 7 8 syl 
 |-  ( x e. ~H -> ( normh ` ( ( projh ` G ) ` x ) ) e. RR )
10 9 resqcld 
 |-  ( x e. ~H -> ( ( normh ` ( ( projh ` G ) ` x ) ) ^ 2 ) e. RR )
11 6 10 subge0d 
 |-  ( x e. ~H -> ( 0 <_ ( ( ( normh ` ( ( projh ` H ) ` x ) ) ^ 2 ) - ( ( normh ` ( ( projh ` G ) ` x ) ) ^ 2 ) ) <-> ( ( normh ` ( ( projh ` G ) ` x ) ) ^ 2 ) <_ ( ( normh ` ( ( projh ` H ) ` x ) ) ^ 2 ) ) )
12 2 pjfi 
 |-  ( projh ` H ) : ~H --> ~H
13 1 pjfi 
 |-  ( projh ` G ) : ~H --> ~H
14 hodval 
 |-  ( ( ( projh ` H ) : ~H --> ~H /\ ( projh ` G ) : ~H --> ~H /\ x e. ~H ) -> ( ( ( projh ` H ) -op ( projh ` G ) ) ` x ) = ( ( ( projh ` H ) ` x ) -h ( ( projh ` G ) ` x ) ) )
15 12 13 14 mp3an12 
 |-  ( x e. ~H -> ( ( ( projh ` H ) -op ( projh ` G ) ) ` x ) = ( ( ( projh ` H ) ` x ) -h ( ( projh ` G ) ` x ) ) )
16 15 oveq1d 
 |-  ( x e. ~H -> ( ( ( ( projh ` H ) -op ( projh ` G ) ) ` x ) .ih x ) = ( ( ( ( projh ` H ) ` x ) -h ( ( projh ` G ) ` x ) ) .ih x ) )
17 id 
 |-  ( x e. ~H -> x e. ~H )
18 his2sub 
 |-  ( ( ( ( projh ` H ) ` x ) e. ~H /\ ( ( projh ` G ) ` x ) e. ~H /\ x e. ~H ) -> ( ( ( ( projh ` H ) ` x ) -h ( ( projh ` G ) ` x ) ) .ih x ) = ( ( ( ( projh ` H ) ` x ) .ih x ) - ( ( ( projh ` G ) ` x ) .ih x ) ) )
19 3 7 17 18 syl3anc 
 |-  ( x e. ~H -> ( ( ( ( projh ` H ) ` x ) -h ( ( projh ` G ) ` x ) ) .ih x ) = ( ( ( ( projh ` H ) ` x ) .ih x ) - ( ( ( projh ` G ) ` x ) .ih x ) ) )
20 2 pjinormi 
 |-  ( x e. ~H -> ( ( ( projh ` H ) ` x ) .ih x ) = ( ( normh ` ( ( projh ` H ) ` x ) ) ^ 2 ) )
21 1 pjinormi 
 |-  ( x e. ~H -> ( ( ( projh ` G ) ` x ) .ih x ) = ( ( normh ` ( ( projh ` G ) ` x ) ) ^ 2 ) )
22 20 21 oveq12d 
 |-  ( x e. ~H -> ( ( ( ( projh ` H ) ` x ) .ih x ) - ( ( ( projh ` G ) ` x ) .ih x ) ) = ( ( ( normh ` ( ( projh ` H ) ` x ) ) ^ 2 ) - ( ( normh ` ( ( projh ` G ) ` x ) ) ^ 2 ) ) )
23 16 19 22 3eqtrd 
 |-  ( x e. ~H -> ( ( ( ( projh ` H ) -op ( projh ` G ) ) ` x ) .ih x ) = ( ( ( normh ` ( ( projh ` H ) ` x ) ) ^ 2 ) - ( ( normh ` ( ( projh ` G ) ` x ) ) ^ 2 ) ) )
24 23 breq2d 
 |-  ( x e. ~H -> ( 0 <_ ( ( ( ( projh ` H ) -op ( projh ` G ) ) ` x ) .ih x ) <-> 0 <_ ( ( ( normh ` ( ( projh ` H ) ` x ) ) ^ 2 ) - ( ( normh ` ( ( projh ` G ) ` x ) ) ^ 2 ) ) ) )
25 normge0 
 |-  ( ( ( projh ` G ) ` x ) e. ~H -> 0 <_ ( normh ` ( ( projh ` G ) ` x ) ) )
26 7 25 syl 
 |-  ( x e. ~H -> 0 <_ ( normh ` ( ( projh ` G ) ` x ) ) )
27 normge0 
 |-  ( ( ( projh ` H ) ` x ) e. ~H -> 0 <_ ( normh ` ( ( projh ` H ) ` x ) ) )
28 3 27 syl 
 |-  ( x e. ~H -> 0 <_ ( normh ` ( ( projh ` H ) ` x ) ) )
29 9 5 26 28 le2sqd 
 |-  ( x e. ~H -> ( ( normh ` ( ( projh ` G ) ` x ) ) <_ ( normh ` ( ( projh ` H ) ` x ) ) <-> ( ( normh ` ( ( projh ` G ) ` x ) ) ^ 2 ) <_ ( ( normh ` ( ( projh ` H ) ` x ) ) ^ 2 ) ) )
30 11 24 29 3bitr4d 
 |-  ( x e. ~H -> ( 0 <_ ( ( ( ( projh ` H ) -op ( projh ` G ) ) ` x ) .ih x ) <-> ( normh ` ( ( projh ` G ) ` x ) ) <_ ( normh ` ( ( projh ` H ) ` x ) ) ) )
31 30 ralbiia 
 |-  ( A. x e. ~H 0 <_ ( ( ( ( projh ` H ) -op ( projh ` G ) ) ` x ) .ih x ) <-> A. x e. ~H ( normh ` ( ( projh ` G ) ` x ) ) <_ ( normh ` ( ( projh ` H ) ` x ) ) )
32 1 2 pjnormssi 
 |-  ( G C_ H <-> A. x e. ~H ( normh ` ( ( projh ` G ) ` x ) ) <_ ( normh ` ( ( projh ` H ) ` x ) ) )
33 31 32 bitr4i 
 |-  ( A. x e. ~H 0 <_ ( ( ( ( projh ` H ) -op ( projh ` G ) ) ` x ) .ih x ) <-> G C_ H )