Metamath Proof Explorer

Theorem reparphti

Description: Lemma for reparpht . (Contributed by NM, 15-Jun-2010) (Revised by Mario Carneiro, 7-Jun-2014)

Ref Expression
Hypotheses reparpht.2 
|- ( ph -> F e. ( II Cn J ) )
reparpht.3 
|- ( ph -> G e. ( II Cn II ) )
reparpht.4 
|- ( ph -> ( G ` 0 ) = 0 )
reparpht.5 
|- ( ph -> ( G ` 1 ) = 1 )
reparphti.6 
|- H = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( F ` ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) ) )
Assertion reparphti 
|- ( ph -> H e. ( ( F o. G ) ( PHtpy ` J ) F ) )

Proof

Step Hyp Ref Expression
1 reparpht.2 
 |-  ( ph -> F e. ( II Cn J ) )
2 reparpht.3 
 |-  ( ph -> G e. ( II Cn II ) )
3 reparpht.4 
 |-  ( ph -> ( G ` 0 ) = 0 )
4 reparpht.5 
 |-  ( ph -> ( G ` 1 ) = 1 )
5 reparphti.6 
 |-  H = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( F ` ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) ) )
6 cnco 
 |-  ( ( G e. ( II Cn II ) /\ F e. ( II Cn J ) ) -> ( F o. G ) e. ( II Cn J ) )
7 2 1 6 syl2anc 
 |-  ( ph -> ( F o. G ) e. ( II Cn J ) )
8 iitopon 
 |-  II e. ( TopOn ` ( 0 [,] 1 ) )
9 8 a1i 
 |-  ( ph -> II e. ( TopOn ` ( 0 [,] 1 ) ) )
10 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
11 10 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
12 cnrest2r 
 |-  ( ( TopOpen ` CCfld ) e. Top -> ( ( II tX II ) Cn ( ( TopOpen ` CCfld ) |`t ( 0 [,] 1 ) ) ) C_ ( ( II tX II ) Cn ( TopOpen ` CCfld ) ) )
13 11 12 mp1i 
 |-  ( ph -> ( ( II tX II ) Cn ( ( TopOpen ` CCfld ) |`t ( 0 [,] 1 ) ) ) C_ ( ( II tX II ) Cn ( TopOpen ` CCfld ) ) )
14 9 9 cnmpt2nd 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> y ) e. ( ( II tX II ) Cn II ) )
15 iirevcn 
 |-  ( z e. ( 0 [,] 1 ) |-> ( 1 - z ) ) e. ( II Cn II )
16 15 a1i 
 |-  ( ph -> ( z e. ( 0 [,] 1 ) |-> ( 1 - z ) ) e. ( II Cn II ) )
17 oveq2 
 |-  ( z = y -> ( 1 - z ) = ( 1 - y ) )
