Metamath Proof Explorer

Theorem pjssdif1i

Description: A necessary and sufficient condition for the difference between two projectors to be a projector. Part 1 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 pjssdif1i 
|- ( G C_ H <-> ( ( projh ` H ) -op ( projh ` G ) ) e. ran projh )

Proof

Step Hyp Ref Expression
1 pjco.1 
 |-  G e. CH
2 pjco.2 
 |-  H e. CH
3 1 2 pjssdif2i 
 |-  ( G C_ H <-> ( ( projh ` H ) -op ( projh ` G ) ) = ( projh ` ( H i^i ( _|_ ` G ) ) ) )
4 pjmfn 
 |-  projh Fn CH
5 1 choccli 
 |-  ( _|_ ` G ) e. CH
6 2 5 chincli 
 |-  ( H i^i ( _|_ ` G ) ) e. CH
7 fnfvelrn 
 |-  ( ( projh Fn CH /\ ( H i^i ( _|_ ` G ) ) e. CH ) -> ( projh ` ( H i^i ( _|_ ` G ) ) ) e. ran projh )
8 4 6 7 mp2an 
 |-  ( projh ` ( H i^i ( _|_ ` G ) ) ) e. ran projh
9 eleq1 
 |-  ( ( ( projh ` H ) -op ( projh ` G ) ) = ( projh ` ( H i^i ( _|_ ` G ) ) ) -> ( ( ( projh ` H ) -op ( projh ` G ) ) e. ran projh <-> ( projh ` ( H i^i ( _|_ ` G ) ) ) e. ran projh ) )
10 8 9 mpbiri 
 |-  ( ( ( projh ` H ) -op ( projh ` G ) ) = ( projh ` ( H i^i ( _|_ ` G ) ) ) -> ( ( projh ` H ) -op ( projh ` G ) ) e. ran projh )
11 fvelrnb 
 |-  ( projh Fn CH -> ( ( ( projh ` H ) -op ( projh ` G ) ) e. ran projh <-> E. x e. CH ( projh ` x ) = ( ( projh ` H ) -op ( projh ` G ) ) ) )
12 4 11 ax-mp 
 |-  ( ( ( projh ` H ) -op ( projh ` G ) ) e. ran projh <-> E. x e. CH ( projh ` x ) = ( ( projh ` H ) -op ( projh ` G ) ) )
13 pjige0 
 |-  ( ( x e. CH /\ y e. ~H ) -> 0 <_ ( ( ( projh ` x ) ` y ) .ih y ) )
14 13 adantlr 
 |-  ( ( ( x e. CH /\ ( projh ` x ) = ( ( projh ` H ) -op ( projh ` G ) ) ) /\ y e. ~H ) -> 0 <_ ( ( ( projh ` x ) ` y ) .ih y ) )
15 fveq1 
 |-  ( ( projh ` x ) = ( ( projh ` H ) -op ( projh ` G ) ) -> ( ( projh ` x ) ` y ) = ( ( ( projh ` H ) -op ( projh ` G ) ) ` y ) )
16 15 oveq1d 
 |-  ( ( projh ` x ) = ( ( projh ` H ) -op ( projh ` G ) ) -> ( ( ( projh ` x ) ` y ) .ih y ) = ( ( ( ( projh ` H ) -op ( projh ` G ) ) ` y ) .ih y ) )
17 16 breq2d 
 |-  ( ( projh ` x ) = ( ( projh ` H ) -op ( projh ` G ) ) -> ( 0 <_ ( ( ( projh ` x ) ` y ) .ih y ) <-> 0 <_ ( ( ( ( projh ` H ) -op ( projh ` G ) ) ` y ) .ih y ) ) )
18 17 ad2antlr 
 |-  ( ( ( x e. CH /\ ( projh ` x ) = ( ( projh ` H ) -op ( projh ` G ) ) ) /\ y e. ~H ) -> ( 0 <_ ( ( ( projh ` x ) ` y ) .ih y ) <-> 0 <_ ( ( ( ( projh ` H ) -op ( projh ` G ) ) ` y ) .ih y ) ) )
19 14 18 mpbid 
 |-  ( ( ( x e. CH /\ ( projh ` x ) = ( ( projh ` H ) -op ( projh ` G ) ) ) /\ y e. ~H ) -> 0 <_ ( ( ( ( projh ` H ) -op ( projh ` G ) ) ` y ) .ih y ) )
20 19 ralrimiva 
 |-  ( ( x e. CH /\ ( projh ` x ) = ( ( projh ` H ) -op ( projh ` G ) ) ) -> A. y e. ~H 0 <_ ( ( ( ( projh ` H ) -op ( projh ` G ) ) ` y ) .ih y ) )
21 20 rexlimiva 
 |-  ( E. x e. CH ( projh ` x ) = ( ( projh ` H ) -op ( projh ` G ) ) -> A. y e. ~H 0 <_ ( ( ( ( projh ` H ) -op ( projh ` G ) ) ` y ) .ih y ) )
22 12 21 sylbi 
 |-  ( ( ( projh ` H ) -op ( projh ` G ) ) e. ran projh -> A. y e. ~H 0 <_ ( ( ( ( projh ` H ) -op ( projh ` G ) ) ` y ) .ih y ) )
23 1 2 pjssposi 
 |-  ( A. y e. ~H 0 <_ ( ( ( ( projh ` H ) -op ( projh ` G ) ) ` y ) .ih y ) <-> G C_ H )
24 23 3 bitri 
 |-  ( A. y e. ~H 0 <_ ( ( ( ( projh ` H ) -op ( projh ` G ) ) ` y ) .ih y ) <-> ( ( projh ` H ) -op ( projh ` G ) ) = ( projh ` ( H i^i ( _|_ ` G ) ) ) )
25 22 24 sylib 
 |-  ( ( ( projh ` H ) -op ( projh ` G ) ) e. ran projh -> ( ( projh ` H ) -op ( projh ` G ) ) = ( projh ` ( H i^i ( _|_ ` G ) ) ) )
26 10 25 impbii 
 |-  ( ( ( projh ` H ) -op ( projh ` G ) ) = ( projh ` ( H i^i ( _|_ ` G ) ) ) <-> ( ( projh ` H ) -op ( projh ` G ) ) e. ran projh )
27 3 26 bitri 
 |-  ( G C_ H <-> ( ( projh ` H ) -op ( projh ` G ) ) e. ran projh )