Metamath Proof Explorer

Theorem pjcompi

Description: Component of a projection. (Contributed by NM, 31-Oct-1999) (Revised by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

Ref Expression
Hypothesis pjidm.1 
|- H e. CH
Assertion pjcompi 
|- ( ( A e. H /\ B e. ( _|_ ` H ) ) -> ( ( projh ` H ) ` ( A +h B ) ) = A )

Proof

Step Hyp Ref Expression
1 pjidm.1 
 |-  H e. CH
2 1 cheli 
 |-  ( A e. H -> A e. ~H )
3 1 choccli 
 |-  ( _|_ ` H ) e. CH
4 3 cheli 
 |-  ( B e. ( _|_ ` H ) -> B e. ~H )
5 hvaddcl 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A +h B ) e. ~H )
6 2 4 5 syl2an 
 |-  ( ( A e. H /\ B e. ( _|_ ` H ) ) -> ( A +h B ) e. ~H )
7 axpjpj 
 |-  ( ( H e. CH /\ ( A +h B ) e. ~H ) -> ( A +h B ) = ( ( ( projh ` H ) ` ( A +h B ) ) +h ( ( projh ` ( _|_ ` H ) ) ` ( A +h B ) ) ) )
8 1 6 7 sylancr 
 |-  ( ( A e. H /\ B e. ( _|_ ` H ) ) -> ( A +h B ) = ( ( ( projh ` H ) ` ( A +h B ) ) +h ( ( projh ` ( _|_ ` H ) ) ` ( A +h B ) ) ) )
9 eqid 
 |-  ( A +h B ) = ( A +h B )
10 axpjcl 
 |-  ( ( H e. CH /\ ( A +h B ) e. ~H ) -> ( ( projh ` H ) ` ( A +h B ) ) e. H )
11 1 6 10 sylancr 
 |-  ( ( A e. H /\ B e. ( _|_ ` H ) ) -> ( ( projh ` H ) ` ( A +h B ) ) e. H )
12 axpjcl 
 |-  ( ( ( _|_ ` H ) e. CH /\ ( A +h B ) e. ~H ) -> ( ( projh ` ( _|_ ` H ) ) ` ( A +h B ) ) e. ( _|_ ` H ) )
13 3 6 12 sylancr 
 |-  ( ( A e. H /\ B e. ( _|_ ` H ) ) -> ( ( projh ` ( _|_ ` H ) ) ` ( A +h B ) ) e. ( _|_ ` H ) )
14 simpl 
 |-  ( ( A e. H /\ B e. ( _|_ ` H ) ) -> A e. H )
15 simpr 
 |-  ( ( A e. H /\ B e. ( _|_ ` H ) ) -> B e. ( _|_ ` H ) )
16 1 chocunii 
 |-  ( ( ( ( ( projh ` H ) ` ( A +h B ) ) e. H /\ ( ( projh ` ( _|_ ` H ) ) ` ( A +h B ) ) e. ( _|_ ` H ) ) /\ ( A e. H /\ B e. ( _|_ ` H ) ) ) -> ( ( ( A +h B ) = ( ( ( projh ` H ) ` ( A +h B ) ) +h ( ( projh ` ( _|_ ` H ) ) ` ( A +h B ) ) ) /\ ( A +h B ) = ( A +h B ) ) -> ( ( ( projh ` H ) ` ( A +h B ) ) = A /\ ( ( projh ` ( _|_ ` H ) ) ` ( A +h B ) ) = B ) ) )
17 11 13 14 15 16 syl22anc 
 |-  ( ( A e. H /\ B e. ( _|_ ` H ) ) -> ( ( ( A +h B ) = ( ( ( projh ` H ) ` ( A +h B ) ) +h ( ( projh ` ( _|_ ` H ) ) ` ( A +h B ) ) ) /\ ( A +h B ) = ( A +h B ) ) -> ( ( ( projh ` H ) ` ( A +h B ) ) = A /\ ( ( projh ` ( _|_ ` H ) ) ` ( A +h B ) ) = B ) ) )
18 9 17 mpan2i 
 |-  ( ( A e. H /\ B e. ( _|_ ` H ) ) -> ( ( A +h B ) = ( ( ( projh ` H ) ` ( A +h B ) ) +h ( ( projh ` ( _|_ ` H ) ) ` ( A +h B ) ) ) -> ( ( ( projh ` H ) ` ( A +h B ) ) = A /\ ( ( projh ` ( _|_ ` H ) ) ` ( A +h B ) ) = B ) ) )
19 8 18 mpd 
 |-  ( ( A e. H /\ B e. ( _|_ ` H ) ) -> ( ( ( projh ` H ) ` ( A +h B ) ) = A /\ ( ( projh ` ( _|_ ` H ) ) ` ( A +h B ) ) = B ) )
20 19 simpld 
 |-  ( ( A e. H /\ B e. ( _|_ ` H ) ) -> ( ( projh ` H ) ` ( A +h B ) ) = A )