18 9 9 14 9 16 17 cnmpt21 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( 1 - y ) ) e. ( ( II tX II ) Cn II ) )
19 10 dfii3 
 |-  II = ( ( TopOpen ` CCfld ) |`t ( 0 [,] 1 ) )
20 19 oveq2i 
 |-  ( ( II tX II ) Cn II ) = ( ( II tX II ) Cn ( ( TopOpen ` CCfld ) |`t ( 0 [,] 1 ) ) )
21 18 20 eleqtrdi 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( 1 - y ) ) e. ( ( II tX II ) Cn ( ( TopOpen ` CCfld ) |`t ( 0 [,] 1 ) ) ) )
22 13 21 sseldd 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( 1 - y ) ) e. ( ( II tX II ) Cn ( TopOpen ` CCfld ) ) )
23 9 9 cnmpt1st 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> x ) e. ( ( II tX II ) Cn II ) )
24 9 9 23 2 cnmpt21f 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( G ` x ) ) e. ( ( II tX II ) Cn II ) )
25 24 20 eleqtrdi 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( G ` x ) ) e. ( ( II tX II ) Cn ( ( TopOpen ` CCfld ) |`t ( 0 [,] 1 ) ) ) )
26 13 25 sseldd 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( G ` x ) ) e. ( ( II tX II ) Cn ( TopOpen ` CCfld ) ) )
27 10 mulcn 
 |-  x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
28 27 a1i 
 |-  ( ph -> x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
29 9 9 22 26 28 cnmpt22f 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( ( 1 - y ) x. ( G ` x ) ) ) e. ( ( II tX II ) Cn ( TopOpen ` CCfld ) ) )
30 14 20 eleqtrdi 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> y ) e. ( ( II tX II ) Cn ( ( TopOpen ` CCfld ) |`t ( 0 [,] 1 ) ) ) )
31 13 30 sseldd 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> y ) e. ( ( II tX II ) Cn ( TopOpen ` CCfld ) ) )
32 23 20 eleqtrdi 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> x ) e. ( ( II tX II ) Cn ( ( TopOpen ` CCfld ) |`t ( 0 [,] 1 ) ) ) )
33 13 32 sseldd 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> x ) e. ( ( II tX II ) Cn ( TopOpen ` CCfld ) ) )
34 9 9 31 33 28 cnmpt22f 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( y x. x ) ) e. ( ( II tX II ) Cn ( TopOpen ` CCfld ) ) )
35 10 addcn 
 |-  + e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
36 35 a1i 
 |-  ( ph -> + e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
37 9 9 29 34 36 cnmpt22f 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) ) e. ( ( II tX II ) Cn ( TopOpen ` CCfld ) ) )
38 10 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
39 38 a1i 
 |-  ( ph -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
40 iiuni 
 |-  ( 0 [,] 1 ) = U. II
41 40 40 cnf 
 |-  ( G e. ( II Cn II ) -> G : ( 0 [,] 1 ) --> ( 0 [,] 1 ) )
42 2 41 syl 
 |-  ( ph -> G : ( 0 [,] 1 ) --> ( 0 [,] 1 ) )
43 42 ffvelrnda 
 |-  ( ( ph /\ x e. ( 0 [,] 1 ) ) -> ( G ` x ) e. ( 0 [,] 1 ) )
44 43 adantrr 
 |-  ( ( ph /\ ( x e. ( 0 [,] 1 ) /\ y e. ( 0 [,] 1 ) ) ) -> ( G ` x ) e. ( 0 [,] 1 ) )
45 simprl 
 |-  ( ( ph /\ ( x e. ( 0 [,] 1 ) /\ y e. ( 0 [,] 1 ) ) ) -> x e. ( 0 [,] 1 ) )
46 simprr 
 |-  ( ( ph /\ ( x e. ( 0 [,] 1 ) /\ y e. ( 0 [,] 1 ) ) ) -> y e. ( 0 [,] 1 ) )
47 0re 
 |-  0 e. RR
48 1re 
 |-  1 e. RR
49 icccvx 
 |-  ( ( 0 e. RR /\ 1 e. RR ) -> ( ( ( G ` x ) e. ( 0 [,] 1 ) /\ x e. ( 0 [,] 1 ) /\ y e. ( 0 [,] 1 ) ) -> ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) e. ( 0 [,] 1 ) ) )
