Metamath Proof Explorer

Theorem pj3si

Description: Stronger 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 pj3si 
|- ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) C_ G ) -> ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( projh ` ( ( F i^i G ) i^i H ) ) )

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 2 3 pj2cocli 
 |-  ( x e. ~H -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) e. F )
5 4 adantl 
 |-  ( ( ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) C_ G /\ x e. ~H ) -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) e. F )
6 1 pjfi 
 |-  ( projh ` F ) : ~H --> ~H
7 2 pjfi 
 |-  ( projh ` G ) : ~H --> ~H
8 6 7 hocofi 
 |-  ( ( projh ` F ) o. ( projh ` G ) ) : ~H --> ~H
9 3 pjfi 
 |-  ( projh ` H ) : ~H --> ~H
10 8 9 hocofni 
 |-  ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) Fn ~H
11 fnfvelrn 
 |-  ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) Fn ~H /\ x e. ~H ) -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) e. ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) )
12 10 11 mpan 
 |-  ( x e. ~H -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) e. ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) )
13 ssel 
 |-  ( ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) C_ G -> ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) e. ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) e. G ) )
14 12 13 syl5 
 |-  ( ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) C_ G -> ( x e. ~H -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) e. G ) )
15 14 imp 
 |-  ( ( ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) C_ G /\ x e. ~H ) -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) e. G )
16 5 15 elind 
 |-  ( ( ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) C_ G /\ x e. ~H ) -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) e. ( F i^i G ) )
17 16 adantll 
 |-  ( ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) C_ G ) /\ x e. ~H ) -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) e. ( F i^i G ) )
18 3 2 1 pj2cocli 
 |-  ( x e. ~H -> ( ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) ` x ) e. H )
19 fveq1 
 |-  ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) = ( ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) ` x ) )
20 19 eleq1d 
 |-  ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) -> ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) e. H <-> ( ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) ` x ) e. H ) )
21 18 20 imbitrrid 
 |-  ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) -> ( x e. ~H -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) e. H ) )
22 21 imp 
 |-  ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ x e. ~H ) -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) e. H )
23 22 adantlr 
 |-  ( ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) C_ G ) /\ x e. ~H ) -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) e. H )
24 17 23 elind 
 |-  ( ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) C_ G ) /\ x e. ~H ) -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) e. ( ( F i^i G ) i^i H ) )
25 8 9 hococli 
 |-  ( x e. ~H -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) e. ~H )
26 hvsubcl 
 |-  ( ( x e. ~H /\ ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) e. ~H ) -> ( x -h ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) ) e. ~H )
27 25 26 mpdan 
 |-  ( x e. ~H -> ( x -h ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) ) e. ~H )
28 27 adantl 
 |-  ( ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) C_ G ) /\ x e. ~H ) -> ( x -h ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) ) e. ~H )
29 simpl 
 |-  ( ( x e. ~H /\ y e. ( ( F i^i G ) i^i H ) ) -> x e. ~H )
30 25 adantr 
 |-  ( ( x e. ~H /\ y e. ( ( F i^i G ) i^i H ) ) -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) e. ~H )
31 1 2 chincli 
 |-  ( F i^i G ) e. CH
32 31 3 chincli 
 |-  ( ( F i^i G ) i^i H ) e. CH
33 32 cheli 
 |-  ( y e. ( ( F i^i G ) i^i H ) -> y e. ~H )
34 33 adantl 
 |-  ( ( x e. ~H /\ y e. ( ( F i^i G ) i^i H ) ) -> y e. ~H )
35 29 30 34 3jca 
 |-  ( ( x e. ~H /\ y e. ( ( F i^i G ) i^i H ) ) -> ( x e. ~H /\ ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) e. ~H /\ y e. ~H ) )
36 35 adantl 
 |-  ( ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) C_ G ) /\ ( x e. ~H /\ y e. ( ( F i^i G ) i^i H ) ) ) -> ( x e. ~H /\ ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) e. ~H /\ y e. ~H ) )
37 his2sub 
 |-  ( ( x e. ~H /\ ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) e. ~H /\ y e. ~H ) -> ( ( x -h ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) ) .ih y ) = ( ( x .ih y ) - ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) .ih y ) ) )
38 36 37 syl 
 |-  ( ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) C_ G ) /\ ( x e. ~H /\ y e. ( ( F i^i G ) i^i H ) ) ) -> ( ( x -h ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) ) .ih y ) = ( ( x .ih y ) - ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) .ih y ) ) )
39 19 adantr 
 |-  ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) C_ G ) -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) = ( ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) ` x ) )
