Step | Hyp | Ref
| Expression |
1 | | poimir.0 |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | | poimir.i |
. . 3
⊢ 𝐼 = ((0[,]1)
↑𝑚 (1...𝑁)) |
3 | | poimir.r |
. . 3
⊢ 𝑅 =
(∏t‘((1...𝑁) × {(topGen‘ran
(,))})) |
4 | | elmapfn 7880 |
. . . . . . . 8
⊢ (𝑥 ∈ ((0[,]1)
↑𝑚 (1...𝑁)) → 𝑥 Fn (1...𝑁)) |
5 | 4, 2 | eleq2s 2719 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐼 → 𝑥 Fn (1...𝑁)) |
6 | 5 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑥 Fn (1...𝑁)) |
7 | | broucube.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↾t 𝐼) Cn (𝑅 ↾t 𝐼))) |
8 | | ovex 6678 |
. . . . . . . . . . . . 13
⊢
(1...𝑁) ∈
V |
9 | | retopon 22567 |
. . . . . . . . . . . . 13
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
10 | 3 | pttoponconst 21400 |
. . . . . . . . . . . . 13
⊢
(((1...𝑁) ∈ V
∧ (topGen‘ran (,)) ∈ (TopOn‘ℝ)) → 𝑅 ∈ (TopOn‘(ℝ
↑𝑚 (1...𝑁)))) |
11 | 8, 9, 10 | mp2an 708 |
. . . . . . . . . . . 12
⊢ 𝑅 ∈ (TopOn‘(ℝ
↑𝑚 (1...𝑁))) |
12 | | reex 10027 |
. . . . . . . . . . . . . 14
⊢ ℝ
∈ V |
13 | | unitssre 12319 |
. . . . . . . . . . . . . 14
⊢ (0[,]1)
⊆ ℝ |
14 | | mapss 7900 |
. . . . . . . . . . . . . 14
⊢ ((ℝ
∈ V ∧ (0[,]1) ⊆ ℝ) → ((0[,]1)
↑𝑚 (1...𝑁)) ⊆ (ℝ
↑𝑚 (1...𝑁))) |
15 | 12, 13, 14 | mp2an 708 |
. . . . . . . . . . . . 13
⊢ ((0[,]1)
↑𝑚 (1...𝑁)) ⊆ (ℝ
↑𝑚 (1...𝑁)) |
16 | 2, 15 | eqsstri 3635 |
. . . . . . . . . . . 12
⊢ 𝐼 ⊆ (ℝ
↑𝑚 (1...𝑁)) |
17 | | resttopon 20965 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ (TopOn‘(ℝ
↑𝑚 (1...𝑁))) ∧ 𝐼 ⊆ (ℝ ↑𝑚
(1...𝑁))) → (𝑅 ↾t 𝐼) ∈ (TopOn‘𝐼)) |
18 | 11, 16, 17 | mp2an 708 |
. . . . . . . . . . 11
⊢ (𝑅 ↾t 𝐼) ∈ (TopOn‘𝐼) |
19 | 18 | toponunii 20721 |
. . . . . . . . . 10
⊢ 𝐼 = ∪
(𝑅 ↾t
𝐼) |
20 | 19, 19 | cnf 21050 |
. . . . . . . . 9
⊢ (𝐹 ∈ ((𝑅 ↾t 𝐼) Cn (𝑅 ↾t 𝐼)) → 𝐹:𝐼⟶𝐼) |
21 | 7, 20 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐼⟶𝐼) |
22 | 21 | ffvelrnda 6359 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) ∈ 𝐼) |
23 | | elmapfn 7880 |
. . . . . . . 8
⊢ ((𝐹‘𝑥) ∈ ((0[,]1) ↑𝑚
(1...𝑁)) → (𝐹‘𝑥) Fn (1...𝑁)) |
24 | 23, 2 | eleq2s 2719 |
. . . . . . 7
⊢ ((𝐹‘𝑥) ∈ 𝐼 → (𝐹‘𝑥) Fn (1...𝑁)) |
25 | 22, 24 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) Fn (1...𝑁)) |
26 | | ovexd 6680 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (1...𝑁) ∈ V) |
27 | | inidm 3822 |
. . . . . 6
⊢
((1...𝑁) ∩
(1...𝑁)) = (1...𝑁) |
28 | | eqidd 2623 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑥‘𝑛) = (𝑥‘𝑛)) |
29 | | eqidd 2623 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑥)‘𝑛) = ((𝐹‘𝑥)‘𝑛)) |
30 | 6, 25, 26, 26, 27, 28, 29 | offval 6904 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑥 ∘𝑓 − (𝐹‘𝑥)) = (𝑛 ∈ (1...𝑁) ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛)))) |
31 | 30 | mpteq2dva 4744 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑥 ∘𝑓 − (𝐹‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))))) |
32 | 18 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑅 ↾t 𝐼) ∈ (TopOn‘𝐼)) |
33 | | ovexd 6680 |
. . . . 5
⊢ (𝜑 → (1...𝑁) ∈ V) |
34 | | retop 22565 |
. . . . . . 7
⊢
(topGen‘ran (,)) ∈ Top |
35 | 34 | fconst6 6095 |
. . . . . 6
⊢
((1...𝑁) ×
{(topGen‘ran (,))}):(1...𝑁)⟶Top |
36 | 35 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((1...𝑁) × {(topGen‘ran
(,))}):(1...𝑁)⟶Top) |
37 | 18 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑅 ↾t 𝐼) ∈ (TopOn‘𝐼)) |
38 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
39 | 38 | cnfldtop 22587 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) ∈ Top |
40 | | cnrest2r 21091 |
. . . . . . . . . . 11
⊢
((TopOpen‘ℂfld) ∈ Top → ((𝑅 ↾t 𝐼) Cn
((TopOpen‘ℂfld) ↾t ℝ)) ⊆
((𝑅 ↾t
𝐼) Cn
(TopOpen‘ℂfld))) |
41 | 39, 40 | ax-mp 5 |
. . . . . . . . . 10
⊢ ((𝑅 ↾t 𝐼) Cn
((TopOpen‘ℂfld) ↾t ℝ)) ⊆
((𝑅 ↾t
𝐼) Cn
(TopOpen‘ℂfld)) |
42 | | resmpt 5449 |
. . . . . . . . . . . . 13
⊢ (𝐼 ⊆ (ℝ
↑𝑚 (1...𝑁)) → ((𝑥 ∈ (ℝ ↑𝑚
(1...𝑁)) ↦ (𝑥‘𝑛)) ↾ 𝐼) = (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛))) |
43 | 16, 42 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (ℝ
↑𝑚 (1...𝑁)) ↦ (𝑥‘𝑛)) ↾ 𝐼) = (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) |
44 | 11 | toponunii 20721 |
. . . . . . . . . . . . . . 15
⊢ (ℝ
↑𝑚 (1...𝑁)) = ∪ 𝑅 |
45 | 44, 3 | ptpjcn 21414 |
. . . . . . . . . . . . . 14
⊢
(((1...𝑁) ∈ V
∧ ((1...𝑁) ×
{(topGen‘ran (,))}):(1...𝑁)⟶Top ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ (ℝ ↑𝑚
(1...𝑁)) ↦ (𝑥‘𝑛)) ∈ (𝑅 Cn (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛))) |
46 | 8, 35, 45 | mp3an12 1414 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (1...𝑁) → (𝑥 ∈ (ℝ ↑𝑚
(1...𝑁)) ↦ (𝑥‘𝑛)) ∈ (𝑅 Cn (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛))) |
47 | 44 | cnrest 21089 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ (ℝ
↑𝑚 (1...𝑁)) ↦ (𝑥‘𝑛)) ∈ (𝑅 Cn (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)) ∧
𝐼 ⊆ (ℝ
↑𝑚 (1...𝑁))) → ((𝑥 ∈ (ℝ ↑𝑚
(1...𝑁)) ↦ (𝑥‘𝑛)) ↾ 𝐼) ∈ ((𝑅 ↾t 𝐼) Cn (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛))) |
48 | 46, 16, 47 | sylancl 694 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (1...𝑁) → ((𝑥 ∈ (ℝ ↑𝑚
(1...𝑁)) ↦ (𝑥‘𝑛)) ↾ 𝐼) ∈ ((𝑅 ↾t 𝐼) Cn (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛))) |
49 | 43, 48 | syl5eqelr 2706 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (1...𝑁) → (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) ∈ ((𝑅 ↾t 𝐼) Cn (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛))) |
50 | | fvex 6201 |
. . . . . . . . . . . . . 14
⊢
(topGen‘ran (,)) ∈ V |
51 | 50 | fvconst2 6469 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) =
(topGen‘ran (,))) |
52 | 38 | tgioo2 22606 |
. . . . . . . . . . . . 13
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
53 | 51, 52 | syl6eq 2672 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) =
((TopOpen‘ℂfld) ↾t
ℝ)) |
54 | 53 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (1...𝑁) → ((𝑅 ↾t 𝐼) Cn (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)) = ((𝑅 ↾t 𝐼) Cn
((TopOpen‘ℂfld) ↾t
ℝ))) |
55 | 49, 54 | eleqtrd 2703 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (1...𝑁) → (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) ∈ ((𝑅 ↾t 𝐼) Cn ((TopOpen‘ℂfld)
↾t ℝ))) |
56 | 41, 55 | sseldi 3601 |
. . . . . . . . 9
⊢ (𝑛 ∈ (1...𝑁) → (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) ∈ ((𝑅 ↾t 𝐼) Cn
(TopOpen‘ℂfld))) |
57 | 56 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) ∈ ((𝑅 ↾t 𝐼) Cn
(TopOpen‘ℂfld))) |
58 | 21 | feqmptd 6249 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐼 ↦ (𝐹‘𝑥))) |
59 | 58, 7 | eqeltrrd 2702 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝐹‘𝑥)) ∈ ((𝑅 ↾t 𝐼) Cn (𝑅 ↾t 𝐼))) |
60 | 59 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ (𝐹‘𝑥)) ∈ ((𝑅 ↾t 𝐼) Cn (𝑅 ↾t 𝐼))) |
61 | | fveq1 6190 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (𝑥‘𝑛) = (𝑧‘𝑛)) |
62 | 61 | cbvmptv 4750 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) = (𝑧 ∈ 𝐼 ↦ (𝑧‘𝑛)) |
63 | 62, 57 | syl5eqelr 2706 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑧 ∈ 𝐼 ↦ (𝑧‘𝑛)) ∈ ((𝑅 ↾t 𝐼) Cn
(TopOpen‘ℂfld))) |
64 | | fveq1 6190 |
. . . . . . . . 9
⊢ (𝑧 = (𝐹‘𝑥) → (𝑧‘𝑛) = ((𝐹‘𝑥)‘𝑛)) |
65 | 37, 60, 37, 63, 64 | cnmpt11 21466 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥)‘𝑛)) ∈ ((𝑅 ↾t 𝐼) Cn
(TopOpen‘ℂfld))) |
66 | 38 | subcn 22669 |
. . . . . . . . 9
⊢ −
∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
67 | 66 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → − ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld))) |
68 | 37, 57, 65, 67 | cnmpt12f 21469 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾t 𝐼) Cn
(TopOpen‘ℂfld))) |
69 | | elmapi 7879 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ((0[,]1)
↑𝑚 (1...𝑁)) → 𝑥:(1...𝑁)⟶(0[,]1)) |
70 | 69, 2 | eleq2s 2719 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐼 → 𝑥:(1...𝑁)⟶(0[,]1)) |
71 | 70 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐼 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥‘𝑛) ∈ (0[,]1)) |
72 | 13, 71 | sseldi 3601 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐼 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥‘𝑛) ∈ ℝ) |
73 | 72 | adantll 750 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑥‘𝑛) ∈ ℝ) |
74 | | elmapi 7879 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑥) ∈ ((0[,]1) ↑𝑚
(1...𝑁)) → (𝐹‘𝑥):(1...𝑁)⟶(0[,]1)) |
75 | 74, 2 | eleq2s 2719 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑥) ∈ 𝐼 → (𝐹‘𝑥):(1...𝑁)⟶(0[,]1)) |
76 | 22, 75 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥):(1...𝑁)⟶(0[,]1)) |
77 | 76 | ffvelrnda 6359 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑥)‘𝑛) ∈ (0[,]1)) |
78 | 13, 77 | sseldi 3601 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑥)‘𝑛) ∈ ℝ) |
79 | 73, 78 | resubcld 10458 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛)) ∈ ℝ) |
80 | 79 | an32s 846 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐼) → ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛)) ∈ ℝ) |
81 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) = (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) |
82 | 80, 81 | fmptd 6385 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))):𝐼⟶ℝ) |
83 | | frn 6053 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))):𝐼⟶ℝ → ran (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ⊆ ℝ) |
84 | 38 | cnfldtopon 22586 |
. . . . . . . . 9
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
85 | | ax-resscn 9993 |
. . . . . . . . 9
⊢ ℝ
⊆ ℂ |
86 | | cnrest2 21090 |
. . . . . . . . 9
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ ran (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ⊆ ℝ ∧ ℝ ⊆
ℂ) → ((𝑥 ∈
𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾t 𝐼) Cn (TopOpen‘ℂfld))
↔ (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾t 𝐼) Cn ((TopOpen‘ℂfld)
↾t ℝ)))) |
87 | 84, 85, 86 | mp3an13 1415 |
. . . . . . . 8
⊢ (ran
(𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ⊆ ℝ → ((𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾t 𝐼) Cn (TopOpen‘ℂfld))
↔ (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾t 𝐼) Cn ((TopOpen‘ℂfld)
↾t ℝ)))) |
88 | 82, 83, 87 | 3syl 18 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾t 𝐼) Cn (TopOpen‘ℂfld))
↔ (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾t 𝐼) Cn ((TopOpen‘ℂfld)
↾t ℝ)))) |
89 | 68, 88 | mpbid 222 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾t 𝐼) Cn ((TopOpen‘ℂfld)
↾t ℝ))) |
90 | 54 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑅 ↾t 𝐼) Cn (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)) = ((𝑅 ↾t 𝐼) Cn
((TopOpen‘ℂfld) ↾t
ℝ))) |
91 | 89, 90 | eleqtrrd 2704 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾t 𝐼) Cn (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛))) |
92 | 3, 32, 33, 36, 91 | ptcn 21430 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛)))) ∈ ((𝑅 ↾t 𝐼) Cn 𝑅)) |
93 | 31, 92 | eqeltrd 2701 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑥 ∘𝑓 − (𝐹‘𝑥))) ∈ ((𝑅 ↾t 𝐼) Cn 𝑅)) |
94 | | simpr2 1068 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → 𝑧 ∈ 𝐼) |
95 | | id 22 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → 𝑥 = 𝑧) |
96 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧)) |
97 | 95, 96 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑥 ∘𝑓 − (𝐹‘𝑥)) = (𝑧 ∘𝑓 − (𝐹‘𝑧))) |
98 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐼 ↦ (𝑥 ∘𝑓 − (𝐹‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑥 ∘𝑓 − (𝐹‘𝑥))) |
99 | | ovex 6678 |
. . . . . . . 8
⊢ (𝑧 ∘𝑓
− (𝐹‘𝑧)) ∈ V |
100 | 97, 98, 99 | fvmpt 6282 |
. . . . . . 7
⊢ (𝑧 ∈ 𝐼 → ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘𝑓 − (𝐹‘𝑥)))‘𝑧) = (𝑧 ∘𝑓 − (𝐹‘𝑧))) |
101 | 100 | fveq1d 6193 |
. . . . . 6
⊢ (𝑧 ∈ 𝐼 → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘𝑓 − (𝐹‘𝑥)))‘𝑧)‘𝑛) = ((𝑧 ∘𝑓 − (𝐹‘𝑧))‘𝑛)) |
102 | 94, 101 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘𝑓 − (𝐹‘𝑥)))‘𝑧)‘𝑛) = ((𝑧 ∘𝑓 − (𝐹‘𝑧))‘𝑛)) |
103 | | elmapfn 7880 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ((0[,]1)
↑𝑚 (1...𝑁)) → 𝑧 Fn (1...𝑁)) |
104 | 103, 2 | eleq2s 2719 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝐼 → 𝑧 Fn (1...𝑁)) |
105 | 104 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) → 𝑧 Fn (1...𝑁)) |
106 | 21 | ffvelrnda 6359 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) ∈ 𝐼) |
107 | | elmapfn 7880 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑧) ∈ ((0[,]1) ↑𝑚
(1...𝑁)) → (𝐹‘𝑧) Fn (1...𝑁)) |
108 | 107, 2 | eleq2s 2719 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑧) ∈ 𝐼 → (𝐹‘𝑧) Fn (1...𝑁)) |
109 | 106, 108 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) Fn (1...𝑁)) |
110 | 109 | adantlr 751 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) Fn (1...𝑁)) |
111 | | ovexd 6680 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) → (1...𝑁) ∈ V) |
112 | | simpllr 799 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑧‘𝑛) = 0) |
113 | | eqidd 2623 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) = ((𝐹‘𝑧)‘𝑛)) |
114 | 105, 110,
111, 111, 27, 112, 113 | ofval 6906 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑧 ∘𝑓 − (𝐹‘𝑧))‘𝑛) = (0 − ((𝐹‘𝑧)‘𝑛))) |
115 | | df-neg 10269 |
. . . . . . . . 9
⊢ -((𝐹‘𝑧)‘𝑛) = (0 − ((𝐹‘𝑧)‘𝑛)) |
116 | 114, 115 | syl6eqr 2674 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑧 ∘𝑓 − (𝐹‘𝑧))‘𝑛) = -((𝐹‘𝑧)‘𝑛)) |
117 | 116 | exp41 638 |
. . . . . . 7
⊢ (𝜑 → ((𝑧‘𝑛) = 0 → (𝑧 ∈ 𝐼 → (𝑛 ∈ (1...𝑁) → ((𝑧 ∘𝑓 − (𝐹‘𝑧))‘𝑛) = -((𝐹‘𝑧)‘𝑛))))) |
118 | 117 | com24 95 |
. . . . . 6
⊢ (𝜑 → (𝑛 ∈ (1...𝑁) → (𝑧 ∈ 𝐼 → ((𝑧‘𝑛) = 0 → ((𝑧 ∘𝑓 − (𝐹‘𝑧))‘𝑛) = -((𝐹‘𝑧)‘𝑛))))) |
119 | 118 | 3imp2 1282 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → ((𝑧 ∘𝑓 − (𝐹‘𝑧))‘𝑛) = -((𝐹‘𝑧)‘𝑛)) |
120 | 102, 119 | eqtrd 2656 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘𝑓 − (𝐹‘𝑥)))‘𝑧)‘𝑛) = -((𝐹‘𝑧)‘𝑛)) |
121 | | elmapi 7879 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑧) ∈ ((0[,]1) ↑𝑚
(1...𝑁)) → (𝐹‘𝑧):(1...𝑁)⟶(0[,]1)) |
122 | 121, 2 | eleq2s 2719 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑧) ∈ 𝐼 → (𝐹‘𝑧):(1...𝑁)⟶(0[,]1)) |
123 | 106, 122 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧):(1...𝑁)⟶(0[,]1)) |
124 | 123 | ffvelrnda 6359 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) ∈ (0[,]1)) |
125 | | 0xr 10086 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ* |
126 | | 1re 10039 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
127 | 126 | rexri 10097 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ* |
128 | | iccgelb 12230 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ* ∧ ((𝐹‘𝑧)‘𝑛) ∈ (0[,]1)) → 0 ≤ ((𝐹‘𝑧)‘𝑛)) |
129 | 125, 127,
128 | mp3an12 1414 |
. . . . . . . . 9
⊢ (((𝐹‘𝑧)‘𝑛) ∈ (0[,]1) → 0 ≤ ((𝐹‘𝑧)‘𝑛)) |
130 | 124, 129 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → 0 ≤ ((𝐹‘𝑧)‘𝑛)) |
131 | 13, 124 | sseldi 3601 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) ∈ ℝ) |
132 | 131 | le0neg2d 10600 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (0 ≤ ((𝐹‘𝑧)‘𝑛) ↔ -((𝐹‘𝑧)‘𝑛) ≤ 0)) |
133 | 130, 132 | mpbid 222 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → -((𝐹‘𝑧)‘𝑛) ≤ 0) |
134 | 133 | an32s 846 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑧 ∈ 𝐼) → -((𝐹‘𝑧)‘𝑛) ≤ 0) |
135 | 134 | anasss 679 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼)) → -((𝐹‘𝑧)‘𝑛) ≤ 0) |
136 | 135 | 3adantr3 1222 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → -((𝐹‘𝑧)‘𝑛) ≤ 0) |
137 | 120, 136 | eqbrtrd 4675 |
. . 3
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘𝑓 − (𝐹‘𝑥)))‘𝑧)‘𝑛) ≤ 0) |
138 | | iccleub 12229 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ* ∧ ((𝐹‘𝑧)‘𝑛) ∈ (0[,]1)) → ((𝐹‘𝑧)‘𝑛) ≤ 1) |
139 | 125, 127,
138 | mp3an12 1414 |
. . . . . . . . 9
⊢ (((𝐹‘𝑧)‘𝑛) ∈ (0[,]1) → ((𝐹‘𝑧)‘𝑛) ≤ 1) |
140 | 124, 139 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) ≤ 1) |
141 | | 1red 10055 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → 1 ∈ ℝ) |
142 | 141, 131 | subge0d 10617 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (0 ≤ (1 − ((𝐹‘𝑧)‘𝑛)) ↔ ((𝐹‘𝑧)‘𝑛) ≤ 1)) |
143 | 140, 142 | mpbird 247 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → 0 ≤ (1 − ((𝐹‘𝑧)‘𝑛))) |
144 | 143 | an32s 846 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑧 ∈ 𝐼) → 0 ≤ (1 − ((𝐹‘𝑧)‘𝑛))) |
145 | 144 | anasss 679 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼)) → 0 ≤ (1 − ((𝐹‘𝑧)‘𝑛))) |
146 | 145 | 3adantr3 1222 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → 0 ≤ (1 − ((𝐹‘𝑧)‘𝑛))) |
147 | | simpr2 1068 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → 𝑧 ∈ 𝐼) |
148 | 147, 101 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘𝑓 − (𝐹‘𝑥)))‘𝑧)‘𝑛) = ((𝑧 ∘𝑓 − (𝐹‘𝑧))‘𝑛)) |
149 | 104 | adantl 482 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) → 𝑧 Fn (1...𝑁)) |
150 | 109 | adantlr 751 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) Fn (1...𝑁)) |
151 | | ovexd 6680 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) → (1...𝑁) ∈ V) |
152 | | simpllr 799 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑧‘𝑛) = 1) |
153 | | eqidd 2623 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) = ((𝐹‘𝑧)‘𝑛)) |
154 | 149, 150,
151, 151, 27, 152, 153 | ofval 6906 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑧 ∘𝑓 − (𝐹‘𝑧))‘𝑛) = (1 − ((𝐹‘𝑧)‘𝑛))) |
155 | 154 | exp41 638 |
. . . . . . 7
⊢ (𝜑 → ((𝑧‘𝑛) = 1 → (𝑧 ∈ 𝐼 → (𝑛 ∈ (1...𝑁) → ((𝑧 ∘𝑓 − (𝐹‘𝑧))‘𝑛) = (1 − ((𝐹‘𝑧)‘𝑛)))))) |
156 | 155 | com24 95 |
. . . . . 6
⊢ (𝜑 → (𝑛 ∈ (1...𝑁) → (𝑧 ∈ 𝐼 → ((𝑧‘𝑛) = 1 → ((𝑧 ∘𝑓 − (𝐹‘𝑧))‘𝑛) = (1 − ((𝐹‘𝑧)‘𝑛)))))) |
157 | 156 | 3imp2 1282 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → ((𝑧 ∘𝑓 − (𝐹‘𝑧))‘𝑛) = (1 − ((𝐹‘𝑧)‘𝑛))) |
158 | 148, 157 | eqtrd 2656 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘𝑓 − (𝐹‘𝑥)))‘𝑧)‘𝑛) = (1 − ((𝐹‘𝑧)‘𝑛))) |
159 | 146, 158 | breqtrrd 4681 |
. . 3
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → 0 ≤ (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘𝑓 − (𝐹‘𝑥)))‘𝑧)‘𝑛)) |
160 | 1, 2, 3, 93, 137, 159 | poimir 33442 |
. 2
⊢ (𝜑 → ∃𝑐 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘𝑓 − (𝐹‘𝑥)))‘𝑐) = ((1...𝑁) × {0})) |
161 | | id 22 |
. . . . . . . 8
⊢ (𝑥 = 𝑐 → 𝑥 = 𝑐) |
162 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑥 = 𝑐 → (𝐹‘𝑥) = (𝐹‘𝑐)) |
163 | 161, 162 | oveq12d 6668 |
. . . . . . 7
⊢ (𝑥 = 𝑐 → (𝑥 ∘𝑓 − (𝐹‘𝑥)) = (𝑐 ∘𝑓 − (𝐹‘𝑐))) |
164 | | ovex 6678 |
. . . . . . 7
⊢ (𝑐 ∘𝑓
− (𝐹‘𝑐)) ∈ V |
165 | 163, 98, 164 | fvmpt 6282 |
. . . . . 6
⊢ (𝑐 ∈ 𝐼 → ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘𝑓 − (𝐹‘𝑥)))‘𝑐) = (𝑐 ∘𝑓 − (𝐹‘𝑐))) |
166 | 165 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘𝑓 − (𝐹‘𝑥)))‘𝑐) = (𝑐 ∘𝑓 − (𝐹‘𝑐))) |
167 | 166 | eqeq1d 2624 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘𝑓 − (𝐹‘𝑥)))‘𝑐) = ((1...𝑁) × {0}) ↔ (𝑐 ∘𝑓 − (𝐹‘𝑐)) = ((1...𝑁) × {0}))) |
168 | | elmapfn 7880 |
. . . . . . . . . . 11
⊢ (𝑐 ∈ ((0[,]1)
↑𝑚 (1...𝑁)) → 𝑐 Fn (1...𝑁)) |
169 | 168, 2 | eleq2s 2719 |
. . . . . . . . . 10
⊢ (𝑐 ∈ 𝐼 → 𝑐 Fn (1...𝑁)) |
170 | 169 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → 𝑐 Fn (1...𝑁)) |
171 | 21 | ffvelrnda 6359 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝐹‘𝑐) ∈ 𝐼) |
172 | | elmapfn 7880 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑐) ∈ ((0[,]1) ↑𝑚
(1...𝑁)) → (𝐹‘𝑐) Fn (1...𝑁)) |
173 | 172, 2 | eleq2s 2719 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑐) ∈ 𝐼 → (𝐹‘𝑐) Fn (1...𝑁)) |
174 | 171, 173 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝐹‘𝑐) Fn (1...𝑁)) |
175 | | ovexd 6680 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (1...𝑁) ∈ V) |
176 | | eqidd 2623 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑐‘𝑛) = (𝑐‘𝑛)) |
177 | | eqidd 2623 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑐)‘𝑛) = ((𝐹‘𝑐)‘𝑛)) |
178 | 170, 174,
175, 175, 27, 176, 177 | ofval 6906 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑐 ∘𝑓 − (𝐹‘𝑐))‘𝑛) = ((𝑐‘𝑛) − ((𝐹‘𝑐)‘𝑛))) |
179 | | c0ex 10034 |
. . . . . . . . . 10
⊢ 0 ∈
V |
180 | 179 | fvconst2 6469 |
. . . . . . . . 9
⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {0})‘𝑛) = 0) |
181 | 180 | adantl 482 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {0})‘𝑛) = 0) |
182 | 178, 181 | eqeq12d 2637 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (((𝑐 ∘𝑓 − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ ((𝑐‘𝑛) − ((𝐹‘𝑐)‘𝑛)) = 0)) |
183 | 13, 85 | sstri 3612 |
. . . . . . . . . 10
⊢ (0[,]1)
⊆ ℂ |
184 | | elmapi 7879 |
. . . . . . . . . . . 12
⊢ (𝑐 ∈ ((0[,]1)
↑𝑚 (1...𝑁)) → 𝑐:(1...𝑁)⟶(0[,]1)) |
185 | 184, 2 | eleq2s 2719 |
. . . . . . . . . . 11
⊢ (𝑐 ∈ 𝐼 → 𝑐:(1...𝑁)⟶(0[,]1)) |
186 | 185 | ffvelrnda 6359 |
. . . . . . . . . 10
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑛 ∈ (1...𝑁)) → (𝑐‘𝑛) ∈ (0[,]1)) |
187 | 183, 186 | sseldi 3601 |
. . . . . . . . 9
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑛 ∈ (1...𝑁)) → (𝑐‘𝑛) ∈ ℂ) |
188 | 187 | adantll 750 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑐‘𝑛) ∈ ℂ) |
189 | | elmapi 7879 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑐) ∈ ((0[,]1) ↑𝑚
(1...𝑁)) → (𝐹‘𝑐):(1...𝑁)⟶(0[,]1)) |
190 | 189, 2 | eleq2s 2719 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑐) ∈ 𝐼 → (𝐹‘𝑐):(1...𝑁)⟶(0[,]1)) |
191 | 171, 190 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝐹‘𝑐):(1...𝑁)⟶(0[,]1)) |
192 | 191 | ffvelrnda 6359 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑐)‘𝑛) ∈ (0[,]1)) |
193 | 183, 192 | sseldi 3601 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑐)‘𝑛) ∈ ℂ) |
194 | 188, 193 | subeq0ad 10402 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (((𝑐‘𝑛) − ((𝐹‘𝑐)‘𝑛)) = 0 ↔ (𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛))) |
195 | 182, 194 | bitrd 268 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (((𝑐 ∘𝑓 − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ (𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛))) |
196 | 195 | ralbidva 2985 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (∀𝑛 ∈ (1...𝑁)((𝑐 ∘𝑓 − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ ∀𝑛 ∈ (1...𝑁)(𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛))) |
197 | 170, 174,
175, 175, 27 | offn 6908 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝑐 ∘𝑓 − (𝐹‘𝑐)) Fn (1...𝑁)) |
198 | | fnconstg 6093 |
. . . . . . 7
⊢ (0 ∈
V → ((1...𝑁) ×
{0}) Fn (1...𝑁)) |
199 | 179, 198 | ax-mp 5 |
. . . . . 6
⊢
((1...𝑁) ×
{0}) Fn (1...𝑁) |
200 | | eqfnfv 6311 |
. . . . . 6
⊢ (((𝑐 ∘𝑓
− (𝐹‘𝑐)) Fn (1...𝑁) ∧ ((1...𝑁) × {0}) Fn (1...𝑁)) → ((𝑐 ∘𝑓 − (𝐹‘𝑐)) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)((𝑐 ∘𝑓 − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛))) |
201 | 197, 199,
200 | sylancl 694 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → ((𝑐 ∘𝑓 − (𝐹‘𝑐)) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)((𝑐 ∘𝑓 − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛))) |
202 | | eqfnfv 6311 |
. . . . . 6
⊢ ((𝑐 Fn (1...𝑁) ∧ (𝐹‘𝑐) Fn (1...𝑁)) → (𝑐 = (𝐹‘𝑐) ↔ ∀𝑛 ∈ (1...𝑁)(𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛))) |
203 | 170, 174,
202 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝑐 = (𝐹‘𝑐) ↔ ∀𝑛 ∈ (1...𝑁)(𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛))) |
204 | 196, 201,
203 | 3bitr4d 300 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → ((𝑐 ∘𝑓 − (𝐹‘𝑐)) = ((1...𝑁) × {0}) ↔ 𝑐 = (𝐹‘𝑐))) |
205 | 167, 204 | bitrd 268 |
. . 3
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘𝑓 − (𝐹‘𝑥)))‘𝑐) = ((1...𝑁) × {0}) ↔ 𝑐 = (𝐹‘𝑐))) |
206 | 205 | rexbidva 3049 |
. 2
⊢ (𝜑 → (∃𝑐 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘𝑓 − (𝐹‘𝑥)))‘𝑐) = ((1...𝑁) × {0}) ↔ ∃𝑐 ∈ 𝐼 𝑐 = (𝐹‘𝑐))) |
207 | 160, 206 | mpbid 222 |
1
⊢ (𝜑 → ∃𝑐 ∈ 𝐼 𝑐 = (𝐹‘𝑐)) |