Step | Hyp | Ref
| Expression |
1 | | poimir.0 |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | | poimir.i |
. . 3
⊢ 𝐼 = ((0[,]1) ↑m
(1...𝑁)) |
3 | | poimir.r |
. . 3
⊢ 𝑅 =
(∏t‘((1...𝑁) × {(topGen‘ran
(,))})) |
4 | | elmapfn 8477 |
. . . . . . . 8
⊢ (𝑥 ∈ ((0[,]1)
↑m (1...𝑁))
→ 𝑥 Fn (1...𝑁)) |
5 | 4, 2 | eleq2s 2851 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐼 → 𝑥 Fn (1...𝑁)) |
6 | 5 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑥 Fn (1...𝑁)) |
7 | | broucube.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↾t 𝐼) Cn (𝑅 ↾t 𝐼))) |
8 | | ovex 7205 |
. . . . . . . . . . . . 13
⊢
(1...𝑁) ∈
V |
9 | | retopon 23518 |
. . . . . . . . . . . . 13
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
10 | 3 | pttoponconst 22350 |
. . . . . . . . . . . . 13
⊢
(((1...𝑁) ∈ V
∧ (topGen‘ran (,)) ∈ (TopOn‘ℝ)) → 𝑅 ∈ (TopOn‘(ℝ
↑m (1...𝑁)))) |
11 | 8, 9, 10 | mp2an 692 |
. . . . . . . . . . . 12
⊢ 𝑅 ∈ (TopOn‘(ℝ
↑m (1...𝑁))) |
12 | | reex 10708 |
. . . . . . . . . . . . . 14
⊢ ℝ
∈ V |
13 | | unitssre 12975 |
. . . . . . . . . . . . . 14
⊢ (0[,]1)
⊆ ℝ |
14 | | mapss 8501 |
. . . . . . . . . . . . . 14
⊢ ((ℝ
∈ V ∧ (0[,]1) ⊆ ℝ) → ((0[,]1) ↑m
(1...𝑁)) ⊆ (ℝ
↑m (1...𝑁))) |
15 | 12, 13, 14 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ ((0[,]1)
↑m (1...𝑁))
⊆ (ℝ ↑m (1...𝑁)) |
16 | 2, 15 | eqsstri 3911 |
. . . . . . . . . . . 12
⊢ 𝐼 ⊆ (ℝ
↑m (1...𝑁)) |
17 | | resttopon 21914 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ (TopOn‘(ℝ
↑m (1...𝑁))) ∧ 𝐼 ⊆ (ℝ ↑m
(1...𝑁))) → (𝑅 ↾t 𝐼) ∈ (TopOn‘𝐼)) |
18 | 11, 16, 17 | mp2an 692 |
. . . . . . . . . . 11
⊢ (𝑅 ↾t 𝐼) ∈ (TopOn‘𝐼) |
19 | 18 | toponunii 21669 |
. . . . . . . . . 10
⊢ 𝐼 = ∪
(𝑅 ↾t
𝐼) |
20 | 19, 19 | cnf 21999 |
. . . . . . . . 9
⊢ (𝐹 ∈ ((𝑅 ↾t 𝐼) Cn (𝑅 ↾t 𝐼)) → 𝐹:𝐼⟶𝐼) |
21 | 7, 20 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐼⟶𝐼) |
22 | 21 | ffvelrnda 6863 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) ∈ 𝐼) |
23 | | elmapfn 8477 |
. . . . . . . 8
⊢ ((𝐹‘𝑥) ∈ ((0[,]1) ↑m
(1...𝑁)) → (𝐹‘𝑥) Fn (1...𝑁)) |
24 | 23, 2 | eleq2s 2851 |
. . . . . . 7
⊢ ((𝐹‘𝑥) ∈ 𝐼 → (𝐹‘𝑥) Fn (1...𝑁)) |
25 | 22, 24 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) Fn (1...𝑁)) |
26 | | ovexd 7207 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (1...𝑁) ∈ V) |
27 | | inidm 4109 |
. . . . . 6
⊢
((1...𝑁) ∩
(1...𝑁)) = (1...𝑁) |
28 | | eqidd 2739 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑥‘𝑛) = (𝑥‘𝑛)) |
29 | | eqidd 2739 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑥)‘𝑛) = ((𝐹‘𝑥)‘𝑛)) |
30 | 6, 25, 26, 26, 27, 28, 29 | offval 7435 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑥 ∘f − (𝐹‘𝑥)) = (𝑛 ∈ (1...𝑁) ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛)))) |
31 | 30 | mpteq2dva 5125 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑥 ∘f − (𝐹‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))))) |
32 | 18 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑅 ↾t 𝐼) ∈ (TopOn‘𝐼)) |
33 | | ovexd 7207 |
. . . . 5
⊢ (𝜑 → (1...𝑁) ∈ V) |
34 | | retop 23516 |
. . . . . . 7
⊢
(topGen‘ran (,)) ∈ Top |
35 | 34 | fconst6 6568 |
. . . . . 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 2738 |
. . . . . . . . . . . 12
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
39 | 38 | cnfldtop 23538 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) ∈ Top |
40 | | cnrest2r 22040 |
. . . . . . . . . . 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 5879 |
. . . . . . . . . . . . 13
⊢ (𝐼 ⊆ (ℝ
↑m (1...𝑁))
→ ((𝑥 ∈ (ℝ
↑m (1...𝑁))
↦ (𝑥‘𝑛)) ↾ 𝐼) = (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛))) |
43 | 16, 42 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (ℝ
↑m (1...𝑁))
↦ (𝑥‘𝑛)) ↾ 𝐼) = (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) |
44 | 11 | toponunii 21669 |
. . . . . . . . . . . . . . 15
⊢ (ℝ
↑m (1...𝑁))
= ∪ 𝑅 |
45 | 44, 3 | ptpjcn 22364 |
. . . . . . . . . . . . . 14
⊢
(((1...𝑁) ∈ V
∧ ((1...𝑁) ×
{(topGen‘ran (,))}):(1...𝑁)⟶Top ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ (ℝ ↑m
(1...𝑁)) ↦ (𝑥‘𝑛)) ∈ (𝑅 Cn (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛))) |
46 | 8, 35, 45 | mp3an12 1452 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (1...𝑁) → (𝑥 ∈ (ℝ ↑m
(1...𝑁)) ↦ (𝑥‘𝑛)) ∈ (𝑅 Cn (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛))) |
47 | 44 | cnrest 22038 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ (ℝ
↑m (1...𝑁))
↦ (𝑥‘𝑛)) ∈ (𝑅 Cn (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)) ∧
𝐼 ⊆ (ℝ
↑m (1...𝑁))) → ((𝑥 ∈ (ℝ ↑m
(1...𝑁)) ↦ (𝑥‘𝑛)) ↾ 𝐼) ∈ ((𝑅 ↾t 𝐼) Cn (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛))) |
48 | 46, 16, 47 | sylancl 589 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (1...𝑁) → ((𝑥 ∈ (ℝ ↑m
(1...𝑁)) ↦ (𝑥‘𝑛)) ↾ 𝐼) ∈ ((𝑅 ↾t 𝐼) Cn (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛))) |
49 | 43, 48 | eqeltrrid 2838 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (1...𝑁) → (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) ∈ ((𝑅 ↾t 𝐼) Cn (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛))) |
50 | | fvex 6689 |
. . . . . . . . . . . . . 14
⊢
(topGen‘ran (,)) ∈ V |
51 | 50 | fvconst2 6978 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) =
(topGen‘ran (,))) |
52 | 38 | tgioo2 23557 |
. . . . . . . . . . . . 13
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
53 | 51, 52 | eqtrdi 2789 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) =
((TopOpen‘ℂfld) ↾t
ℝ)) |
54 | 53 | oveq2d 7188 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (1...𝑁) → ((𝑅 ↾t 𝐼) Cn (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)) = ((𝑅 ↾t 𝐼) Cn
((TopOpen‘ℂfld) ↾t
ℝ))) |
55 | 49, 54 | eleqtrd 2835 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (1...𝑁) → (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) ∈ ((𝑅 ↾t 𝐼) Cn ((TopOpen‘ℂfld)
↾t ℝ))) |
56 | 41, 55 | sseldi 3875 |
. . . . . . . . 9
⊢ (𝑛 ∈ (1...𝑁) → (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) ∈ ((𝑅 ↾t 𝐼) Cn
(TopOpen‘ℂfld))) |
57 | 56 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) ∈ ((𝑅 ↾t 𝐼) Cn
(TopOpen‘ℂfld))) |
58 | 21 | feqmptd 6739 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐼 ↦ (𝐹‘𝑥))) |
59 | 58, 7 | eqeltrrd 2834 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝐹‘𝑥)) ∈ ((𝑅 ↾t 𝐼) Cn (𝑅 ↾t 𝐼))) |
60 | 59 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ (𝐹‘𝑥)) ∈ ((𝑅 ↾t 𝐼) Cn (𝑅 ↾t 𝐼))) |
61 | | fveq1 6675 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (𝑥‘𝑛) = (𝑧‘𝑛)) |
62 | 61 | cbvmptv 5133 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐼 ↦ (𝑥‘𝑛)) = (𝑧 ∈ 𝐼 ↦ (𝑧‘𝑛)) |
63 | 62, 57 | eqeltrrid 2838 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑧 ∈ 𝐼 ↦ (𝑧‘𝑛)) ∈ ((𝑅 ↾t 𝐼) Cn
(TopOpen‘ℂfld))) |
64 | | fveq1 6675 |
. . . . . . . . 9
⊢ (𝑧 = (𝐹‘𝑥) → (𝑧‘𝑛) = ((𝐹‘𝑥)‘𝑛)) |
65 | 37, 60, 37, 63, 64 | cnmpt11 22416 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥)‘𝑛)) ∈ ((𝑅 ↾t 𝐼) Cn
(TopOpen‘ℂfld))) |
66 | 38 | subcn 23620 |
. . . . . . . . 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 22419 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾t 𝐼) Cn
(TopOpen‘ℂfld))) |
69 | | elmapi 8461 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ((0[,]1)
↑m (1...𝑁))
→ 𝑥:(1...𝑁)⟶(0[,]1)) |
70 | 69, 2 | eleq2s 2851 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐼 → 𝑥:(1...𝑁)⟶(0[,]1)) |
71 | 70 | ffvelrnda 6863 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐼 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥‘𝑛) ∈ (0[,]1)) |
72 | 13, 71 | sseldi 3875 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐼 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥‘𝑛) ∈ ℝ) |
73 | 72 | adantll 714 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑥‘𝑛) ∈ ℝ) |
74 | | elmapi 8461 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑥) ∈ ((0[,]1) ↑m
(1...𝑁)) → (𝐹‘𝑥):(1...𝑁)⟶(0[,]1)) |
75 | 74, 2 | eleq2s 2851 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑥) ∈ 𝐼 → (𝐹‘𝑥):(1...𝑁)⟶(0[,]1)) |
76 | 22, 75 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥):(1...𝑁)⟶(0[,]1)) |
77 | 76 | ffvelrnda 6863 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑥)‘𝑛) ∈ (0[,]1)) |
78 | 13, 77 | sseldi 3875 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑥)‘𝑛) ∈ ℝ) |
79 | 73, 78 | resubcld 11148 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛)) ∈ ℝ) |
80 | 79 | an32s 652 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐼) → ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛)) ∈ ℝ) |
81 | 80 | fmpttd 6891 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))):𝐼⟶ℝ) |
82 | | frn 6511 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))):𝐼⟶ℝ → ran (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ⊆ ℝ) |
83 | 38 | cnfldtopon 23537 |
. . . . . . . . 9
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
84 | | ax-resscn 10674 |
. . . . . . . . 9
⊢ ℝ
⊆ ℂ |
85 | | cnrest2 22039 |
. . . . . . . . 9
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ ran (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ⊆ ℝ ∧ ℝ ⊆
ℂ) → ((𝑥 ∈
𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾t 𝐼) Cn (TopOpen‘ℂfld))
↔ (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾t 𝐼) Cn ((TopOpen‘ℂfld)
↾t ℝ)))) |
86 | 83, 84, 85 | mp3an13 1453 |
. . . . . . . 8
⊢ (ran
(𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ⊆ ℝ → ((𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾t 𝐼) Cn (TopOpen‘ℂfld))
↔ (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾t 𝐼) Cn ((TopOpen‘ℂfld)
↾t ℝ)))) |
87 | 81, 82, 86 | 3syl 18 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾t 𝐼) Cn (TopOpen‘ℂfld))
↔ (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾t 𝐼) Cn ((TopOpen‘ℂfld)
↾t ℝ)))) |
88 | 68, 87 | mpbid 235 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾t 𝐼) Cn ((TopOpen‘ℂfld)
↾t ℝ))) |
89 | 54 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑅 ↾t 𝐼) Cn (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)) = ((𝑅 ↾t 𝐼) Cn
((TopOpen‘ℂfld) ↾t
ℝ))) |
90 | 88, 89 | eleqtrrd 2836 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐼 ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛))) ∈ ((𝑅 ↾t 𝐼) Cn (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛))) |
91 | 3, 32, 33, 36, 90 | ptcn 22380 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑥‘𝑛) − ((𝐹‘𝑥)‘𝑛)))) ∈ ((𝑅 ↾t 𝐼) Cn 𝑅)) |
92 | 31, 91 | eqeltrd 2833 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑥 ∘f − (𝐹‘𝑥))) ∈ ((𝑅 ↾t 𝐼) Cn 𝑅)) |
93 | | simpr2 1196 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → 𝑧 ∈ 𝐼) |
94 | | id 22 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → 𝑥 = 𝑧) |
95 | | fveq2 6676 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧)) |
96 | 94, 95 | oveq12d 7190 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑥 ∘f − (𝐹‘𝑥)) = (𝑧 ∘f − (𝐹‘𝑧))) |
97 | | eqid 2738 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐼 ↦ (𝑥 ∘f − (𝐹‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑥 ∘f − (𝐹‘𝑥))) |
98 | | ovex 7205 |
. . . . . . . 8
⊢ (𝑧 ∘f −
(𝐹‘𝑧)) ∈ V |
99 | 96, 97, 98 | fvmpt 6777 |
. . . . . . 7
⊢ (𝑧 ∈ 𝐼 → ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘f − (𝐹‘𝑥)))‘𝑧) = (𝑧 ∘f − (𝐹‘𝑧))) |
100 | 99 | fveq1d 6678 |
. . . . . 6
⊢ (𝑧 ∈ 𝐼 → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘f − (𝐹‘𝑥)))‘𝑧)‘𝑛) = ((𝑧 ∘f − (𝐹‘𝑧))‘𝑛)) |
101 | 93, 100 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘f − (𝐹‘𝑥)))‘𝑧)‘𝑛) = ((𝑧 ∘f − (𝐹‘𝑧))‘𝑛)) |
102 | | elmapfn 8477 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ((0[,]1)
↑m (1...𝑁))
→ 𝑧 Fn (1...𝑁)) |
103 | 102, 2 | eleq2s 2851 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝐼 → 𝑧 Fn (1...𝑁)) |
104 | 103 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) → 𝑧 Fn (1...𝑁)) |
105 | 21 | ffvelrnda 6863 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) ∈ 𝐼) |
106 | | elmapfn 8477 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑧) ∈ ((0[,]1) ↑m
(1...𝑁)) → (𝐹‘𝑧) Fn (1...𝑁)) |
107 | 106, 2 | eleq2s 2851 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑧) ∈ 𝐼 → (𝐹‘𝑧) Fn (1...𝑁)) |
108 | 105, 107 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) Fn (1...𝑁)) |
109 | 108 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) Fn (1...𝑁)) |
110 | | ovexd 7207 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) → (1...𝑁) ∈ V) |
111 | | simpllr 776 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑧‘𝑛) = 0) |
112 | | eqidd 2739 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) = ((𝐹‘𝑧)‘𝑛)) |
113 | 104, 109,
110, 110, 27, 111, 112 | ofval 7437 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑧 ∘f − (𝐹‘𝑧))‘𝑛) = (0 − ((𝐹‘𝑧)‘𝑛))) |
114 | | df-neg 10953 |
. . . . . . . . 9
⊢ -((𝐹‘𝑧)‘𝑛) = (0 − ((𝐹‘𝑧)‘𝑛)) |
115 | 113, 114 | eqtr4di 2791 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 0) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑧 ∘f − (𝐹‘𝑧))‘𝑛) = -((𝐹‘𝑧)‘𝑛)) |
116 | 115 | exp41 438 |
. . . . . . 7
⊢ (𝜑 → ((𝑧‘𝑛) = 0 → (𝑧 ∈ 𝐼 → (𝑛 ∈ (1...𝑁) → ((𝑧 ∘f − (𝐹‘𝑧))‘𝑛) = -((𝐹‘𝑧)‘𝑛))))) |
117 | 116 | com24 95 |
. . . . . 6
⊢ (𝜑 → (𝑛 ∈ (1...𝑁) → (𝑧 ∈ 𝐼 → ((𝑧‘𝑛) = 0 → ((𝑧 ∘f − (𝐹‘𝑧))‘𝑛) = -((𝐹‘𝑧)‘𝑛))))) |
118 | 117 | 3imp2 1350 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → ((𝑧 ∘f − (𝐹‘𝑧))‘𝑛) = -((𝐹‘𝑧)‘𝑛)) |
119 | 101, 118 | eqtrd 2773 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘f − (𝐹‘𝑥)))‘𝑧)‘𝑛) = -((𝐹‘𝑧)‘𝑛)) |
120 | | elmapi 8461 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑧) ∈ ((0[,]1) ↑m
(1...𝑁)) → (𝐹‘𝑧):(1...𝑁)⟶(0[,]1)) |
121 | 120, 2 | eleq2s 2851 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑧) ∈ 𝐼 → (𝐹‘𝑧):(1...𝑁)⟶(0[,]1)) |
122 | 105, 121 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧):(1...𝑁)⟶(0[,]1)) |
123 | 122 | ffvelrnda 6863 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) ∈ (0[,]1)) |
124 | | 0xr 10768 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ* |
125 | | 1xr 10780 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ* |
126 | | iccgelb 12879 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ* ∧ ((𝐹‘𝑧)‘𝑛) ∈ (0[,]1)) → 0 ≤ ((𝐹‘𝑧)‘𝑛)) |
127 | 124, 125,
126 | mp3an12 1452 |
. . . . . . . . 9
⊢ (((𝐹‘𝑧)‘𝑛) ∈ (0[,]1) → 0 ≤ ((𝐹‘𝑧)‘𝑛)) |
128 | 123, 127 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → 0 ≤ ((𝐹‘𝑧)‘𝑛)) |
129 | 13, 123 | sseldi 3875 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) ∈ ℝ) |
130 | 129 | le0neg2d 11292 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (0 ≤ ((𝐹‘𝑧)‘𝑛) ↔ -((𝐹‘𝑧)‘𝑛) ≤ 0)) |
131 | 128, 130 | mpbid 235 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → -((𝐹‘𝑧)‘𝑛) ≤ 0) |
132 | 131 | an32s 652 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑧 ∈ 𝐼) → -((𝐹‘𝑧)‘𝑛) ≤ 0) |
133 | 132 | anasss 470 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼)) → -((𝐹‘𝑧)‘𝑛) ≤ 0) |
134 | 133 | 3adantr3 1172 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → -((𝐹‘𝑧)‘𝑛) ≤ 0) |
135 | 119, 134 | eqbrtrd 5052 |
. . 3
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘f − (𝐹‘𝑥)))‘𝑧)‘𝑛) ≤ 0) |
136 | | iccleub 12878 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ* ∧ ((𝐹‘𝑧)‘𝑛) ∈ (0[,]1)) → ((𝐹‘𝑧)‘𝑛) ≤ 1) |
137 | 124, 125,
136 | mp3an12 1452 |
. . . . . . . . 9
⊢ (((𝐹‘𝑧)‘𝑛) ∈ (0[,]1) → ((𝐹‘𝑧)‘𝑛) ≤ 1) |
138 | 123, 137 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) ≤ 1) |
139 | | 1red 10722 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → 1 ∈ ℝ) |
140 | 139, 129 | subge0d 11310 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (0 ≤ (1 − ((𝐹‘𝑧)‘𝑛)) ↔ ((𝐹‘𝑧)‘𝑛) ≤ 1)) |
141 | 138, 140 | mpbird 260 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → 0 ≤ (1 − ((𝐹‘𝑧)‘𝑛))) |
142 | 141 | an32s 652 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑧 ∈ 𝐼) → 0 ≤ (1 − ((𝐹‘𝑧)‘𝑛))) |
143 | 142 | anasss 470 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼)) → 0 ≤ (1 − ((𝐹‘𝑧)‘𝑛))) |
144 | 143 | 3adantr3 1172 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → 0 ≤ (1 − ((𝐹‘𝑧)‘𝑛))) |
145 | | simpr2 1196 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → 𝑧 ∈ 𝐼) |
146 | 145, 100 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘f − (𝐹‘𝑥)))‘𝑧)‘𝑛) = ((𝑧 ∘f − (𝐹‘𝑧))‘𝑛)) |
147 | 103 | adantl 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) → 𝑧 Fn (1...𝑁)) |
148 | 108 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) Fn (1...𝑁)) |
149 | | ovexd 7207 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) → (1...𝑁) ∈ V) |
150 | | simpllr 776 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑧‘𝑛) = 1) |
151 | | eqidd 2739 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑧)‘𝑛) = ((𝐹‘𝑧)‘𝑛)) |
152 | 147, 148,
149, 149, 27, 150, 151 | ofval 7437 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑧‘𝑛) = 1) ∧ 𝑧 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑧 ∘f − (𝐹‘𝑧))‘𝑛) = (1 − ((𝐹‘𝑧)‘𝑛))) |
153 | 152 | exp41 438 |
. . . . . . 7
⊢ (𝜑 → ((𝑧‘𝑛) = 1 → (𝑧 ∈ 𝐼 → (𝑛 ∈ (1...𝑁) → ((𝑧 ∘f − (𝐹‘𝑧))‘𝑛) = (1 − ((𝐹‘𝑧)‘𝑛)))))) |
154 | 153 | com24 95 |
. . . . . 6
⊢ (𝜑 → (𝑛 ∈ (1...𝑁) → (𝑧 ∈ 𝐼 → ((𝑧‘𝑛) = 1 → ((𝑧 ∘f − (𝐹‘𝑧))‘𝑛) = (1 − ((𝐹‘𝑧)‘𝑛)))))) |
155 | 154 | 3imp2 1350 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → ((𝑧 ∘f − (𝐹‘𝑧))‘𝑛) = (1 − ((𝐹‘𝑧)‘𝑛))) |
156 | 146, 155 | eqtrd 2773 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘f − (𝐹‘𝑥)))‘𝑧)‘𝑛) = (1 − ((𝐹‘𝑧)‘𝑛))) |
157 | 144, 156 | breqtrrd 5058 |
. . 3
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → 0 ≤ (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘f − (𝐹‘𝑥)))‘𝑧)‘𝑛)) |
158 | 1, 2, 3, 92, 135, 157 | poimir 35455 |
. 2
⊢ (𝜑 → ∃𝑐 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘f − (𝐹‘𝑥)))‘𝑐) = ((1...𝑁) × {0})) |
159 | | id 22 |
. . . . . . . 8
⊢ (𝑥 = 𝑐 → 𝑥 = 𝑐) |
160 | | fveq2 6676 |
. . . . . . . 8
⊢ (𝑥 = 𝑐 → (𝐹‘𝑥) = (𝐹‘𝑐)) |
161 | 159, 160 | oveq12d 7190 |
. . . . . . 7
⊢ (𝑥 = 𝑐 → (𝑥 ∘f − (𝐹‘𝑥)) = (𝑐 ∘f − (𝐹‘𝑐))) |
162 | | ovex 7205 |
. . . . . . 7
⊢ (𝑐 ∘f −
(𝐹‘𝑐)) ∈ V |
163 | 161, 97, 162 | fvmpt 6777 |
. . . . . 6
⊢ (𝑐 ∈ 𝐼 → ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘f − (𝐹‘𝑥)))‘𝑐) = (𝑐 ∘f − (𝐹‘𝑐))) |
164 | 163 | adantl 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘f − (𝐹‘𝑥)))‘𝑐) = (𝑐 ∘f − (𝐹‘𝑐))) |
165 | 164 | eqeq1d 2740 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘f − (𝐹‘𝑥)))‘𝑐) = ((1...𝑁) × {0}) ↔ (𝑐 ∘f − (𝐹‘𝑐)) = ((1...𝑁) × {0}))) |
166 | | elmapfn 8477 |
. . . . . . . . . . 11
⊢ (𝑐 ∈ ((0[,]1)
↑m (1...𝑁))
→ 𝑐 Fn (1...𝑁)) |
167 | 166, 2 | eleq2s 2851 |
. . . . . . . . . 10
⊢ (𝑐 ∈ 𝐼 → 𝑐 Fn (1...𝑁)) |
168 | 167 | adantl 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → 𝑐 Fn (1...𝑁)) |
169 | 21 | ffvelrnda 6863 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝐹‘𝑐) ∈ 𝐼) |
170 | | elmapfn 8477 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑐) ∈ ((0[,]1) ↑m
(1...𝑁)) → (𝐹‘𝑐) Fn (1...𝑁)) |
171 | 170, 2 | eleq2s 2851 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑐) ∈ 𝐼 → (𝐹‘𝑐) Fn (1...𝑁)) |
172 | 169, 171 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝐹‘𝑐) Fn (1...𝑁)) |
173 | | ovexd 7207 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (1...𝑁) ∈ V) |
174 | | eqidd 2739 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑐‘𝑛) = (𝑐‘𝑛)) |
175 | | eqidd 2739 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑐)‘𝑛) = ((𝐹‘𝑐)‘𝑛)) |
176 | 168, 172,
173, 173, 27, 174, 175 | ofval 7437 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑐 ∘f − (𝐹‘𝑐))‘𝑛) = ((𝑐‘𝑛) − ((𝐹‘𝑐)‘𝑛))) |
177 | | c0ex 10715 |
. . . . . . . . . 10
⊢ 0 ∈
V |
178 | 177 | fvconst2 6978 |
. . . . . . . . 9
⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {0})‘𝑛) = 0) |
179 | 178 | adantl 485 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {0})‘𝑛) = 0) |
180 | 176, 179 | eqeq12d 2754 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (((𝑐 ∘f − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ ((𝑐‘𝑛) − ((𝐹‘𝑐)‘𝑛)) = 0)) |
181 | 13, 84 | sstri 3886 |
. . . . . . . . . 10
⊢ (0[,]1)
⊆ ℂ |
182 | | elmapi 8461 |
. . . . . . . . . . . 12
⊢ (𝑐 ∈ ((0[,]1)
↑m (1...𝑁))
→ 𝑐:(1...𝑁)⟶(0[,]1)) |
183 | 182, 2 | eleq2s 2851 |
. . . . . . . . . . 11
⊢ (𝑐 ∈ 𝐼 → 𝑐:(1...𝑁)⟶(0[,]1)) |
184 | 183 | ffvelrnda 6863 |
. . . . . . . . . 10
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑛 ∈ (1...𝑁)) → (𝑐‘𝑛) ∈ (0[,]1)) |
185 | 181, 184 | sseldi 3875 |
. . . . . . . . 9
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑛 ∈ (1...𝑁)) → (𝑐‘𝑛) ∈ ℂ) |
186 | 185 | adantll 714 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (𝑐‘𝑛) ∈ ℂ) |
187 | | elmapi 8461 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑐) ∈ ((0[,]1) ↑m
(1...𝑁)) → (𝐹‘𝑐):(1...𝑁)⟶(0[,]1)) |
188 | 187, 2 | eleq2s 2851 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑐) ∈ 𝐼 → (𝐹‘𝑐):(1...𝑁)⟶(0[,]1)) |
189 | 169, 188 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝐹‘𝑐):(1...𝑁)⟶(0[,]1)) |
190 | 189 | ffvelrnda 6863 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑐)‘𝑛) ∈ (0[,]1)) |
191 | 181, 190 | sseldi 3875 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑐)‘𝑛) ∈ ℂ) |
192 | 186, 191 | subeq0ad 11087 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (((𝑐‘𝑛) − ((𝐹‘𝑐)‘𝑛)) = 0 ↔ (𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛))) |
193 | 180, 192 | bitrd 282 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑛 ∈ (1...𝑁)) → (((𝑐 ∘f − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ (𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛))) |
194 | 193 | ralbidva 3108 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (∀𝑛 ∈ (1...𝑁)((𝑐 ∘f − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ ∀𝑛 ∈ (1...𝑁)(𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛))) |
195 | 168, 172,
173, 173, 27 | offn 7439 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝑐 ∘f − (𝐹‘𝑐)) Fn (1...𝑁)) |
196 | | fnconstg 6566 |
. . . . . . 7
⊢ (0 ∈
V → ((1...𝑁) ×
{0}) Fn (1...𝑁)) |
197 | 177, 196 | ax-mp 5 |
. . . . . 6
⊢
((1...𝑁) ×
{0}) Fn (1...𝑁) |
198 | | eqfnfv 6811 |
. . . . . 6
⊢ (((𝑐 ∘f −
(𝐹‘𝑐)) Fn (1...𝑁) ∧ ((1...𝑁) × {0}) Fn (1...𝑁)) → ((𝑐 ∘f − (𝐹‘𝑐)) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)((𝑐 ∘f − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛))) |
199 | 195, 197,
198 | sylancl 589 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → ((𝑐 ∘f − (𝐹‘𝑐)) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)((𝑐 ∘f − (𝐹‘𝑐))‘𝑛) = (((1...𝑁) × {0})‘𝑛))) |
200 | | eqfnfv 6811 |
. . . . . 6
⊢ ((𝑐 Fn (1...𝑁) ∧ (𝐹‘𝑐) Fn (1...𝑁)) → (𝑐 = (𝐹‘𝑐) ↔ ∀𝑛 ∈ (1...𝑁)(𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛))) |
201 | 168, 172,
200 | syl2anc 587 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝑐 = (𝐹‘𝑐) ↔ ∀𝑛 ∈ (1...𝑁)(𝑐‘𝑛) = ((𝐹‘𝑐)‘𝑛))) |
202 | 194, 199,
201 | 3bitr4d 314 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → ((𝑐 ∘f − (𝐹‘𝑐)) = ((1...𝑁) × {0}) ↔ 𝑐 = (𝐹‘𝑐))) |
203 | 165, 202 | bitrd 282 |
. . 3
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (((𝑥 ∈ 𝐼 ↦ (𝑥 ∘f − (𝐹‘𝑥)))‘𝑐) = ((1...𝑁) × {0}) ↔ 𝑐 = (𝐹‘𝑐))) |
204 | 203 | rexbidva 3206 |
. 2
⊢ (𝜑 → (∃𝑐 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ (𝑥 ∘f − (𝐹‘𝑥)))‘𝑐) = ((1...𝑁) × {0}) ↔ ∃𝑐 ∈ 𝐼 𝑐 = (𝐹‘𝑐))) |
205 | 158, 204 | mpbid 235 |
1
⊢ (𝜑 → ∃𝑐 ∈ 𝐼 𝑐 = (𝐹‘𝑐)) |