Metamath Proof Explorer

Theorem broucube

Description: Brouwer - or as Kulpa calls it, "Bohl-Brouwer" - fixed point theorem for the unit cube. Theorem on Kulpa p. 548. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 
|- ( ph -> N e. NN )
poimir.i 
|- I = ( ( 0 [,] 1 ) ^m ( 1 ... N ) )
poimir.r 
|- R = ( Xt_ ` ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) )
broucube.1 
|- ( ph -> F e. ( ( R |`t I ) Cn ( R |`t I ) ) )
Assertion broucube 
|- ( ph -> E. c e. I c = ( F ` c ) )

Proof

Step Hyp Ref Expression
1 poimir.0 
 |-  ( ph -> N e. NN )
2 poimir.i 
 |-  I = ( ( 0 [,] 1 ) ^m ( 1 ... N ) )
3 poimir.r 
 |-  R = ( Xt_ ` ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) )
4 broucube.1 
 |-  ( ph -> F e. ( ( R |`t I ) Cn ( R |`t I ) ) )
5 elmapfn 
 |-  ( x e. ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) -> x Fn ( 1 ... N ) )
6 5 2 eleq2s 
 |-  ( x e. I -> x Fn ( 1 ... N ) )
7 6 adantl 
 |-  ( ( ph /\ x e. I ) -> x Fn ( 1 ... N ) )
8 ovex 
 |-  ( 1 ... N ) e. _V
9 retopon 
 |-  ( topGen ` ran (,) ) e. ( TopOn ` RR )
10 3 pttoponconst 
 |-  ( ( ( 1 ... N ) e. _V /\ ( topGen ` ran (,) ) e. ( TopOn ` RR ) ) -> R e. ( TopOn ` ( RR ^m ( 1 ... N ) ) ) )
11 8 9 10 mp2an 
 |-  R e. ( TopOn ` ( RR ^m ( 1 ... N ) ) )
12 reex 
 |-  RR e. _V
13 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
14 mapss 
 |-  ( ( RR e. _V /\ ( 0 [,] 1 ) C_ RR ) -> ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) C_ ( RR ^m ( 1 ... N ) ) )
15 12 13 14 mp2an 
 |-  ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) C_ ( RR ^m ( 1 ... N ) )
16 2 15 eqsstri 
 |-  I C_ ( RR ^m ( 1 ... N ) )
17 resttopon 
 |-  ( ( R e. ( TopOn ` ( RR ^m ( 1 ... N ) ) ) /\ I C_ ( RR ^m ( 1 ... N ) ) ) -> ( R |`t I ) e. ( TopOn ` I ) )
18 11 16 17 mp2an 
 |-  ( R |`t I ) e. ( TopOn ` I )
19 18 toponunii 
 |-  I = U. ( R |`t I )
20 19 19 cnf 
 |-  ( F e. ( ( R |`t I ) Cn ( R |`t I ) ) -> F : I --> I )
21 4 20 syl 
 |-  ( ph -> F : I --> I )
22 21 ffvelrnda 
 |-  ( ( ph /\ x e. I ) -> ( F ` x ) e. I )
23 elmapfn 
 |-  ( ( F ` x ) e. ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) -> ( F ` x ) Fn ( 1 ... N ) )
24 23 2 eleq2s 
 |-  ( ( F ` x ) e. I -> ( F ` x ) Fn ( 1 ... N ) )
25 22 24 syl 
 |-  ( ( ph /\ x e. I ) -> ( F ` x ) Fn ( 1 ... N ) )
26 ovexd 
 |-  ( ( ph /\ x e. I ) -> ( 1 ... N ) e. _V )
27 inidm 
 |-  ( ( 1 ... N ) i^i ( 1 ... N ) ) = ( 1 ... N )
28 eqidd 
 |-  ( ( ( ph /\ x e. I ) /\ n e. ( 1 ... N ) ) -> ( x ` n ) = ( x ` n ) )
29 eqidd 
 |-  ( ( ( ph /\ x e. I ) /\ n e. ( 1 ... N ) ) -> ( ( F ` x ) ` n ) = ( ( F ` x ) ` n ) )
30 7 25 26 26 27 28 29 offval 
 |-  ( ( ph /\ x e. I ) -> ( x oF - ( F ` x ) ) = ( n e. ( 1 ... N ) |-> ( ( x ` n ) - ( ( F ` x ) ` n ) ) ) )
31 30 mpteq2dva 
 |-  ( ph -> ( x e. I |-> ( x oF - ( F ` x ) ) ) = ( x e. I |-> ( n e. ( 1 ... N ) |-> ( ( x ` n ) - ( ( F ` x ) ` n ) ) ) ) )
32 18 a1i 
 |-  ( ph -> ( R |`t I ) e. ( TopOn ` I ) )
33 ovexd 
 |-  ( ph -> ( 1 ... N ) e. _V )
34 retop 
 |-  ( topGen ` ran (,) ) e. Top
35 34 fconst6 
 |-  ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) : ( 1 ... N ) --> Top
36 35 a1i 
 |-  ( ph -> ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) : ( 1 ... N ) --> Top )