40 39 oveq1d 
 |-  ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) C_ G ) -> ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) .ih y ) = ( ( ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) ` x ) .ih y ) )
41 3 2 1 pjadj2coi 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) ` x ) .ih y ) = ( x .ih ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` y ) ) )
42 33 41 sylan2 
 |-  ( ( x e. ~H /\ y e. ( ( F i^i G ) i^i H ) ) -> ( ( ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) ` x ) .ih y ) = ( x .ih ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` y ) ) )
43 1 2 3 pj3lem1 
 |-  ( y e. ( ( F i^i G ) i^i H ) -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` y ) = y )
44 43 oveq2d 
 |-  ( y e. ( ( F i^i G ) i^i H ) -> ( x .ih ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` y ) ) = ( x .ih y ) )
45 44 adantl 
 |-  ( ( x e. ~H /\ y e. ( ( F i^i G ) i^i H ) ) -> ( x .ih ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` y ) ) = ( x .ih y ) )
46 42 45 eqtrd 
 |-  ( ( x e. ~H /\ y e. ( ( F i^i G ) i^i H ) ) -> ( ( ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) ` x ) .ih y ) = ( x .ih y ) )
47 40 46 sylan9eq 
 |-  ( ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) C_ G ) /\ ( x e. ~H /\ y e. ( ( F i^i G ) i^i H ) ) ) -> ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) .ih y ) = ( x .ih y ) )
48 47 oveq1d 
 |-  ( ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) C_ G ) /\ ( x e. ~H /\ y e. ( ( F i^i G ) i^i H ) ) ) -> ( ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) .ih y ) - ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) .ih y ) ) = ( ( x .ih y ) - ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) .ih y ) ) )
49 25 33 anim12i 
 |-  ( ( x e. ~H /\ y e. ( ( F i^i G ) i^i H ) ) -> ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) e. ~H /\ y e. ~H ) )
50 49 adantl 
 |-  ( ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) C_ G ) /\ ( x e. ~H /\ y e. ( ( F i^i G ) i^i H ) ) ) -> ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) e. ~H /\ y e. ~H ) )
51 hicl 
 |-  ( ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) e. ~H /\ y e. ~H ) -> ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) .ih y ) e. CC )
52 50 51 syl 
 |-  ( ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) C_ G ) /\ ( x e. ~H /\ y e. ( ( F i^i G ) i^i H ) ) ) -> ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) .ih y ) e. CC )
53 52 subidd 
 |-  ( ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) C_ G ) /\ ( x e. ~H /\ y e. ( ( F i^i G ) i^i H ) ) ) -> ( ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) .ih y ) - ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) .ih y ) ) = 0 )
54 38 48 53 3eqtr2d 
 |-  ( ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) C_ G ) /\ ( x e. ~H /\ y e. ( ( F i^i G ) i^i H ) ) ) -> ( ( x -h ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) ) .ih y ) = 0 )
55 54 expr 
 |-  ( ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) C_ G ) /\ x e. ~H ) -> ( y e. ( ( F i^i G ) i^i H ) -> ( ( x -h ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) ) .ih y ) = 0 ) )
56 55 ralrimiv 
 |-  ( ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) C_ G ) /\ x e. ~H ) -> A. y e. ( ( F i^i G ) i^i H ) ( ( x -h ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) ) .ih y ) = 0 )
57 32 chshii 
 |-  ( ( F i^i G ) i^i H ) e. SH
58 shocel 
 |-  ( ( ( F i^i G ) i^i H ) e. SH -> ( ( x -h ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) ) e. ( _|_ ` ( ( F i^i G ) i^i H ) ) <-> ( ( x -h ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) ) e. ~H /\ A. y e. ( ( F i^i G ) i^i H ) ( ( x -h ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) ) .ih y ) = 0 ) ) )
