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 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
poimir.i ⊢ 𝐼 = ( ( 0 [,] 1 ) ↑m ( 1 ... 𝑁 ) )
poimir.r ⊢ 𝑅 = ( ∏t ‘ ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) )
broucube.1 ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝑅 ↾t 𝐼 ) Cn ( 𝑅 ↾t 𝐼 ) ) )
Assertion broucube ( 𝜑 → ∃ 𝑐 ∈ 𝐼 𝑐 = ( 𝐹 ‘ 𝑐 ) )

Proof

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