37 18 a1i 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( R |`t I ) e. ( TopOn ` I ) )
38 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
39 38 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
40 cnrest2r 
 |-  ( ( TopOpen ` CCfld ) e. Top -> ( ( R |`t I ) Cn ( ( TopOpen ` CCfld ) |`t RR ) ) C_ ( ( R |`t I ) Cn ( TopOpen ` CCfld ) ) )
41 39 40 ax-mp 
 |-  ( ( R |`t I ) Cn ( ( TopOpen ` CCfld ) |`t RR ) ) C_ ( ( R |`t I ) Cn ( TopOpen ` CCfld ) )
42 resmpt 
 |-  ( I C_ ( RR ^m ( 1 ... N ) ) -> ( ( x e. ( RR ^m ( 1 ... N ) ) |-> ( x ` n ) ) |` I ) = ( x e. I |-> ( x ` n ) ) )
43 16 42 ax-mp 
 |-  ( ( x e. ( RR ^m ( 1 ... N ) ) |-> ( x ` n ) ) |` I ) = ( x e. I |-> ( x ` n ) )
44 11 toponunii 
 |-  ( RR ^m ( 1 ... N ) ) = U. R
45 44 3 ptpjcn 
 |-  ( ( ( 1 ... N ) e. _V /\ ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) : ( 1 ... N ) --> Top /\ n e. ( 1 ... N ) ) -> ( x e. ( RR ^m ( 1 ... N ) ) |-> ( x ` n ) ) e. ( R Cn ( ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ` n ) ) )
46 8 35 45 mp3an12 
 |-  ( n e. ( 1 ... N ) -> ( x e. ( RR ^m ( 1 ... N ) ) |-> ( x ` n ) ) e. ( R Cn ( ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ` n ) ) )
47 44 cnrest 
 |-  ( ( ( x e. ( RR ^m ( 1 ... N ) ) |-> ( x ` n ) ) e. ( R Cn ( ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ` n ) ) /\ I C_ ( RR ^m ( 1 ... N ) ) ) -> ( ( x e. ( RR ^m ( 1 ... N ) ) |-> ( x ` n ) ) |` I ) e. ( ( R |`t I ) Cn ( ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ` n ) ) )
48 46 16 47 sylancl 
 |-  ( n e. ( 1 ... N ) -> ( ( x e. ( RR ^m ( 1 ... N ) ) |-> ( x ` n ) ) |` I ) e. ( ( R |`t I ) Cn ( ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ` n ) ) )
49 43 48 eqeltrrid 
 |-  ( n e. ( 1 ... N ) -> ( x e. I |-> ( x ` n ) ) e. ( ( R |`t I ) Cn ( ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ` n ) ) )
50 fvex 
 |-  ( topGen ` ran (,) ) e. _V
51 50 fvconst2 
 |-  ( n e. ( 1 ... N ) -> ( ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ` n ) = ( topGen ` ran (,) ) )
52 38 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
53 51 52 eqtrdi 
 |-  ( n e. ( 1 ... N ) -> ( ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ` n ) = ( ( TopOpen ` CCfld ) |`t RR ) )
54 53 oveq2d 
 |-  ( n e. ( 1 ... N ) -> ( ( R |`t I ) Cn ( ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ` n ) ) = ( ( R |`t I ) Cn ( ( TopOpen ` CCfld ) |`t RR ) ) )
55 49 54 eleqtrd 
 |-  ( n e. ( 1 ... N ) -> ( x e. I |-> ( x ` n ) ) e. ( ( R |`t I ) Cn ( ( TopOpen ` CCfld ) |`t RR ) ) )
56 41 55 sselid 
 |-  ( n e. ( 1 ... N ) -> ( x e. I |-> ( x ` n ) ) e. ( ( R |`t I ) Cn ( TopOpen ` CCfld ) ) )
57 56 adantl 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( x e. I |-> ( x ` n ) ) e. ( ( R |`t I ) Cn ( TopOpen ` CCfld ) ) )
58 21 feqmptd 
 |-  ( ph -> F = ( x e. I |-> ( F ` x ) ) )
