Metamath Proof Explorer

Theorem pj2cocli

Description: Closure of double composition of projections. (Contributed by NM, 2-Dec-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjadj2co.1 
|- F e. CH
pjadj2co.2 
|- G e. CH
pjadj2co.3 
|- H e. CH
Assertion pj2cocli 
|- ( A e. ~H -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` A ) e. F )

Proof

Step Hyp Ref Expression
1 pjadj2co.1 
 |-  F e. CH
2 pjadj2co.2 
 |-  G e. CH
3 pjadj2co.3 
 |-  H e. CH
4 1 pjfi 
 |-  ( projh ` F ) : ~H --> ~H
5 2 pjfi 
 |-  ( projh ` G ) : ~H --> ~H
6 3 pjfi 
 |-  ( projh ` H ) : ~H --> ~H
7 4 5 6 ho2coi 
 |-  ( A e. ~H -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` A ) = ( ( projh ` F ) ` ( ( projh ` G ) ` ( ( projh ` H ) ` A ) ) ) )
8 3 pjhcli 
 |-  ( A e. ~H -> ( ( projh ` H ) ` A ) e. ~H )
9 2 pjhcli 
 |-  ( ( ( projh ` H ) ` A ) e. ~H -> ( ( projh ` G ) ` ( ( projh ` H ) ` A ) ) e. ~H )
10 1 pjcli 
 |-  ( ( ( projh ` G ) ` ( ( projh ` H ) ` A ) ) e. ~H -> ( ( projh ` F ) ` ( ( projh ` G ) ` ( ( projh ` H ) ` A ) ) ) e. F )
11 8 9 10 3syl 
 |-  ( A e. ~H -> ( ( projh ` F ) ` ( ( projh ` G ) ` ( ( projh ` H ) ` A ) ) ) e. F )
12 7 11 eqeltrd 
 |-  ( A e. ~H -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` A ) e. F )