Metamath Proof Explorer

Theorem pj3cor1i

Description: Projection triplet corollary. (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 pj3cor1i 
|- ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) ) -> ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` F ) ) o. ( projh ` G ) ) )

Proof

Step Hyp Ref Expression
1 pjadj2co.1 
 |-  F e. CH
2 pjadj2co.2 
 |-  G e. CH
3 pjadj2co.3 
 |-  H e. CH
4 fveq1 
 |-  ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` y ) = ( ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) ` y ) )
5 4 oveq2d 
 |-  ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) -> ( x .ih ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` y ) ) = ( x .ih ( ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) ` y ) ) )
6 5 adantl 
 |-  ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) ) -> ( x .ih ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` y ) ) = ( x .ih ( ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) ` y ) ) )
7 6 ad2antlr 
 |-  ( ( ( x e. ~H /\ ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) ) ) /\ y e. ~H ) -> ( x .ih ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` y ) ) = ( x .ih ( ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) ` y ) ) )
8 1 2 chincli 
 |-  ( F i^i G ) e. CH
9 8 3 chincli 
 |-  ( ( F i^i G ) i^i H ) e. CH
10 9 pjadji 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( ( projh ` ( ( F i^i G ) i^i H ) ) ` x ) .ih y ) = ( x .ih ( ( projh ` ( ( F i^i G ) i^i H ) ) ` y ) ) )
11 10 adantlr 
 |-  ( ( ( x e. ~H /\ ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) ) ) /\ y e. ~H ) -> ( ( ( projh ` ( ( F i^i G ) i^i H ) ) ` x ) .ih y ) = ( x .ih ( ( projh ` ( ( F i^i G ) i^i H ) ) ` y ) ) )
12 1 2 3 pj3i 
 |-  ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) ) -> ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( projh ` ( ( F i^i G ) i^i H ) ) )
13 12 fveq1d 
 |-  ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) ) -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) = ( ( projh ` ( ( F i^i G ) i^i H ) ) ` x ) )
14 13 oveq1d 
 |-  ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) ) -> ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) .ih y ) = ( ( ( projh ` ( ( F i^i G ) i^i H ) ) ` x ) .ih y ) )
15 14 ad2antlr 
 |-  ( ( ( x e. ~H /\ ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) ) ) /\ y e. ~H ) -> ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) .ih y ) = ( ( ( projh ` ( ( F i^i G ) i^i H ) ) ` x ) .ih y ) )
16 12 fveq1d 
 |-  ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) ) -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` y ) = ( ( projh ` ( ( F i^i G ) i^i H ) ) ` y ) )
17 16 oveq2d 
 |-  ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) ) -> ( x .ih ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` y ) ) = ( x .ih ( ( projh ` ( ( F i^i G ) i^i H ) ) ` y ) ) )
18 17 ad2antlr 
 |-  ( ( ( x e. ~H /\ ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) ) ) /\ y e. ~H ) -> ( x .ih ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` y ) ) = ( x .ih ( ( projh ` ( ( F i^i G ) i^i H ) ) ` y ) ) )
19 11 15 18 3eqtr4d 
 |-  ( ( ( x e. ~H /\ ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) ) ) /\ y e. ~H ) -> ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) .ih y ) = ( x .ih ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` y ) ) )
20 3 1 2 pjadj2coi 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( ( ( ( projh ` H ) o. ( projh ` F ) ) o. ( projh ` G ) ) ` x ) .ih y ) = ( x .ih ( ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) ` y ) ) )
21 20 adantlr 
 |-  ( ( ( x e. ~H /\ ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) ) ) /\ y e. ~H ) -> ( ( ( ( ( projh ` H ) o. ( projh ` F ) ) o. ( projh ` G ) ) ` x ) .ih y ) = ( x .ih ( ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) ` y ) ) )
22 7 19 21 3eqtr4d 
 |-  ( ( ( x e. ~H /\ ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) ) ) /\ y e. ~H ) -> ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) .ih y ) = ( ( ( ( ( projh ` H ) o. ( projh ` F ) ) o. ( projh ` G ) ) ` x ) .ih y ) )
23 22 exp31 
 |-  ( x e. ~H -> ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) ) -> ( y e. ~H -> ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) .ih y ) = ( ( ( ( ( projh ` H ) o. ( projh ` F ) ) o. ( projh ` G ) ) ` x ) .ih y ) ) ) )
24 23 ralrimdv 
 |-  ( x e. ~H -> ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) ) -> A. y e. ~H ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) .ih y ) = ( ( ( ( ( projh ` H ) o. ( projh ` F ) ) o. ( projh ` G ) ) ` x ) .ih y ) ) )
25 1 pjfi 
 |-  ( projh ` F ) : ~H --> ~H
26 2 pjfi 
 |-  ( projh ` G ) : ~H --> ~H
27 25 26 hocofi 
 |-  ( ( projh ` F ) o. ( projh ` G ) ) : ~H --> ~H
28 3 pjfi 
 |-  ( projh ` H ) : ~H --> ~H
29 27 28 hococli 
 |-  ( x e. ~H -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) e. ~H )
30 28 25 hocofi 
 |-  ( ( projh ` H ) o. ( projh ` F ) ) : ~H --> ~H
31 30 26 hococli 
 |-  ( x e. ~H -> ( ( ( ( projh ` H ) o. ( projh ` F ) ) o. ( projh ` G ) ) ` x ) e. ~H )
32 hial2eq 
 |-  ( ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) e. ~H /\ ( ( ( ( projh ` H ) o. ( projh ` F ) ) o. ( projh ` G ) ) ` x ) e. ~H ) -> ( A. y e. ~H ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) .ih y ) = ( ( ( ( ( projh ` H ) o. ( projh ` F ) ) o. ( projh ` G ) ) ` x ) .ih y ) <-> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) = ( ( ( ( projh ` H ) o. ( projh ` F ) ) o. ( projh ` G ) ) ` x ) ) )
33 29 31 32 syl2anc 
 |-  ( x e. ~H -> ( A. y e. ~H ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) .ih y ) = ( ( ( ( ( projh ` H ) o. ( projh ` F ) ) o. ( projh ` G ) ) ` x ) .ih y ) <-> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) = ( ( ( ( projh ` H ) o. ( projh ` F ) ) o. ( projh ` G ) ) ` x ) ) )
34 24 33 sylibd 
 |-  ( x e. ~H -> ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) ) -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) = ( ( ( ( projh ` H ) o. ( projh ` F ) ) o. ( projh ` G ) ) ` x ) ) )
35 34 com12 
 |-  ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) ) -> ( x e. ~H -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) = ( ( ( ( projh ` H ) o. ( projh ` F ) ) o. ( projh ` G ) ) ` x ) ) )
36 35 ralrimiv 
 |-  ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) ) -> A. x e. ~H ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) = ( ( ( ( projh ` H ) o. ( projh ` F ) ) o. ( projh ` G ) ) ` x ) )
37 27 28 hocofi 
 |-  ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) : ~H --> ~H
38 30 26 hocofi 
 |-  ( ( ( projh ` H ) o. ( projh ` F ) ) o. ( projh ` G ) ) : ~H --> ~H
39 37 38 hoeqi 
 |-  ( A. x e. ~H ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) = ( ( ( ( projh ` H ) o. ( projh ` F ) ) o. ( projh ` G ) ) ` x ) <-> ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` F ) ) o. ( projh ` G ) ) )
40 36 39 sylib 
 |-  ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` G ) o. ( projh ` F ) ) o. ( projh ` H ) ) ) -> ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` F ) ) o. ( projh ` G ) ) )