59 58 4 eqeltrrd 
 |-  ( ph -> ( x e. I |-> ( F ` x ) ) e. ( ( R |`t I ) Cn ( R |`t I ) ) )
60 59 adantr 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( x e. I |-> ( F ` x ) ) e. ( ( R |`t I ) Cn ( R |`t I ) ) )
61 fveq1 
 |-  ( x = z -> ( x ` n ) = ( z ` n ) )
62 61 cbvmptv 
 |-  ( x e. I |-> ( x ` n ) ) = ( z e. I |-> ( z ` n ) )
63 62 57 eqeltrrid 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( z e. I |-> ( z ` n ) ) e. ( ( R |`t I ) Cn ( TopOpen ` CCfld ) ) )
64 fveq1 
 |-  ( z = ( F ` x ) -> ( z ` n ) = ( ( F ` x ) ` n ) )
65 37 60 37 63 64 cnmpt11 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( x e. I |-> ( ( F ` x ) ` n ) ) e. ( ( R |`t I ) Cn ( TopOpen ` CCfld ) ) )
66 38 subcn 
 |-  - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
67 66 a1i 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
68 37 57 65 67 cnmpt12f 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( x e. I |-> ( ( x ` n ) - ( ( F ` x ) ` n ) ) ) e. ( ( R |`t I ) Cn ( TopOpen ` CCfld ) ) )
69 elmapi 
 |-  ( x e. ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) -> x : ( 1 ... N ) --> ( 0 [,] 1 ) )
70 69 2 eleq2s 
 |-  ( x e. I -> x : ( 1 ... N ) --> ( 0 [,] 1 ) )
71 70 ffvelrnda 
 |-  ( ( x e. I /\ n e. ( 1 ... N ) ) -> ( x ` n ) e. ( 0 [,] 1 ) )
72 13 71 sselid 
 |-  ( ( x e. I /\ n e. ( 1 ... N ) ) -> ( x ` n ) e. RR )
73 72 adantll 
 |-  ( ( ( ph /\ x e. I ) /\ n e. ( 1 ... N ) ) -> ( x ` n ) e. RR )
74 elmapi 
 |-  ( ( F ` x ) e. ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) -> ( F ` x ) : ( 1 ... N ) --> ( 0 [,] 1 ) )
75 74 2 eleq2s 
 |-  ( ( F ` x ) e. I -> ( F ` x ) : ( 1 ... N ) --> ( 0 [,] 1 ) )
76 22 75 syl 
 |-  ( ( ph /\ x e. I ) -> ( F ` x ) : ( 1 ... N ) --> ( 0 [,] 1 ) )