50 47 48 49 mp2an 
 |-  ( ( ( G ` x ) e. ( 0 [,] 1 ) /\ x e. ( 0 [,] 1 ) /\ y e. ( 0 [,] 1 ) ) -> ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) e. ( 0 [,] 1 ) )
51 44 45 46 50 syl3anc 
 |-  ( ( ph /\ ( x e. ( 0 [,] 1 ) /\ y e. ( 0 [,] 1 ) ) ) -> ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) e. ( 0 [,] 1 ) )
52 51 ralrimivva 
 |-  ( ph -> A. x e. ( 0 [,] 1 ) A. y e. ( 0 [,] 1 ) ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) e. ( 0 [,] 1 ) )
53 eqid 
 |-  ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) ) = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) )
54 53 fmpo 
 |-  ( A. x e. ( 0 [,] 1 ) A. y e. ( 0 [,] 1 ) ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) e. ( 0 [,] 1 ) <-> ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) ) : ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) --> ( 0 [,] 1 ) )
55 52 54 sylib 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) ) : ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) --> ( 0 [,] 1 ) )
56 55 frnd 
 |-  ( ph -> ran ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) ) C_ ( 0 [,] 1 ) )
57 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
58 ax-resscn 
 |-  RR C_ CC
59 57 58 sstri 
 |-  ( 0 [,] 1 ) C_ CC
60 59 a1i 
 |-  ( ph -> ( 0 [,] 1 ) C_ CC )
61 cnrest2 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ran ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) ) C_ ( 0 [,] 1 ) /\ ( 0 [,] 1 ) C_ CC ) -> ( ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) ) e. ( ( II tX II ) Cn ( TopOpen ` CCfld ) ) <-> ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) ) e. ( ( II tX II ) Cn ( ( TopOpen ` CCfld ) |`t ( 0 [,] 1 ) ) ) ) )
62 39 56 60 61 syl3anc 
 |-  ( ph -> ( ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) ) e. ( ( II tX II ) Cn ( TopOpen ` CCfld ) ) <-> ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) ) e. ( ( II tX II ) Cn ( ( TopOpen ` CCfld ) |`t ( 0 [,] 1 ) ) ) ) )
63 37 62 mpbid 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) ) e. ( ( II tX II ) Cn ( ( TopOpen ` CCfld ) |`t ( 0 [,] 1 ) ) ) )
64 63 20 eleqtrrdi 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) ) e. ( ( II tX II ) Cn II ) )
65 9 9 64 1 cnmpt21f 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( F ` ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) ) ) e. ( ( II tX II ) Cn J ) )
66 5 65 eqeltrid 
 |-  ( ph -> H e. ( ( II tX II ) Cn J ) )
67 42 ffvelrnda 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( G ` s ) e. ( 0 [,] 1 ) )
68 59 67 sseldi 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( G ` s ) e. CC )
69 68 mulid2d 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 1 x. ( G ` s ) ) = ( G ` s ) )
70 59 sseli 
 |-  ( s e. ( 0 [,] 1 ) -> s e. CC )
71 70 adantl 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> s e. CC )
72 71 mul02d 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 0 x. s ) = 0 )
73 69 72 oveq12d 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( ( 1 x. ( G ` s ) ) + ( 0 x. s ) ) = ( ( G ` s ) + 0 ) )
74 68 addid1d 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( ( G ` s ) + 0 ) = ( G ` s ) )
75 73 74 eqtrd 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( ( 1 x. ( G ` s ) ) + ( 0 x. s ) ) = ( G ` s ) )
76 75 fveq2d 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( F ` ( ( 1 x. ( G ` s ) ) + ( 0 x. s ) ) ) = ( F ` ( G ` s ) ) )
77 simpr 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> s e. ( 0 [,] 1 ) )
78 0elunit 
 |-  0 e. ( 0 [,] 1 )
79 simpr 
 |-  ( ( x = s /\ y = 0 ) -> y = 0 )
80 79 oveq2d 
 |-  ( ( x = s /\ y = 0 ) -> ( 1 - y ) = ( 1 - 0 ) )
81 1m0e1 
 |-  ( 1 - 0 ) = 1
82 80 81 eqtrdi 
 |-  ( ( x = s /\ y = 0 ) -> ( 1 - y ) = 1 )
83 simpl 
 |-  ( ( x = s /\ y = 0 ) -> x = s )
84 83 fveq2d 
 |-  ( ( x = s /\ y = 0 ) -> ( G ` x ) = ( G ` s ) )
85 82 84 oveq12d 
 |-  ( ( x = s /\ y = 0 ) -> ( ( 1 - y ) x. ( G ` x ) ) = ( 1 x. ( G ` s ) ) )
86 79 83 oveq12d 
 |-  ( ( x = s /\ y = 0 ) -> ( y x. x ) = ( 0 x. s ) )
