Metamath Proof Explorer

Theorem pjocini

Description: Membership of projection in orthocomplement of intersection. (Contributed by NM, 21-Apr-2001) (New usage is discouraged.)

Ref Expression
Hypotheses pjocin.1 
|- G e. CH
pjocin.2 
|- H e. CH
Assertion pjocini 
|- ( A e. ( _|_ ` ( G i^i H ) ) -> ( ( projh ` G ) ` A ) e. ( _|_ ` ( G i^i H ) ) )

Proof

Step Hyp Ref Expression
1 pjocin.1 
 |-  G e. CH
2 pjocin.2 
 |-  H e. CH
3 1 2 chincli 
 |-  ( G i^i H ) e. CH
4 3 choccli 
 |-  ( _|_ ` ( G i^i H ) ) e. CH
5 4 cheli 
 |-  ( A e. ( _|_ ` ( G i^i H ) ) -> A e. ~H )
6 pjpo 
 |-  ( ( G e. CH /\ A e. ~H ) -> ( ( projh ` G ) ` A ) = ( A -h ( ( projh ` ( _|_ ` G ) ) ` A ) ) )
7 1 5 6 sylancr 
 |-  ( A e. ( _|_ ` ( G i^i H ) ) -> ( ( projh ` G ) ` A ) = ( A -h ( ( projh ` ( _|_ ` G ) ) ` A ) ) )
8 inss1 
 |-  ( G i^i H ) C_ G
9 3 1 chsscon3i 
 |-  ( ( G i^i H ) C_ G <-> ( _|_ ` G ) C_ ( _|_ ` ( G i^i H ) ) )
10 8 9 mpbi 
 |-  ( _|_ ` G ) C_ ( _|_ ` ( G i^i H ) )
11 1 choccli 
 |-  ( _|_ ` G ) e. CH
12 11 pjcli 
 |-  ( A e. ~H -> ( ( projh ` ( _|_ ` G ) ) ` A ) e. ( _|_ ` G ) )
13 5 12 syl 
 |-  ( A e. ( _|_ ` ( G i^i H ) ) -> ( ( projh ` ( _|_ ` G ) ) ` A ) e. ( _|_ ` G ) )
14 10 13 sseldi 
 |-  ( A e. ( _|_ ` ( G i^i H ) ) -> ( ( projh ` ( _|_ ` G ) ) ` A ) e. ( _|_ ` ( G i^i H ) ) )
15 4 chshii 
 |-  ( _|_ ` ( G i^i H ) ) e. SH
16 shsubcl 
 |-  ( ( ( _|_ ` ( G i^i H ) ) e. SH /\ A e. ( _|_ ` ( G i^i H ) ) /\ ( ( projh ` ( _|_ ` G ) ) ` A ) e. ( _|_ ` ( G i^i H ) ) ) -> ( A -h ( ( projh ` ( _|_ ` G ) ) ` A ) ) e. ( _|_ ` ( G i^i H ) ) )
17 15 16 mp3an1 
 |-  ( ( A e. ( _|_ ` ( G i^i H ) ) /\ ( ( projh ` ( _|_ ` G ) ) ` A ) e. ( _|_ ` ( G i^i H ) ) ) -> ( A -h ( ( projh ` ( _|_ ` G ) ) ` A ) ) e. ( _|_ ` ( G i^i H ) ) )
18 14 17 mpdan 
 |-  ( A e. ( _|_ ` ( G i^i H ) ) -> ( A -h ( ( projh ` ( _|_ ` G ) ) ` A ) ) e. ( _|_ ` ( G i^i H ) ) )
19 7 18 eqeltrd 
 |-  ( A e. ( _|_ ` ( G i^i H ) ) -> ( ( projh ` G ) ` A ) e. ( _|_ ` ( G i^i H ) ) )