77 76 ffvelrnda 
 |-  ( ( ( ph /\ x e. I ) /\ n e. ( 1 ... N ) ) -> ( ( F ` x ) ` n ) e. ( 0 [,] 1 ) )
78 13 77 sselid 
 |-  ( ( ( ph /\ x e. I ) /\ n e. ( 1 ... N ) ) -> ( ( F ` x ) ` n ) e. RR )
79 73 78 resubcld 
 |-  ( ( ( ph /\ x e. I ) /\ n e. ( 1 ... N ) ) -> ( ( x ` n ) - ( ( F ` x ) ` n ) ) e. RR )
80 79 an32s 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. I ) -> ( ( x ` n ) - ( ( F ` x ) ` n ) ) e. RR )
81 80 fmpttd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( x e. I |-> ( ( x ` n ) - ( ( F ` x ) ` n ) ) ) : I --> RR )
82 frn 
 |-  ( ( x e. I |-> ( ( x ` n ) - ( ( F ` x ) ` n ) ) ) : I --> RR -> ran ( x e. I |-> ( ( x ` n ) - ( ( F ` x ) ` n ) ) ) C_ RR )
83 38 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
84 ax-resscn 
 |-  RR C_ CC
85 cnrest2 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ran ( x e. I |-> ( ( x ` n ) - ( ( F ` x ) ` n ) ) ) C_ RR /\ RR C_ CC ) -> ( ( x e. I |-> ( ( x ` n ) - ( ( F ` x ) ` n ) ) ) e. ( ( R |`t I ) Cn ( TopOpen ` CCfld ) ) <-> ( x e. I |-> ( ( x ` n ) - ( ( F ` x ) ` n ) ) ) e. ( ( R |`t I ) Cn ( ( TopOpen ` CCfld ) |`t RR ) ) ) )
86 83 84 85 mp3an13 
 |-  ( ran ( x e. I |-> ( ( x ` n ) - ( ( F ` x ) ` n ) ) ) C_ RR -> ( ( x e. I |-> ( ( x ` n ) - ( ( F ` x ) ` n ) ) ) e. ( ( R |`t I ) Cn ( TopOpen ` CCfld ) ) <-> ( x e. I |-> ( ( x ` n ) - ( ( F ` x ) ` n ) ) ) e. ( ( R |`t I ) Cn ( ( TopOpen ` CCfld ) |`t RR ) ) ) )
87 81 82 86 3syl 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( x e. I |-> ( ( x ` n ) - ( ( F ` x ) ` n ) ) ) e. ( ( R |`t I ) Cn ( TopOpen ` CCfld ) ) <-> ( x e. I |-> ( ( x ` n ) - ( ( F ` x ) ` n ) ) ) e. ( ( R |`t I ) Cn ( ( TopOpen ` CCfld ) |`t RR ) ) ) )
88 68 87 mpbid 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( x e. I |-> ( ( x ` n ) - ( ( F ` x ) ` n ) ) ) e. ( ( R |`t I ) Cn ( ( TopOpen ` CCfld ) |`t RR ) ) )
89 54 adantl 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( R |`t I ) Cn ( ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ` n ) ) = ( ( R |`t I ) Cn ( ( TopOpen ` CCfld ) |`t RR ) ) )
90 88 89 eleqtrrd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( x e. I |-> ( ( x ` n ) - ( ( F ` x ) ` n ) ) ) e. ( ( R |`t I ) Cn ( ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ` n ) ) )
91 3 32 33 36 90 ptcn 
 |-  ( ph -> ( x e. I |-> ( n e. ( 1 ... N ) |-> ( ( x ` n ) - ( ( F ` x ) ` n ) ) ) ) e. ( ( R |`t I ) Cn R ) )
92 31 91 eqeltrd 
 |-  ( ph -> ( x e. I |-> ( x oF - ( F ` x ) ) ) e. ( ( R |`t I ) Cn R ) )
93 simpr2 
 |-  ( ( ph /\ ( n e. ( 1 ... N ) /\ z e. I /\ ( z ` n ) = 0 ) ) -> z e. I )
94 id 
 |-  ( x = z -> x = z )
95 fveq2 
 |-  ( x = z -> ( F ` x ) = ( F ` z ) )
96 94 95 oveq12d 
 |-  ( x = z -> ( x oF - ( F ` x ) ) = ( z oF - ( F ` z ) ) )
97 eqid 
 |-  ( x e. I |-> ( x oF - ( F ` x ) ) ) = ( x e. I |-> ( x oF - ( F ` x ) ) )
98 ovex 
 |-  ( z oF - ( F ` z ) ) e. _V
99 96 97 98 fvmpt 
 |-  ( z e. I -> ( ( x e. I |-> ( x oF - ( F ` x ) ) ) ` z ) = ( z oF - ( F ` z ) ) )
100 99 fveq1d 
 |-  ( z e. I -> ( ( ( x e. I |-> ( x oF - ( F ` x ) ) ) ` z ) ` n ) = ( ( z oF - ( F ` z ) ) ` n ) )
101 93 100 syl 
 |-  ( ( ph /\ ( n e. ( 1 ... N ) /\ z e. I /\ ( z ` n ) = 0 ) ) -> ( ( ( x e. I |-> ( x oF - ( F ` x ) ) ) ` z ) ` n ) = ( ( z oF - ( F ` z ) ) ` n ) )
102 elmapfn 
 |-  ( z e. ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) -> z Fn ( 1 ... N ) )
103 102 2 eleq2s 
 |-  ( z e. I -> z Fn ( 1 ... N ) )
104 103 adantl 
 |-  ( ( ( ph /\ ( z ` n ) = 0 ) /\ z e. I ) -> z Fn ( 1 ... N ) )
105 21 ffvelrnda 
 |-  ( ( ph /\ z e. I ) -> ( F ` z ) e. I )
106 elmapfn 
 |-  ( ( F ` z ) e. ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) -> ( F ` z ) Fn ( 1 ... N ) )
107 106 2 eleq2s 
 |-  ( ( F ` z ) e. I -> ( F ` z ) Fn ( 1 ... N ) )
108 105 107 syl 
 |-  ( ( ph /\ z e. I ) -> ( F ` z ) Fn ( 1 ... N ) )
109 108 adantlr 
 |-  ( ( ( ph /\ ( z ` n ) = 0 ) /\ z e. I ) -> ( F ` z ) Fn ( 1 ... N ) )
110 ovexd 
 |-  ( ( ( ph /\ ( z ` n ) = 0 ) /\ z e. I ) -> ( 1 ... N ) e. _V )
111 simpllr 
 |-  ( ( ( ( ph /\ ( z ` n ) = 0 ) /\ z e. I ) /\ n e. ( 1 ... N ) ) -> ( z ` n ) = 0 )
112 eqidd 
 |-  ( ( ( ( ph /\ ( z ` n ) = 0 ) /\ z e. I ) /\ n e. ( 1 ... N ) ) -> ( ( F ` z ) ` n ) = ( ( F ` z ) ` n ) )
113 104 109 110 110 27 111 112 ofval 
 |-  ( ( ( ( ph /\ ( z ` n ) = 0 ) /\ z e. I ) /\ n e. ( 1 ... N ) ) -> ( ( z oF - ( F ` z ) ) ` n ) = ( 0 - ( ( F ` z ) ` n ) ) )
114 df-neg 
 |-  -u ( ( F ` z ) ` n ) = ( 0 - ( ( F ` z ) ` n ) )
115 113 114 eqtr4di 
 |-  ( ( ( ( ph /\ ( z ` n ) = 0 ) /\ z e. I ) /\ n e. ( 1 ... N ) ) -> ( ( z oF - ( F ` z ) ) ` n ) = -u ( ( F ` z ) ` n ) )
116 115 exp41 
 |-  ( ph -> ( ( z ` n ) = 0 -> ( z e. I -> ( n e. ( 1 ... N ) -> ( ( z oF - ( F ` z ) ) ` n ) = -u ( ( F ` z ) ` n ) ) ) ) )
117 116 com24 
 |-  ( ph -> ( n e. ( 1 ... N ) -> ( z e. I -> ( ( z ` n ) = 0 -> ( ( z oF - ( F ` z ) ) ` n ) = -u ( ( F ` z ) ` n ) ) ) ) )
118 117 3imp2 
 |-  ( ( ph /\ ( n e. ( 1 ... N ) /\ z e. I /\ ( z ` n ) = 0 ) ) -> ( ( z oF - ( F ` z ) ) ` n ) = -u ( ( F ` z ) ` n ) )
119 101 118 eqtrd 
 |-  ( ( ph /\ ( n e. ( 1 ... N ) /\ z e. I /\ ( z ` n ) = 0 ) ) -> ( ( ( x e. I |-> ( x oF - ( F ` x ) ) ) ` z ) ` n ) = -u ( ( F ` z ) ` n ) )
120 elmapi 
 |-  ( ( F ` z ) e. ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) -> ( F ` z ) : ( 1 ... N ) --> ( 0 [,] 1 ) )
121 120 2 eleq2s 
 |-  ( ( F ` z ) e. I -> ( F ` z ) : ( 1 ... N ) --> ( 0 [,] 1 ) )
122 105 121 syl 
 |-  ( ( ph /\ z e. I ) -> ( F ` z ) : ( 1 ... N ) --> ( 0 [,] 1 ) )
123 122 ffvelrnda 
 |-  ( ( ( ph /\ z e. I ) /\ n e. ( 1 ... N ) ) -> ( ( F ` z ) ` n ) e. ( 0 [,] 1 ) )
124 0xr 
 |-  0 e. RR*
125 1xr 
 |-  1 e. RR*
126 iccgelb 
 |-  ( ( 0 e. RR* /\ 1 e. RR* /\ ( ( F ` z ) ` n ) e. ( 0 [,] 1 ) ) -> 0 <_ ( ( F ` z ) ` n ) )
127 124 125 126 mp3an12 
 |-  ( ( ( F ` z ) ` n ) e. ( 0 [,] 1 ) -> 0 <_ ( ( F ` z ) ` n ) )
128 123 127 syl 
 |-  ( ( ( ph /\ z e. I ) /\ n e. ( 1 ... N ) ) -> 0 <_ ( ( F ` z ) ` n ) )
129 13 123 sselid 
 |-  ( ( ( ph /\ z e. I ) /\ n e. ( 1 ... N ) ) -> ( ( F ` z ) ` n ) e. RR )
130 129 le0neg2d 
 |-  ( ( ( ph /\ z e. I ) /\ n e. ( 1 ... N ) ) -> ( 0 <_ ( ( F ` z ) ` n ) <-> -u ( ( F ` z ) ` n ) <_ 0 ) )
131 128 130 mpbid 
 |-  ( ( ( ph /\ z e. I ) /\ n e. ( 1 ... N ) ) -> -u ( ( F ` z ) ` n ) <_ 0 )
132 131 an32s 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ z e. I ) -> -u ( ( F ` z ) ` n ) <_ 0 )
133 132 anasss 
 |-  ( ( ph /\ ( n e. ( 1 ... N ) /\ z e. I ) ) -> -u ( ( F ` z ) ` n ) <_ 0 )
134 133 3adantr3 
 |-  ( ( ph /\ ( n e. ( 1 ... N ) /\ z e. I /\ ( z ` n ) = 0 ) ) -> -u ( ( F ` z ) ` n ) <_ 0 )
135 119 134 eqbrtrd 
 |-  ( ( ph /\ ( n e. ( 1 ... N ) /\ z e. I /\ ( z ` n ) = 0 ) ) -> ( ( ( x e. I |-> ( x oF - ( F ` x ) ) ) ` z ) ` n ) <_ 0 )