87 85 86 oveq12d 
 |-  ( ( x = s /\ y = 0 ) -> ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) = ( ( 1 x. ( G ` s ) ) + ( 0 x. s ) ) )
88 87 fveq2d 
 |-  ( ( x = s /\ y = 0 ) -> ( F ` ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) ) = ( F ` ( ( 1 x. ( G ` s ) ) + ( 0 x. s ) ) ) )
89 fvex 
 |-  ( F ` ( ( 1 x. ( G ` s ) ) + ( 0 x. s ) ) ) e. _V
90 88 5 89 ovmpoa 
 |-  ( ( s e. ( 0 [,] 1 ) /\ 0 e. ( 0 [,] 1 ) ) -> ( s H 0 ) = ( F ` ( ( 1 x. ( G ` s ) ) + ( 0 x. s ) ) ) )
91 77 78 90 sylancl 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( s H 0 ) = ( F ` ( ( 1 x. ( G ` s ) ) + ( 0 x. s ) ) ) )
92 fvco3 
 |-  ( ( G : ( 0 [,] 1 ) --> ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) -> ( ( F o. G ) ` s ) = ( F ` ( G ` s ) ) )
93 42 92 sylan 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( ( F o. G ) ` s ) = ( F ` ( G ` s ) ) )
94 76 91 93 3eqtr4d 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( s H 0 ) = ( ( F o. G ) ` s ) )
95 1elunit 
 |-  1 e. ( 0 [,] 1 )
96 simpr 
 |-  ( ( x = s /\ y = 1 ) -> y = 1 )
97 96 oveq2d 
 |-  ( ( x = s /\ y = 1 ) -> ( 1 - y ) = ( 1 - 1 ) )
98 1m1e0 
 |-  ( 1 - 1 ) = 0
99 97 98 eqtrdi 
 |-  ( ( x = s /\ y = 1 ) -> ( 1 - y ) = 0 )
100 simpl 
 |-  ( ( x = s /\ y = 1 ) -> x = s )
101 100 fveq2d 
 |-  ( ( x = s /\ y = 1 ) -> ( G ` x ) = ( G ` s ) )
102 99 101 oveq12d 
 |-  ( ( x = s /\ y = 1 ) -> ( ( 1 - y ) x. ( G ` x ) ) = ( 0 x. ( G ` s ) ) )
103 96 100 oveq12d 
 |-  ( ( x = s /\ y = 1 ) -> ( y x. x ) = ( 1 x. s ) )
104 102 103 oveq12d 
 |-  ( ( x = s /\ y = 1 ) -> ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) = ( ( 0 x. ( G ` s ) ) + ( 1 x. s ) ) )
105 104 fveq2d 
 |-  ( ( x = s /\ y = 1 ) -> ( F ` ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) ) = ( F ` ( ( 0 x. ( G ` s ) ) + ( 1 x. s ) ) ) )
106 fvex 
 |-  ( F ` ( ( 0 x. ( G ` s ) ) + ( 1 x. s ) ) ) e. _V
107 105 5 106 ovmpoa 
 |-  ( ( s e. ( 0 [,] 1 ) /\ 1 e. ( 0 [,] 1 ) ) -> ( s H 1 ) = ( F ` ( ( 0 x. ( G ` s ) ) + ( 1 x. s ) ) ) )
108 77 95 107 sylancl 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( s H 1 ) = ( F ` ( ( 0 x. ( G ` s ) ) + ( 1 x. s ) ) ) )
109 68 mul02d 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 0 x. ( G ` s ) ) = 0 )
110 71 mulid2d 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 1 x. s ) = s )
111 109 110 oveq12d 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( ( 0 x. ( G ` s ) ) + ( 1 x. s ) ) = ( 0 + s ) )
112 71 addid2d 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 0 + s ) = s )
113 111 112 eqtrd 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( ( 0 x. ( G ` s ) ) + ( 1 x. s ) ) = s )
114 113 fveq2d 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( F ` ( ( 0 x. ( G ` s ) ) + ( 1 x. s ) ) ) = ( F ` s ) )
115 108 114 eqtrd 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( s H 1 ) = ( F ` s ) )
116 3 adantr 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( G ` 0 ) = 0 )
117 116 oveq2d 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( ( 1 - s ) x. ( G ` 0 ) ) = ( ( 1 - s ) x. 0 ) )
118 ax-1cn 
 |-  1 e. CC
119 subcl 
 |-  ( ( 1 e. CC /\ s e. CC ) -> ( 1 - s ) e. CC )
120 118 71 119 sylancr 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 1 - s ) e. CC )
121 120 mul01d 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( ( 1 - s ) x. 0 ) = 0 )
122 117 121 eqtrd 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( ( 1 - s ) x. ( G ` 0 ) ) = 0 )
123 71 mul01d 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( s x. 0 ) = 0 )
124 122 123 oveq12d 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( ( ( 1 - s ) x. ( G ` 0 ) ) + ( s x. 0 ) ) = ( 0 + 0 ) )
125 00id 
 |-  ( 0 + 0 ) = 0
