Metamath Proof Explorer

Theorem pjorthcoi

Description: Composition of projections of orthogonal subspaces. Part (i)->(iia) of Theorem 27.4 of Halmos p. 45. (Contributed by NM, 6-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjco.1 
|- G e. CH
pjco.2 
|- H e. CH
Assertion pjorthcoi 
|- ( G C_ ( _|_ ` H ) -> ( ( projh ` G ) o. ( projh ` H ) ) = 0hop )

Proof

Step Hyp Ref Expression
1 pjco.1 
 |-  G e. CH
2 pjco.2 
 |-  H e. CH
3 2 pjcli 
 |-  ( x e. ~H -> ( ( projh ` H ) ` x ) e. H )
4 1 2 chsscon2i 
 |-  ( G C_ ( _|_ ` H ) <-> H C_ ( _|_ ` G ) )
5 ssel 
 |-  ( H C_ ( _|_ ` G ) -> ( ( ( projh ` H ) ` x ) e. H -> ( ( projh ` H ) ` x ) e. ( _|_ ` G ) ) )
6 4 5 sylbi 
 |-  ( G C_ ( _|_ ` H ) -> ( ( ( projh ` H ) ` x ) e. H -> ( ( projh ` H ) ` x ) e. ( _|_ ` G ) ) )
7 3 6 syl5com 
 |-  ( x e. ~H -> ( G C_ ( _|_ ` H ) -> ( ( projh ` H ) ` x ) e. ( _|_ ` G ) ) )
8 2 pjhcli 
 |-  ( x e. ~H -> ( ( projh ` H ) ` x ) e. ~H )
9 pjoc2 
 |-  ( ( G e. CH /\ ( ( projh ` H ) ` x ) e. ~H ) -> ( ( ( projh ` H ) ` x ) e. ( _|_ ` G ) <-> ( ( projh ` G ) ` ( ( projh ` H ) ` x ) ) = 0h ) )
10 1 8 9 sylancr 
 |-  ( x e. ~H -> ( ( ( projh ` H ) ` x ) e. ( _|_ ` G ) <-> ( ( projh ` G ) ` ( ( projh ` H ) ` x ) ) = 0h ) )
11 7 10 sylibd 
 |-  ( x e. ~H -> ( G C_ ( _|_ ` H ) -> ( ( projh ` G ) ` ( ( projh ` H ) ` x ) ) = 0h ) )
12 11 impcom 
 |-  ( ( G C_ ( _|_ ` H ) /\ x e. ~H ) -> ( ( projh ` G ) ` ( ( projh ` H ) ` x ) ) = 0h )
13 1 2 pjcoi 
 |-  ( x e. ~H -> ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) = ( ( projh ` G ) ` ( ( projh ` H ) ` x ) ) )
14 13 adantl 
 |-  ( ( G C_ ( _|_ ` H ) /\ x e. ~H ) -> ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) = ( ( projh ` G ) ` ( ( projh ` H ) ` x ) ) )
15 ho0val 
 |-  ( x e. ~H -> ( 0hop ` x ) = 0h )
16 15 adantl 
 |-  ( ( G C_ ( _|_ ` H ) /\ x e. ~H ) -> ( 0hop ` x ) = 0h )
17 12 14 16 3eqtr4d 
 |-  ( ( G C_ ( _|_ ` H ) /\ x e. ~H ) -> ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) = ( 0hop ` x ) )
18 17 ralrimiva 
 |-  ( G C_ ( _|_ ` H ) -> A. x e. ~H ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) = ( 0hop ` x ) )
19 1 pjfi 
 |-  ( projh ` G ) : ~H --> ~H
20 2 pjfi 
 |-  ( projh ` H ) : ~H --> ~H
21 19 20 hocofi 
 |-  ( ( projh ` G ) o. ( projh ` H ) ) : ~H --> ~H
22 ho0f 
 |-  0hop : ~H --> ~H
23 21 22 hoeqi 
 |-  ( A. x e. ~H ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) = ( 0hop ` x ) <-> ( ( projh ` G ) o. ( projh ` H ) ) = 0hop )
24 18 23 sylib 
 |-  ( G C_ ( _|_ ` H ) -> ( ( projh ` G ) o. ( projh ` H ) ) = 0hop )