136 iccleub 
 |-  ( ( 0 e. RR* /\ 1 e. RR* /\ ( ( F ` z ) ` n ) e. ( 0 [,] 1 ) ) -> ( ( F ` z ) ` n ) <_ 1 )
137 124 125 136 mp3an12 
 |-  ( ( ( F ` z ) ` n ) e. ( 0 [,] 1 ) -> ( ( F ` z ) ` n ) <_ 1 )
138 123 137 syl 
 |-  ( ( ( ph /\ z e. I ) /\ n e. ( 1 ... N ) ) -> ( ( F ` z ) ` n ) <_ 1 )
139 1red 
 |-  ( ( ( ph /\ z e. I ) /\ n e. ( 1 ... N ) ) -> 1 e. RR )
140 139 129 subge0d 
 |-  ( ( ( ph /\ z e. I ) /\ n e. ( 1 ... N ) ) -> ( 0 <_ ( 1 - ( ( F ` z ) ` n ) ) <-> ( ( F ` z ) ` n ) <_ 1 ) )
141 138 140 mpbird 
 |-  ( ( ( ph /\ z e. I ) /\ n e. ( 1 ... N ) ) -> 0 <_ ( 1 - ( ( F ` z ) ` n ) ) )
142 141 an32s 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ z e. I ) -> 0 <_ ( 1 - ( ( F ` z ) ` n ) ) )
143 142 anasss 
 |-  ( ( ph /\ ( n e. ( 1 ... N ) /\ z e. I ) ) -> 0 <_ ( 1 - ( ( F ` z ) ` n ) ) )
144 143 3adantr3 
 |-  ( ( ph /\ ( n e. ( 1 ... N ) /\ z e. I /\ ( z ` n ) = 1 ) ) -> 0 <_ ( 1 - ( ( F ` z ) ` n ) ) )
145 simpr2 
 |-  ( ( ph /\ ( n e. ( 1 ... N ) /\ z e. I /\ ( z ` n ) = 1 ) ) -> z e. I )
146 145 100 syl 
 |-  ( ( ph /\ ( n e. ( 1 ... N ) /\ z e. I /\ ( z ` n ) = 1 ) ) -> ( ( ( x e. I |-> ( x oF - ( F ` x ) ) ) ` z ) ` n ) = ( ( z oF - ( F ` z ) ) ` n ) )
147 103 adantl 
 |-  ( ( ( ph /\ ( z ` n ) = 1 ) /\ z e. I ) -> z Fn ( 1 ... N ) )
148 108 adantlr 
 |-  ( ( ( ph /\ ( z ` n ) = 1 ) /\ z e. I ) -> ( F ` z ) Fn ( 1 ... N ) )
149 ovexd 
 |-  ( ( ( ph /\ ( z ` n ) = 1 ) /\ z e. I ) -> ( 1 ... N ) e. _V )
150 simpllr 
 |-  ( ( ( ( ph /\ ( z ` n ) = 1 ) /\ z e. I ) /\ n e. ( 1 ... N ) ) -> ( z ` n ) = 1 )
151 eqidd 
 |-  ( ( ( ( ph /\ ( z ` n ) = 1 ) /\ z e. I ) /\ n e. ( 1 ... N ) ) -> ( ( F ` z ) ` n ) = ( ( F ` z ) ` n ) )
152 147 148 149 149 27 150 151 ofval 
 |-  ( ( ( ( ph /\ ( z ` n ) = 1 ) /\ z e. I ) /\ n e. ( 1 ... N ) ) -> ( ( z oF - ( F ` z ) ) ` n ) = ( 1 - ( ( F ` z ) ` n ) ) )
153 152 exp41 
 |-  ( ph -> ( ( z ` n ) = 1 -> ( z e. I -> ( n e. ( 1 ... N ) -> ( ( z oF - ( F ` z ) ) ` n ) = ( 1 - ( ( F ` z ) ` n ) ) ) ) ) )
154 153 com24 
 |-  ( ph -> ( n e. ( 1 ... N ) -> ( z e. I -> ( ( z ` n ) = 1 -> ( ( z oF - ( F ` z ) ) ` n ) = ( 1 - ( ( F ` z ) ` n ) ) ) ) ) )
155 154 3imp2 
 |-  ( ( ph /\ ( n e. ( 1 ... N ) /\ z e. I /\ ( z ` n ) = 1 ) ) -> ( ( z oF - ( F ` z ) ) ` n ) = ( 1 - ( ( F ` z ) ` n ) ) )
156 146 155 eqtrd 
 |-  ( ( ph /\ ( n e. ( 1 ... N ) /\ z e. I /\ ( z ` n ) = 1 ) ) -> ( ( ( x e. I |-> ( x oF - ( F ` x ) ) ) ` z ) ` n ) = ( 1 - ( ( F ` z ) ` n ) ) )
157 144 156 breqtrrd 
 |-  ( ( ph /\ ( n e. ( 1 ... N ) /\ z e. I /\ ( z ` n ) = 1 ) ) -> 0 <_ ( ( ( x e. I |-> ( x oF - ( F ` x ) ) ) ` z ) ` n ) )
158 1 2 3 92 135 157 poimir 
 |-  ( ph -> E. c e. I ( ( x e. I |-> ( x oF - ( F ` x ) ) ) ` c ) = ( ( 1 ... N ) X. { 0 } ) )
159 id 
 |-  ( x = c -> x = c )
160 fveq2 
 |-  ( x = c -> ( F ` x ) = ( F ` c ) )
161 159 160 oveq12d 
 |-  ( x = c -> ( x oF - ( F ` x ) ) = ( c oF - ( F ` c ) ) )
162 ovex 
 |-  ( c oF - ( F ` c ) ) e. _V
163 161 97 162 fvmpt 
 |-  ( c e. I -> ( ( x e. I |-> ( x oF - ( F ` x ) ) ) ` c ) = ( c oF - ( F ` c ) ) )
164 163 adantl 
 |-  ( ( ph /\ c e. I ) -> ( ( x e. I |-> ( x oF - ( F ` x ) ) ) ` c ) = ( c oF - ( F ` c ) ) )
165 164 eqeq1d 
 |-  ( ( ph /\ c e. I ) -> ( ( ( x e. I |-> ( x oF - ( F ` x ) ) ) ` c ) = ( ( 1 ... N ) X. { 0 } ) <-> ( c oF - ( F ` c ) ) = ( ( 1 ... N ) X. { 0 } ) ) )
166 elmapfn 
 |-  ( c e. ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) -> c Fn ( 1 ... N ) )
167 166 2 eleq2s 
 |-  ( c e. I -> c Fn ( 1 ... N ) )
168 167 adantl 
 |-  ( ( ph /\ c e. I ) -> c Fn ( 1 ... N ) )
169 21 ffvelrnda 
 |-  ( ( ph /\ c e. I ) -> ( F ` c ) e. I )
170 elmapfn 
 |-  ( ( F ` c ) e. ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) -> ( F ` c ) Fn ( 1 ... N ) )
171 170 2 eleq2s 
 |-  ( ( F ` c ) e. I -> ( F ` c ) Fn ( 1 ... N ) )
172 169 171 syl 
 |-  ( ( ph /\ c e. I ) -> ( F ` c ) Fn ( 1 ... N ) )
173 ovexd 
 |-  ( ( ph /\ c e. I ) -> ( 1 ... N ) e. _V )
174 eqidd 
 |-  ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( c ` n ) = ( c ` n ) )
175 eqidd 
 |-  ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( ( F ` c ) ` n ) = ( ( F ` c ) ` n ) )
176 168 172 173 173 27 174 175 ofval 
 |-  ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( ( c oF - ( F ` c ) ) ` n ) = ( ( c ` n ) - ( ( F ` c ) ` n ) ) )
177 c0ex 
 |-  0 e. _V
178 177 fvconst2 
 |-  ( n e. ( 1 ... N ) -> ( ( ( 1 ... N ) X. { 0 } ) ` n ) = 0 )
179 178 adantl 
 |-  ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( ( ( 1 ... N ) X. { 0 } ) ` n ) = 0 )
180 176 179 eqeq12d 
 |-  ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( ( ( c oF - ( F ` c ) ) ` n ) = ( ( ( 1 ... N ) X. { 0 } ) ` n ) <-> ( ( c ` n ) - ( ( F ` c ) ` n ) ) = 0 ) )
181 13 84 sstri 
 |-  ( 0 [,] 1 ) C_ CC
182 elmapi 
 |-  ( c e. ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) -> c : ( 1 ... N ) --> ( 0 [,] 1 ) )
183 182 2 eleq2s 
 |-  ( c e. I -> c : ( 1 ... N ) --> ( 0 [,] 1 ) )
184 183 ffvelrnda 
 |-  ( ( c e. I /\ n e. ( 1 ... N ) ) -> ( c ` n ) e. ( 0 [,] 1 ) )
185 181 184 sselid 
 |-  ( ( c e. I /\ n e. ( 1 ... N ) ) -> ( c ` n ) e. CC )
186 185 adantll 
 |-  ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( c ` n ) e. CC )
187 elmapi 
 |-  ( ( F ` c ) e. ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) -> ( F ` c ) : ( 1 ... N ) --> ( 0 [,] 1 ) )
188 187 2 eleq2s 
 |-  ( ( F ` c ) e. I -> ( F ` c ) : ( 1 ... N ) --> ( 0 [,] 1 ) )
189 169 188 syl 
 |-  ( ( ph /\ c e. I ) -> ( F ` c ) : ( 1 ... N ) --> ( 0 [,] 1 ) )
190 189 ffvelrnda 
 |-  ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( ( F ` c ) ` n ) e. ( 0 [,] 1 ) )
191 181 190 sselid 
 |-  ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( ( F ` c ) ` n ) e. CC )
192 186 191 subeq0ad 
 |-  ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( ( ( c ` n ) - ( ( F ` c ) ` n ) ) = 0 <-> ( c ` n ) = ( ( F ` c ) ` n ) ) )
193 180 192 bitrd 
 |-  ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( ( ( c oF - ( F ` c ) ) ` n ) = ( ( ( 1 ... N ) X. { 0 } ) ` n ) <-> ( c ` n ) = ( ( F ` c ) ` n ) ) )
194 193 ralbidva 
 |-  ( ( ph /\ c e. I ) -> ( A. n e. ( 1 ... N ) ( ( c oF - ( F ` c ) ) ` n ) = ( ( ( 1 ... N ) X. { 0 } ) ` n ) <-> A. n e. ( 1 ... N ) ( c ` n ) = ( ( F ` c ) ` n ) ) )
195 168 172 173 173 27 offn 
 |-  ( ( ph /\ c e. I ) -> ( c oF - ( F ` c ) ) Fn ( 1 ... N ) )
196 fnconstg 
 |-  ( 0 e. _V -> ( ( 1 ... N ) X. { 0 } ) Fn ( 1 ... N ) )
197 177 196 ax-mp 
 |-  ( ( 1 ... N ) X. { 0 } ) Fn ( 1 ... N )
198 eqfnfv 
 |-  ( ( ( c oF - ( F ` c ) ) Fn ( 1 ... N ) /\ ( ( 1 ... N ) X. { 0 } ) Fn ( 1 ... N ) ) -> ( ( c oF - ( F ` c ) ) = ( ( 1 ... N ) X. { 0 } ) <-> A. n e. ( 1 ... N ) ( ( c oF - ( F ` c ) ) ` n ) = ( ( ( 1 ... N ) X. { 0 } ) ` n ) ) )
199 195 197 198 sylancl 
 |-  ( ( ph /\ c e. I ) -> ( ( c oF - ( F ` c ) ) = ( ( 1 ... N ) X. { 0 } ) <-> A. n e. ( 1 ... N ) ( ( c oF - ( F ` c ) ) ` n ) = ( ( ( 1 ... N ) X. { 0 } ) ` n ) ) )
200 eqfnfv 
 |-  ( ( c Fn ( 1 ... N ) /\ ( F ` c ) Fn ( 1 ... N ) ) -> ( c = ( F ` c ) <-> A. n e. ( 1 ... N ) ( c ` n ) = ( ( F ` c ) ` n ) ) )
201 168 172 200 syl2anc 
 |-  ( ( ph /\ c e. I ) -> ( c = ( F ` c ) <-> A. n e. ( 1 ... N ) ( c ` n ) = ( ( F ` c ) ` n ) ) )
202 194 199 201 3bitr4d 
 |-  ( ( ph /\ c e. I ) -> ( ( c oF - ( F ` c ) ) = ( ( 1 ... N ) X. { 0 } ) <-> c = ( F ` c ) ) )
203 165 202 bitrd 
 |-  ( ( ph /\ c e. I ) -> ( ( ( x e. I |-> ( x oF - ( F ` x ) ) ) ` c ) = ( ( 1 ... N ) X. { 0 } ) <-> c = ( F ` c ) ) )
204 203 rexbidva 
 |-  ( ph -> ( E. c e. I ( ( x e. I |-> ( x oF - ( F ` x ) ) ) ` c ) = ( ( 1 ... N ) X. { 0 } ) <-> E. c e. I c = ( F ` c ) ) )
205 158 204 mpbid 
 |-  ( ph -> E. c e. I c = ( F ` c ) )