126 124 125 eqtrdi 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( ( ( 1 - s ) x. ( G ` 0 ) ) + ( s x. 0 ) ) = 0 )
127 126 fveq2d 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( F ` ( ( ( 1 - s ) x. ( G ` 0 ) ) + ( s x. 0 ) ) ) = ( F ` 0 ) )
128 simpr 
 |-  ( ( x = 0 /\ y = s ) -> y = s )
129 128 oveq2d 
 |-  ( ( x = 0 /\ y = s ) -> ( 1 - y ) = ( 1 - s ) )
130 simpl 
 |-  ( ( x = 0 /\ y = s ) -> x = 0 )
131 130 fveq2d 
 |-  ( ( x = 0 /\ y = s ) -> ( G ` x ) = ( G ` 0 ) )
132 129 131 oveq12d 
 |-  ( ( x = 0 /\ y = s ) -> ( ( 1 - y ) x. ( G ` x ) ) = ( ( 1 - s ) x. ( G ` 0 ) ) )
133 128 130 oveq12d 
 |-  ( ( x = 0 /\ y = s ) -> ( y x. x ) = ( s x. 0 ) )
134 132 133 oveq12d 
 |-  ( ( x = 0 /\ y = s ) -> ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) = ( ( ( 1 - s ) x. ( G ` 0 ) ) + ( s x. 0 ) ) )
135 134 fveq2d 
 |-  ( ( x = 0 /\ y = s ) -> ( F ` ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) ) = ( F ` ( ( ( 1 - s ) x. ( G ` 0 ) ) + ( s x. 0 ) ) ) )
136 fvex 
 |-  ( F ` ( ( ( 1 - s ) x. ( G ` 0 ) ) + ( s x. 0 ) ) ) e. _V
137 135 5 136 ovmpoa 
 |-  ( ( 0 e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) -> ( 0 H s ) = ( F ` ( ( ( 1 - s ) x. ( G ` 0 ) ) + ( s x. 0 ) ) ) )
138 78 77 137 sylancr 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 0 H s ) = ( F ` ( ( ( 1 - s ) x. ( G ` 0 ) ) + ( s x. 0 ) ) ) )
139 fvco3 
 |-  ( ( G : ( 0 [,] 1 ) --> ( 0 [,] 1 ) /\ 0 e. ( 0 [,] 1 ) ) -> ( ( F o. G ) ` 0 ) = ( F ` ( G ` 0 ) ) )
140 42 78 139 sylancl 
 |-  ( ph -> ( ( F o. G ) ` 0 ) = ( F ` ( G ` 0 ) ) )