59 57 58 ax-mp 
 |-  ( ( x -h ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) ) e. ( _|_ ` ( ( F i^i G ) i^i H ) ) <-> ( ( x -h ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) ) e. ~H /\ A. y e. ( ( F i^i G ) i^i H ) ( ( x -h ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) ) .ih y ) = 0 ) )
60 28 56 59 sylanbrc 
 |-  ( ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) C_ G ) /\ x e. ~H ) -> ( x -h ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) ) e. ( _|_ ` ( ( F i^i G ) i^i H ) ) )
61 32 pjvi 
 |-  ( ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) e. ( ( F i^i G ) i^i H ) /\ ( x -h ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) ) e. ( _|_ ` ( ( F i^i G ) i^i H ) ) ) -> ( ( projh ` ( ( F i^i G ) i^i H ) ) ` ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) +h ( x -h ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) ) ) ) = ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) )
62 24 60 61 syl2anc 
 |-  ( ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) C_ G ) /\ x e. ~H ) -> ( ( projh ` ( ( F i^i G ) i^i H ) ) ` ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) +h ( x -h ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) ) ) ) = ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) )
63 id 
 |-  ( x e. ~H -> x e. ~H )
64 hvaddsub12 
 |-  ( ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) e. ~H /\ x e. ~H /\ ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) e. ~H ) -> ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) +h ( x -h ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) ) ) = ( x +h ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) -h ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) ) ) )
65 25 63 25 64 syl3anc 
 |-  ( x e. ~H -> ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) +h ( x -h ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) ) ) = ( x +h ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) -h ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) ) ) )
66 hvsubid 
 |-  ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) e. ~H -> ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) -h ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) ) = 0h )
67 25 66 syl 
 |-  ( x e. ~H -> ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) -h ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) ) = 0h )
68 67 oveq2d 
 |-  ( x e. ~H -> ( x +h ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) -h ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) ) ) = ( x +h 0h ) )
69 ax-hvaddid 
 |-  ( x e. ~H -> ( x +h 0h ) = x )
70 68 69 eqtrd 
 |-  ( x e. ~H -> ( x +h ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) -h ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) ) ) = x )
71 65 70 eqtrd 
 |-  ( x e. ~H -> ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) +h ( x -h ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) ) ) = x )
72 71 fveq2d 
 |-  ( x e. ~H -> ( ( projh ` ( ( F i^i G ) i^i H ) ) ` ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) +h ( x -h ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) ) ) ) = ( ( projh ` ( ( F i^i G ) i^i H ) ) ` x ) )
73 72 adantl 
 |-  ( ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) C_ G ) /\ x e. ~H ) -> ( ( projh ` ( ( F i^i G ) i^i H ) ) ` ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) +h ( x -h ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) ) ) ) = ( ( projh ` ( ( F i^i G ) i^i H ) ) ` x ) )
74 62 73 eqtr3d 
 |-  ( ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) C_ G ) /\ x e. ~H ) -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) = ( ( projh ` ( ( F i^i G ) i^i H ) ) ` x ) )
75 74 ralrimiva 
 |-  ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) C_ G ) -> A. x e. ~H ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) = ( ( projh ` ( ( F i^i G ) i^i H ) ) ` x ) )
76 8 9 hocofi 
 |-  ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) : ~H --> ~H
77 32 pjfi 
 |-  ( projh ` ( ( F i^i G ) i^i H ) ) : ~H --> ~H
78 76 77 hoeqi 
 |-  ( A. x e. ~H ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` x ) = ( ( projh ` ( ( F i^i G ) i^i H ) ) ` x ) <-> ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( projh ` ( ( F i^i G ) i^i H ) ) )
79 75 78 sylib 
 |-  ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) /\ ran ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) C_ G ) -> ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) = ( projh ` ( ( F i^i G ) i^i H ) ) )