Metamath Proof Explorer

Theorem pj3lem1

Description: Lemma for projection triplet theorem. (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 pj3lem1 
|- ( A e. ( ( F i^i G ) i^i H ) -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` A ) = A )

Proof

Step Hyp Ref Expression
1 pjadj2co.1 
 |-  F e. CH
2 pjadj2co.2 
 |-  G e. CH
3 pjadj2co.3 
 |-  H e. CH
4 coass 
 |-  ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( projh ` F ) o. ( ( projh ` G ) o. ( projh ` H ) ) )
5 4 fveq1i 
 |-  ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` A ) = ( ( ( projh ` F ) o. ( ( projh ` G ) o. ( projh ` H ) ) ) ` A )
6 elin 
 |-  ( A e. ( F i^i ( G i^i H ) ) <-> ( A e. F /\ A e. ( G i^i H ) ) )
7 1 cheli 
 |-  ( A e. F -> A e. ~H )
8 7 adantr 
 |-  ( ( A e. F /\ A e. ( G i^i H ) ) -> A e. ~H )
9 1 pjfi 
 |-  ( projh ` F ) : ~H --> ~H
10 2 pjfi 
 |-  ( projh ` G ) : ~H --> ~H
11 3 pjfi 
 |-  ( projh ` H ) : ~H --> ~H
12 10 11 hocofi 
 |-  ( ( projh ` G ) o. ( projh ` H ) ) : ~H --> ~H
13 9 12 hocoi 
 |-  ( A e. ~H -> ( ( ( projh ` F ) o. ( ( projh ` G ) o. ( projh ` H ) ) ) ` A ) = ( ( projh ` F ) ` ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) ) )
14 8 13 syl 
 |-  ( ( A e. F /\ A e. ( G i^i H ) ) -> ( ( ( projh ` F ) o. ( ( projh ` G ) o. ( projh ` H ) ) ) ` A ) = ( ( projh ` F ) ` ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) ) )
15 2 3 pjclem4a 
 |-  ( A e. ( G i^i H ) -> ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) = A )
16 eleq1 
 |-  ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) = A -> ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) e. F <-> A e. F ) )
17 pjid 
 |-  ( ( F e. CH /\ ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) e. F ) -> ( ( projh ` F ) ` ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) ) = ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) )
18 1 17 mpan 
 |-  ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) e. F -> ( ( projh ` F ) ` ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) ) = ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) )
19 16 18 syl6bir 
 |-  ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) = A -> ( A e. F -> ( ( projh ` F ) ` ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) ) = ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) ) )
20 eqeq2 
 |-  ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) = A -> ( ( ( projh ` F ) ` ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) ) = ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) <-> ( ( projh ` F ) ` ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) ) = A ) )
21 19 20 sylibd 
 |-  ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) = A -> ( A e. F -> ( ( projh ` F ) ` ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) ) = A ) )
22 15 21 syl 
 |-  ( A e. ( G i^i H ) -> ( A e. F -> ( ( projh ` F ) ` ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) ) = A ) )
23 22 impcom 
 |-  ( ( A e. F /\ A e. ( G i^i H ) ) -> ( ( projh ` F ) ` ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) ) = A )
24 14 23 eqtrd 
 |-  ( ( A e. F /\ A e. ( G i^i H ) ) -> ( ( ( projh ` F ) o. ( ( projh ` G ) o. ( projh ` H ) ) ) ` A ) = A )
25 6 24 sylbi 
 |-  ( A e. ( F i^i ( G i^i H ) ) -> ( ( ( projh ` F ) o. ( ( projh ` G ) o. ( projh ` H ) ) ) ` A ) = A )
26 inass 
 |-  ( ( F i^i G ) i^i H ) = ( F i^i ( G i^i H ) )
27 25 26 eleq2s 
 |-  ( A e. ( ( F i^i G ) i^i H ) -> ( ( ( projh ` F ) o. ( ( projh ` G ) o. ( projh ` H ) ) ) ` A ) = A )
28 5 27 syl5eq 
 |-  ( A e. ( ( F i^i G ) i^i H ) -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` A ) = A )