141 3 fveq2d 
 |-  ( ph -> ( F ` ( G ` 0 ) ) = ( F ` 0 ) )
142 140 141 eqtrd 
 |-  ( ph -> ( ( F o. G ) ` 0 ) = ( F ` 0 ) )
143 142 adantr 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( ( F o. G ) ` 0 ) = ( F ` 0 ) )
144 127 138 143 3eqtr4d 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 0 H s ) = ( ( F o. G ) ` 0 ) )
145 4 adantr 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( G ` 1 ) = 1 )
146 145 oveq2d 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( ( 1 - s ) x. ( G ` 1 ) ) = ( ( 1 - s ) x. 1 ) )
147 120 mulid1d 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( ( 1 - s ) x. 1 ) = ( 1 - s ) )
148 146 147 eqtrd 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( ( 1 - s ) x. ( G ` 1 ) ) = ( 1 - s ) )
149 71 mulid1d 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( s x. 1 ) = s )
150 148 149 oveq12d 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( ( ( 1 - s ) x. ( G ` 1 ) ) + ( s x. 1 ) ) = ( ( 1 - s ) + s ) )
151 npcan 
 |-  ( ( 1 e. CC /\ s e. CC ) -> ( ( 1 - s ) + s ) = 1 )
152 118 71 151 sylancr 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( ( 1 - s ) + s ) = 1 )
153 150 152 eqtrd 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( ( ( 1 - s ) x. ( G ` 1 ) ) + ( s x. 1 ) ) = 1 )
154 153 fveq2d 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( F ` ( ( ( 1 - s ) x. ( G ` 1 ) ) + ( s x. 1 ) ) ) = ( F ` 1 ) )
155 simpr 
 |-  ( ( x = 1 /\ y = s ) -> y = s )
156 155 oveq2d 
 |-  ( ( x = 1 /\ y = s ) -> ( 1 - y ) = ( 1 - s ) )
157 simpl 
 |-  ( ( x = 1 /\ y = s ) -> x = 1 )
158 157 fveq2d 
 |-  ( ( x = 1 /\ y = s ) -> ( G ` x ) = ( G ` 1 ) )
159 156 158 oveq12d 
 |-  ( ( x = 1 /\ y = s ) -> ( ( 1 - y ) x. ( G ` x ) ) = ( ( 1 - s ) x. ( G ` 1 ) ) )
160 155 157 oveq12d 
 |-  ( ( x = 1 /\ y = s ) -> ( y x. x ) = ( s x. 1 ) )
161 159 160 oveq12d 
 |-  ( ( x = 1 /\ y = s ) -> ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) = ( ( ( 1 - s ) x. ( G ` 1 ) ) + ( s x. 1 ) ) )
162 161 fveq2d 
 |-  ( ( x = 1 /\ y = s ) -> ( F ` ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) ) = ( F ` ( ( ( 1 - s ) x. ( G ` 1 ) ) + ( s x. 1 ) ) ) )
163 fvex 
 |-  ( F ` ( ( ( 1 - s ) x. ( G ` 1 ) ) + ( s x. 1 ) ) ) e. _V
164 162 5 163 ovmpoa 
 |-  ( ( 1 e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) -> ( 1 H s ) = ( F ` ( ( ( 1 - s ) x. ( G ` 1 ) ) + ( s x. 1 ) ) ) )
165 95 77 164 sylancr 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 1 H s ) = ( F ` ( ( ( 1 - s ) x. ( G ` 1 ) ) + ( s x. 1 ) ) ) )
166 fvco3 
 |-  ( ( G : ( 0 [,] 1 ) --> ( 0 [,] 1 ) /\ 1 e. ( 0 [,] 1 ) ) -> ( ( F o. G ) ` 1 ) = ( F ` ( G ` 1 ) ) )
167 42 95 166 sylancl 
 |-  ( ph -> ( ( F o. G ) ` 1 ) = ( F ` ( G ` 1 ) ) )
168 4 fveq2d 
 |-  ( ph -> ( F ` ( G ` 1 ) ) = ( F ` 1 ) )
169 167 168 eqtrd 
 |-  ( ph -> ( ( F o. G ) ` 1 ) = ( F ` 1 ) )
170 169 adantr 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( ( F o. G ) ` 1 ) = ( F ` 1 ) )
171 154 165 170 3eqtr4d 
 |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 1 H s ) = ( ( F o. G ) ` 1 ) )
172 7 1 66 94 115 144 171 isphtpy2d 
 |-  ( ph -> H e. ( ( F o. G ) ( PHtpy ` J ) F ) )