Step | Hyp | Ref
| Expression |
1 | | dv11cn.f |
. . . . 5
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) |
2 | | ffn 5958 |
. . . . 5
⊢ (𝐹:𝑋⟶ℂ → 𝐹 Fn 𝑋) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐹 Fn 𝑋) |
4 | | dv11cn.g |
. . . . 5
⊢ (𝜑 → 𝐺:𝑋⟶ℂ) |
5 | | ffn 5958 |
. . . . 5
⊢ (𝐺:𝑋⟶ℂ → 𝐺 Fn 𝑋) |
6 | 4, 5 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐺 Fn 𝑋) |
7 | | dv11cn.x |
. . . . . 6
⊢ 𝑋 = (𝐴(ball‘(abs ∘ − ))𝑅) |
8 | | ovex 6577 |
. . . . . 6
⊢ (𝐴(ball‘(abs ∘ −
))𝑅) ∈
V |
9 | 7, 8 | eqeltri 2684 |
. . . . 5
⊢ 𝑋 ∈ V |
10 | 9 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ V) |
11 | | inidm 3784 |
. . . 4
⊢ (𝑋 ∩ 𝑋) = 𝑋 |
12 | 3, 6, 10, 10, 11 | offn 6806 |
. . 3
⊢ (𝜑 → (𝐹 ∘𝑓 − 𝐺) Fn 𝑋) |
13 | | 0cn 9911 |
. . . 4
⊢ 0 ∈
ℂ |
14 | | fnconstg 6006 |
. . . 4
⊢ (0 ∈
ℂ → (𝑋 ×
{0}) Fn 𝑋) |
15 | 13, 14 | mp1i 13 |
. . 3
⊢ (𝜑 → (𝑋 × {0}) Fn 𝑋) |
16 | | subcl 10159 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 − 𝑦) ∈ ℂ) |
17 | 16 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 − 𝑦) ∈ ℂ) |
18 | 17, 1, 4, 10, 10, 11 | off 6810 |
. . . . . 6
⊢ (𝜑 → (𝐹 ∘𝑓 − 𝐺):𝑋⟶ℂ) |
19 | 18 | ffvelrnda 6267 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐹 ∘𝑓 − 𝐺)‘𝑥) ∈ ℂ) |
20 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
21 | | dv11cn.c |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ 𝑋) |
22 | 21 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ 𝑋) |
23 | 20, 22 | jca 553 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑥 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) |
24 | | cnxmet 22386 |
. . . . . . . . . . . 12
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
25 | 24 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs ∘ − )
∈ (∞Met‘ℂ)) |
26 | | dv11cn.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℂ) |
27 | | dv11cn.r |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈
ℝ*) |
28 | | blssm 22033 |
. . . . . . . . . . 11
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℝ*) → (𝐴(ball‘(abs ∘ −
))𝑅) ⊆
ℂ) |
29 | 25, 26, 27, 28 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴(ball‘(abs ∘ − ))𝑅) ⊆
ℂ) |
30 | 7, 29 | syl5eqss 3612 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ⊆ ℂ) |
31 | 1 | ffvelrnda 6267 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ ℂ) |
32 | 4 | ffvelrnda 6267 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐺‘𝑥) ∈ ℂ) |
33 | 1 | feqmptd 6159 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝑋 ↦ (𝐹‘𝑥))) |
34 | 4 | feqmptd 6159 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝑋 ↦ (𝐺‘𝑥))) |
35 | 10, 31, 32, 33, 34 | offval2 6812 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 ∘𝑓 − 𝐺) = (𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) − (𝐺‘𝑥)))) |
36 | 35 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℂ D (𝐹 ∘𝑓
− 𝐺)) = (ℂ D
(𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) − (𝐺‘𝑥))))) |
37 | | cnelprrecn 9908 |
. . . . . . . . . . . . . . 15
⊢ ℂ
∈ {ℝ, ℂ} |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ℂ ∈ {ℝ,
ℂ}) |
39 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢ ((ℂ
D 𝐹)‘𝑥) ∈ V |
40 | 39 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((ℂ D 𝐹)‘𝑥) ∈ V) |
41 | 33 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℂ D 𝐹) = (ℂ D (𝑥 ∈ 𝑋 ↦ (𝐹‘𝑥)))) |
42 | | dvfcn 23478 |
. . . . . . . . . . . . . . . . 17
⊢ (ℂ
D 𝐹):dom (ℂ D 𝐹)⟶ℂ |
43 | | dv11cn.d |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → dom (ℂ D 𝐹) = 𝑋) |
44 | 43 | feq2d 5944 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((ℂ D 𝐹):dom (ℂ D 𝐹)⟶ℂ ↔ (ℂ
D 𝐹):𝑋⟶ℂ)) |
45 | 42, 44 | mpbii 222 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ℂ D 𝐹):𝑋⟶ℂ) |
46 | 45 | feqmptd 6159 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℂ D 𝐹) = (𝑥 ∈ 𝑋 ↦ ((ℂ D 𝐹)‘𝑥))) |
47 | 41, 46 | eqtr3d 2646 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ℂ D (𝑥 ∈ 𝑋 ↦ (𝐹‘𝑥))) = (𝑥 ∈ 𝑋 ↦ ((ℂ D 𝐹)‘𝑥))) |
48 | | dv11cn.e |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℂ D 𝐹) = (ℂ D 𝐺)) |
49 | 34 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℂ D 𝐺) = (ℂ D (𝑥 ∈ 𝑋 ↦ (𝐺‘𝑥)))) |
50 | 48, 46, 49 | 3eqtr3rd 2653 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ℂ D (𝑥 ∈ 𝑋 ↦ (𝐺‘𝑥))) = (𝑥 ∈ 𝑋 ↦ ((ℂ D 𝐹)‘𝑥))) |
51 | 38, 31, 40, 47, 32, 40, 50 | dvmptsub 23536 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℂ D (𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) − (𝐺‘𝑥)))) = (𝑥 ∈ 𝑋 ↦ (((ℂ D 𝐹)‘𝑥) − ((ℂ D 𝐹)‘𝑥)))) |
52 | 45 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((ℂ D 𝐹)‘𝑥) ∈ ℂ) |
53 | 52 | subidd 10259 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((ℂ D 𝐹)‘𝑥) − ((ℂ D 𝐹)‘𝑥)) = 0) |
54 | 53 | mpteq2dva 4672 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (((ℂ D 𝐹)‘𝑥) − ((ℂ D 𝐹)‘𝑥))) = (𝑥 ∈ 𝑋 ↦ 0)) |
55 | | fconstmpt 5085 |
. . . . . . . . . . . . . 14
⊢ (𝑋 × {0}) = (𝑥 ∈ 𝑋 ↦ 0) |
56 | 54, 55 | syl6eqr 2662 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (((ℂ D 𝐹)‘𝑥) − ((ℂ D 𝐹)‘𝑥))) = (𝑋 × {0})) |
57 | 36, 51, 56 | 3eqtrd 2648 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℂ D (𝐹 ∘𝑓
− 𝐺)) = (𝑋 × {0})) |
58 | 57 | dmeqd 5248 |
. . . . . . . . . . 11
⊢ (𝜑 → dom (ℂ D (𝐹 ∘𝑓
− 𝐺)) = dom (𝑋 × {0})) |
59 | | snnzg 4251 |
. . . . . . . . . . . 12
⊢ (0 ∈
ℂ → {0} ≠ ∅) |
60 | | dmxp 5265 |
. . . . . . . . . . . 12
⊢ ({0} ≠
∅ → dom (𝑋
× {0}) = 𝑋) |
61 | 13, 59, 60 | mp2b 10 |
. . . . . . . . . . 11
⊢ dom
(𝑋 × {0}) = 𝑋 |
62 | 58, 61 | syl6eq 2660 |
. . . . . . . . . 10
⊢ (𝜑 → dom (ℂ D (𝐹 ∘𝑓
− 𝐺)) = 𝑋) |
63 | | eqimss2 3621 |
. . . . . . . . . 10
⊢ (dom
(ℂ D (𝐹
∘𝑓 − 𝐺)) = 𝑋 → 𝑋 ⊆ dom (ℂ D (𝐹 ∘𝑓 − 𝐺))) |
64 | 62, 63 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ⊆ dom (ℂ D (𝐹 ∘𝑓 − 𝐺))) |
65 | | 0red 9920 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
ℝ) |
66 | 57 | fveq1d 6105 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((ℂ D (𝐹 ∘𝑓
− 𝐺))‘𝑥) = ((𝑋 × {0})‘𝑥)) |
67 | | c0ex 9913 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
68 | 67 | fvconst2 6374 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑋 → ((𝑋 × {0})‘𝑥) = 0) |
69 | 66, 68 | sylan9eq 2664 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((ℂ D (𝐹 ∘𝑓 − 𝐺))‘𝑥) = 0) |
70 | 69 | abs00bd 13879 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (abs‘((ℂ D (𝐹 ∘𝑓
− 𝐺))‘𝑥)) = 0) |
71 | | 0le0 10987 |
. . . . . . . . . 10
⊢ 0 ≤
0 |
72 | 70, 71 | syl6eqbr 4622 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (abs‘((ℂ D (𝐹 ∘𝑓
− 𝐺))‘𝑥)) ≤ 0) |
73 | 30, 18, 26, 27, 7, 64, 65, 72 | dvlipcn 23561 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (abs‘(((𝐹 ∘𝑓 − 𝐺)‘𝑥) − ((𝐹 ∘𝑓 − 𝐺)‘𝐶))) ≤ (0 · (abs‘(𝑥 − 𝐶)))) |
74 | 23, 73 | syldan 486 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (abs‘(((𝐹 ∘𝑓 − 𝐺)‘𝑥) − ((𝐹 ∘𝑓 − 𝐺)‘𝐶))) ≤ (0 · (abs‘(𝑥 − 𝐶)))) |
75 | 35 | fveq1d 6105 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐹 ∘𝑓 − 𝐺)‘𝐶) = ((𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) − (𝐺‘𝑥)))‘𝐶)) |
76 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐶 → (𝐹‘𝑥) = (𝐹‘𝐶)) |
77 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐶 → (𝐺‘𝑥) = (𝐺‘𝐶)) |
78 | 76, 77 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐶 → ((𝐹‘𝑥) − (𝐺‘𝑥)) = ((𝐹‘𝐶) − (𝐺‘𝐶))) |
79 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) − (𝐺‘𝑥))) = (𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) − (𝐺‘𝑥))) |
80 | | ovex 6577 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝐶) − (𝐺‘𝐶)) ∈ V |
81 | 78, 79, 80 | fvmpt 6191 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ 𝑋 → ((𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) − (𝐺‘𝑥)))‘𝐶) = ((𝐹‘𝐶) − (𝐺‘𝐶))) |
82 | 21, 81 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) − (𝐺‘𝑥)))‘𝐶) = ((𝐹‘𝐶) − (𝐺‘𝐶))) |
83 | 1, 21 | ffvelrnd 6268 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹‘𝐶) ∈ ℂ) |
84 | | dv11cn.p |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹‘𝐶) = (𝐺‘𝐶)) |
85 | 83, 84 | subeq0bd 10335 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐹‘𝐶) − (𝐺‘𝐶)) = 0) |
86 | 75, 82, 85 | 3eqtrd 2648 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐹 ∘𝑓 − 𝐺)‘𝐶) = 0) |
87 | 86 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐹 ∘𝑓 − 𝐺)‘𝐶) = 0) |
88 | 87 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((𝐹 ∘𝑓 − 𝐺)‘𝑥) − ((𝐹 ∘𝑓 − 𝐺)‘𝐶)) = (((𝐹 ∘𝑓 − 𝐺)‘𝑥) − 0)) |
89 | 19 | subid1d 10260 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((𝐹 ∘𝑓 − 𝐺)‘𝑥) − 0) = ((𝐹 ∘𝑓 − 𝐺)‘𝑥)) |
90 | 88, 89 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((𝐹 ∘𝑓 − 𝐺)‘𝑥) − ((𝐹 ∘𝑓 − 𝐺)‘𝐶)) = ((𝐹 ∘𝑓 − 𝐺)‘𝑥)) |
91 | 90 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (abs‘(((𝐹 ∘𝑓 − 𝐺)‘𝑥) − ((𝐹 ∘𝑓 − 𝐺)‘𝐶))) = (abs‘((𝐹 ∘𝑓 − 𝐺)‘𝑥))) |
92 | 30 | sselda 3568 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ℂ) |
93 | 30, 21 | sseldd 3569 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈ ℂ) |
94 | 93 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ ℂ) |
95 | 92, 94 | subcld 10271 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑥 − 𝐶) ∈ ℂ) |
96 | 95 | abscld 14023 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (abs‘(𝑥 − 𝐶)) ∈ ℝ) |
97 | 96 | recnd 9947 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (abs‘(𝑥 − 𝐶)) ∈ ℂ) |
98 | 97 | mul02d 10113 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (0 · (abs‘(𝑥 − 𝐶))) = 0) |
99 | 74, 91, 98 | 3brtr3d 4614 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (abs‘((𝐹 ∘𝑓 − 𝐺)‘𝑥)) ≤ 0) |
100 | 19 | absge0d 14031 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 0 ≤ (abs‘((𝐹 ∘𝑓
− 𝐺)‘𝑥))) |
101 | 19 | abscld 14023 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (abs‘((𝐹 ∘𝑓 − 𝐺)‘𝑥)) ∈ ℝ) |
102 | | 0re 9919 |
. . . . . . 7
⊢ 0 ∈
ℝ |
103 | | letri3 10002 |
. . . . . . 7
⊢
(((abs‘((𝐹
∘𝑓 − 𝐺)‘𝑥)) ∈ ℝ ∧ 0 ∈ ℝ)
→ ((abs‘((𝐹
∘𝑓 − 𝐺)‘𝑥)) = 0 ↔ ((abs‘((𝐹 ∘𝑓 − 𝐺)‘𝑥)) ≤ 0 ∧ 0 ≤ (abs‘((𝐹 ∘𝑓
− 𝐺)‘𝑥))))) |
104 | 101, 102,
103 | sylancl 693 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((abs‘((𝐹 ∘𝑓 − 𝐺)‘𝑥)) = 0 ↔ ((abs‘((𝐹 ∘𝑓 − 𝐺)‘𝑥)) ≤ 0 ∧ 0 ≤ (abs‘((𝐹 ∘𝑓
− 𝐺)‘𝑥))))) |
105 | 99, 100, 104 | mpbir2and 959 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (abs‘((𝐹 ∘𝑓 − 𝐺)‘𝑥)) = 0) |
106 | 19, 105 | abs00d 14033 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐹 ∘𝑓 − 𝐺)‘𝑥) = 0) |
107 | 68 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑋 × {0})‘𝑥) = 0) |
108 | 106, 107 | eqtr4d 2647 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐹 ∘𝑓 − 𝐺)‘𝑥) = ((𝑋 × {0})‘𝑥)) |
109 | 12, 15, 108 | eqfnfvd 6222 |
. 2
⊢ (𝜑 → (𝐹 ∘𝑓 − 𝐺) = (𝑋 × {0})) |
110 | | ofsubeq0 10894 |
. . 3
⊢ ((𝑋 ∈ V ∧ 𝐹:𝑋⟶ℂ ∧ 𝐺:𝑋⟶ℂ) → ((𝐹 ∘𝑓 − 𝐺) = (𝑋 × {0}) ↔ 𝐹 = 𝐺)) |
111 | 10, 1, 4, 110 | syl3anc 1318 |
. 2
⊢ (𝜑 → ((𝐹 ∘𝑓 − 𝐺) = (𝑋 × {0}) ↔ 𝐹 = 𝐺)) |
112 | 109, 111 | mpbid 221 |
1
⊢ (𝜑 → 𝐹 = 𝐺) |