Metamath Proof Explorer

Theorem pjssdif2i

Description: The projection subspace of the difference between two projectors. Part 2 of Theorem 29.3 of Halmos p. 48 (shortened with pjssposi ). (Contributed by NM, 2-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypotheses pjco.1 
|- G e. CH
pjco.2 
|- H e. CH
Assertion pjssdif2i 
|- ( G C_ H <-> ( ( projh ` H ) -op ( projh ` G ) ) = ( projh ` ( H i^i ( _|_ ` G ) ) ) )

Proof

Step Hyp Ref Expression
1 pjco.1 
 |-  G e. CH
2 pjco.2 
 |-  H e. CH
3 2 pjfi 
 |-  ( projh ` H ) : ~H --> ~H
4 1 pjfi 
 |-  ( projh ` G ) : ~H --> ~H
5 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 ) ) )
6 3 4 5 mp3an12 
 |-  ( x e. ~H -> ( ( ( projh ` H ) -op ( projh ` G ) ) ` x ) = ( ( ( projh ` H ) ` x ) -h ( ( projh ` G ) ` x ) ) )
7 6 adantl 
 |-  ( ( G C_ H /\ x e. ~H ) -> ( ( ( projh ` H ) -op ( projh ` G ) ) ` x ) = ( ( ( projh ` H ) ` x ) -h ( ( projh ` G ) ` x ) ) )
8 2 1 pjssmi 
 |-  ( x e. ~H -> ( G C_ H -> ( ( ( projh ` H ) ` x ) -h ( ( projh ` G ) ` x ) ) = ( ( projh ` ( H i^i ( _|_ ` G ) ) ) ` x ) ) )
9 8 impcom 
 |-  ( ( G C_ H /\ x e. ~H ) -> ( ( ( projh ` H ) ` x ) -h ( ( projh ` G ) ` x ) ) = ( ( projh ` ( H i^i ( _|_ ` G ) ) ) ` x ) )
10 7 9 eqtrd 
 |-  ( ( G C_ H /\ x e. ~H ) -> ( ( ( projh ` H ) -op ( projh ` G ) ) ` x ) = ( ( projh ` ( H i^i ( _|_ ` G ) ) ) ` x ) )
11 10 ralrimiva 
 |-  ( G C_ H -> A. x e. ~H ( ( ( projh ` H ) -op ( projh ` G ) ) ` x ) = ( ( projh ` ( H i^i ( _|_ ` G ) ) ) ` x ) )
12 3 4 hosubfni 
 |-  ( ( projh ` H ) -op ( projh ` G ) ) Fn ~H
13 1 choccli 
 |-  ( _|_ ` G ) e. CH
14 2 13 chincli 
 |-  ( H i^i ( _|_ ` G ) ) e. CH
15 14 pjfni 
 |-  ( projh ` ( H i^i ( _|_ ` G ) ) ) Fn ~H
16 eqfnfv 
 |-  ( ( ( ( projh ` H ) -op ( projh ` G ) ) Fn ~H /\ ( projh ` ( H i^i ( _|_ ` G ) ) ) Fn ~H ) -> ( ( ( projh ` H ) -op ( projh ` G ) ) = ( projh ` ( H i^i ( _|_ ` G ) ) ) <-> A. x e. ~H ( ( ( projh ` H ) -op ( projh ` G ) ) ` x ) = ( ( projh ` ( H i^i ( _|_ ` G ) ) ) ` x ) ) )
17 12 15 16 mp2an 
 |-  ( ( ( projh ` H ) -op ( projh ` G ) ) = ( projh ` ( H i^i ( _|_ ` G ) ) ) <-> A. x e. ~H ( ( ( projh ` H ) -op ( projh ` G ) ) ` x ) = ( ( projh ` ( H i^i ( _|_ ` G ) ) ) ` x ) )
18 11 17 sylibr 
 |-  ( G C_ H -> ( ( projh ` H ) -op ( projh ` G ) ) = ( projh ` ( H i^i ( _|_ ` G ) ) ) )
19 14 pjige0i 
 |-  ( x e. ~H -> 0 <_ ( ( ( projh ` ( H i^i ( _|_ ` G ) ) ) ` x ) .ih x ) )
20 19 adantl 
 |-  ( ( ( ( projh ` H ) -op ( projh ` G ) ) = ( projh ` ( H i^i ( _|_ ` G ) ) ) /\ x e. ~H ) -> 0 <_ ( ( ( projh ` ( H i^i ( _|_ ` G ) ) ) ` x ) .ih x ) )
21 fveq1 
 |-  ( ( ( projh ` H ) -op ( projh ` G ) ) = ( projh ` ( H i^i ( _|_ ` G ) ) ) -> ( ( ( projh ` H ) -op ( projh ` G ) ) ` x ) = ( ( projh ` ( H i^i ( _|_ ` G ) ) ) ` x ) )
22 21 oveq1d 
 |-  ( ( ( projh ` H ) -op ( projh ` G ) ) = ( projh ` ( H i^i ( _|_ ` G ) ) ) -> ( ( ( ( projh ` H ) -op ( projh ` G ) ) ` x ) .ih x ) = ( ( ( projh ` ( H i^i ( _|_ ` G ) ) ) ` x ) .ih x ) )
23 22 adantr 
 |-  ( ( ( ( projh ` H ) -op ( projh ` G ) ) = ( projh ` ( H i^i ( _|_ ` G ) ) ) /\ x e. ~H ) -> ( ( ( ( projh ` H ) -op ( projh ` G ) ) ` x ) .ih x ) = ( ( ( projh ` ( H i^i ( _|_ ` G ) ) ) ` x ) .ih x ) )
24 20 23 breqtrrd 
 |-  ( ( ( ( projh ` H ) -op ( projh ` G ) ) = ( projh ` ( H i^i ( _|_ ` G ) ) ) /\ x e. ~H ) -> 0 <_ ( ( ( ( projh ` H ) -op ( projh ` G ) ) ` x ) .ih x ) )
25 24 ralrimiva 
 |-  ( ( ( projh ` H ) -op ( projh ` G ) ) = ( projh ` ( H i^i ( _|_ ` G ) ) ) -> A. x e. ~H 0 <_ ( ( ( ( projh ` H ) -op ( projh ` G ) ) ` x ) .ih x ) )
26 1 2 pjssposi 
 |-  ( A. x e. ~H 0 <_ ( ( ( ( projh ` H ) -op ( projh ` G ) ) ` x ) .ih x ) <-> G C_ H )
27 25 26 sylib 
 |-  ( ( ( projh ` H ) -op ( projh ` G ) ) = ( projh ` ( H i^i ( _|_ ` G ) ) ) -> G C_ H )
28 18 27 impbii 
 |-  ( G C_ H <-> ( ( projh ` H ) -op ( projh ` G ) ) = ( projh ` ( H i^i ( _|_ ` G ) ) ) )