Step | Hyp | Ref
| Expression |
1 | | dv11cn.f |
. . . . 5
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) |
2 | 1 | ffnd 6292 |
. . . 4
⊢ (𝜑 → 𝐹 Fn 𝑋) |
3 | | dv11cn.g |
. . . . 5
⊢ (𝜑 → 𝐺:𝑋⟶ℂ) |
4 | 3 | ffnd 6292 |
. . . 4
⊢ (𝜑 → 𝐺 Fn 𝑋) |
5 | | dv11cn.x |
. . . . . 6
⊢ 𝑋 = (𝐴(ball‘(abs ∘ − ))𝑅) |
6 | | ovex 6954 |
. . . . . 6
⊢ (𝐴(ball‘(abs ∘ −
))𝑅) ∈
V |
7 | 5, 6 | eqeltri 2855 |
. . . . 5
⊢ 𝑋 ∈ V |
8 | 7 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ V) |
9 | | inidm 4043 |
. . . 4
⊢ (𝑋 ∩ 𝑋) = 𝑋 |
10 | 2, 4, 8, 8, 9 | offn 7185 |
. . 3
⊢ (𝜑 → (𝐹 ∘𝑓 − 𝐺) Fn 𝑋) |
11 | | 0cn 10368 |
. . . 4
⊢ 0 ∈
ℂ |
12 | | fnconstg 6343 |
. . . 4
⊢ (0 ∈
ℂ → (𝑋 ×
{0}) Fn 𝑋) |
13 | 11, 12 | mp1i 13 |
. . 3
⊢ (𝜑 → (𝑋 × {0}) Fn 𝑋) |
14 | | subcl 10621 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 − 𝑦) ∈ ℂ) |
15 | 14 | adantl 475 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 − 𝑦) ∈ ℂ) |
16 | 15, 1, 3, 8, 8, 9 | off 7189 |
. . . . . 6
⊢ (𝜑 → (𝐹 ∘𝑓 − 𝐺):𝑋⟶ℂ) |
17 | 16 | ffvelrnda 6623 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐹 ∘𝑓 − 𝐺)‘𝑥) ∈ ℂ) |
18 | | simpr 479 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
19 | | dv11cn.c |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ 𝑋) |
20 | 19 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ 𝑋) |
21 | 18, 20 | jca 507 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑥 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) |
22 | | cnxmet 22984 |
. . . . . . . . . . . 12
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
23 | 22 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs ∘ − )
∈ (∞Met‘ℂ)) |
24 | | dv11cn.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℂ) |
25 | | dv11cn.r |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈
ℝ*) |
26 | | blssm 22631 |
. . . . . . . . . . 11
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℝ*) → (𝐴(ball‘(abs ∘ −
))𝑅) ⊆
ℂ) |
27 | 23, 24, 25, 26 | syl3anc 1439 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴(ball‘(abs ∘ − ))𝑅) ⊆
ℂ) |
28 | 5, 27 | syl5eqss 3868 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ⊆ ℂ) |
29 | 1 | ffvelrnda 6623 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ ℂ) |
30 | 3 | ffvelrnda 6623 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐺‘𝑥) ∈ ℂ) |
31 | 1 | feqmptd 6509 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝑋 ↦ (𝐹‘𝑥))) |
32 | 3 | feqmptd 6509 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝑋 ↦ (𝐺‘𝑥))) |
33 | 8, 29, 30, 31, 32 | offval2 7191 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 ∘𝑓 − 𝐺) = (𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) − (𝐺‘𝑥)))) |
34 | 33 | oveq2d 6938 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℂ D (𝐹 ∘𝑓
− 𝐺)) = (ℂ D
(𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) − (𝐺‘𝑥))))) |
35 | | cnelprrecn 10365 |
. . . . . . . . . . . . . . 15
⊢ ℂ
∈ {ℝ, ℂ} |
36 | 35 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ℂ ∈ {ℝ,
ℂ}) |
37 | | fvexd 6461 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((ℂ D 𝐹)‘𝑥) ∈ V) |
38 | 31 | oveq2d 6938 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℂ D 𝐹) = (ℂ D (𝑥 ∈ 𝑋 ↦ (𝐹‘𝑥)))) |
39 | | dvfcn 24109 |
. . . . . . . . . . . . . . . . 17
⊢ (ℂ
D 𝐹):dom (ℂ D 𝐹)⟶ℂ |
40 | | dv11cn.d |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → dom (ℂ D 𝐹) = 𝑋) |
41 | 40 | feq2d 6277 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((ℂ D 𝐹):dom (ℂ D 𝐹)⟶ℂ ↔ (ℂ
D 𝐹):𝑋⟶ℂ)) |
42 | 39, 41 | mpbii 225 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ℂ D 𝐹):𝑋⟶ℂ) |
43 | 42 | feqmptd 6509 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℂ D 𝐹) = (𝑥 ∈ 𝑋 ↦ ((ℂ D 𝐹)‘𝑥))) |
44 | 38, 43 | eqtr3d 2816 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ℂ D (𝑥 ∈ 𝑋 ↦ (𝐹‘𝑥))) = (𝑥 ∈ 𝑋 ↦ ((ℂ D 𝐹)‘𝑥))) |
45 | | dv11cn.e |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℂ D 𝐹) = (ℂ D 𝐺)) |
46 | 32 | oveq2d 6938 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℂ D 𝐺) = (ℂ D (𝑥 ∈ 𝑋 ↦ (𝐺‘𝑥)))) |
47 | 45, 43, 46 | 3eqtr3rd 2823 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ℂ D (𝑥 ∈ 𝑋 ↦ (𝐺‘𝑥))) = (𝑥 ∈ 𝑋 ↦ ((ℂ D 𝐹)‘𝑥))) |
48 | 36, 29, 37, 44, 30, 37, 47 | dvmptsub 24167 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℂ D (𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) − (𝐺‘𝑥)))) = (𝑥 ∈ 𝑋 ↦ (((ℂ D 𝐹)‘𝑥) − ((ℂ D 𝐹)‘𝑥)))) |
49 | 42 | ffvelrnda 6623 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((ℂ D 𝐹)‘𝑥) ∈ ℂ) |
50 | 49 | subidd 10722 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((ℂ D 𝐹)‘𝑥) − ((ℂ D 𝐹)‘𝑥)) = 0) |
51 | 50 | mpteq2dva 4979 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (((ℂ D 𝐹)‘𝑥) − ((ℂ D 𝐹)‘𝑥))) = (𝑥 ∈ 𝑋 ↦ 0)) |
52 | | fconstmpt 5411 |
. . . . . . . . . . . . . 14
⊢ (𝑋 × {0}) = (𝑥 ∈ 𝑋 ↦ 0) |
53 | 51, 52 | syl6eqr 2832 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (((ℂ D 𝐹)‘𝑥) − ((ℂ D 𝐹)‘𝑥))) = (𝑋 × {0})) |
54 | 34, 48, 53 | 3eqtrd 2818 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℂ D (𝐹 ∘𝑓
− 𝐺)) = (𝑋 × {0})) |
55 | 54 | dmeqd 5571 |
. . . . . . . . . . 11
⊢ (𝜑 → dom (ℂ D (𝐹 ∘𝑓
− 𝐺)) = dom (𝑋 × {0})) |
56 | | snnzg 4541 |
. . . . . . . . . . . 12
⊢ (0 ∈
ℂ → {0} ≠ ∅) |
57 | | dmxp 5589 |
. . . . . . . . . . . 12
⊢ ({0} ≠
∅ → dom (𝑋
× {0}) = 𝑋) |
58 | 11, 56, 57 | mp2b 10 |
. . . . . . . . . . 11
⊢ dom
(𝑋 × {0}) = 𝑋 |
59 | 55, 58 | syl6eq 2830 |
. . . . . . . . . 10
⊢ (𝜑 → dom (ℂ D (𝐹 ∘𝑓
− 𝐺)) = 𝑋) |
60 | | eqimss2 3877 |
. . . . . . . . . 10
⊢ (dom
(ℂ D (𝐹
∘𝑓 − 𝐺)) = 𝑋 → 𝑋 ⊆ dom (ℂ D (𝐹 ∘𝑓 − 𝐺))) |
61 | 59, 60 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ⊆ dom (ℂ D (𝐹 ∘𝑓 − 𝐺))) |
62 | | 0red 10380 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
ℝ) |
63 | 54 | fveq1d 6448 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((ℂ D (𝐹 ∘𝑓
− 𝐺))‘𝑥) = ((𝑋 × {0})‘𝑥)) |
64 | | c0ex 10370 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
65 | 64 | fvconst2 6741 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑋 → ((𝑋 × {0})‘𝑥) = 0) |
66 | 63, 65 | sylan9eq 2834 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((ℂ D (𝐹 ∘𝑓 − 𝐺))‘𝑥) = 0) |
67 | 66 | abs00bd 14438 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (abs‘((ℂ D (𝐹 ∘𝑓
− 𝐺))‘𝑥)) = 0) |
68 | | 0le0 11483 |
. . . . . . . . . 10
⊢ 0 ≤
0 |
69 | 67, 68 | syl6eqbr 4925 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (abs‘((ℂ D (𝐹 ∘𝑓
− 𝐺))‘𝑥)) ≤ 0) |
70 | 28, 16, 24, 25, 5, 61, 62, 69 | dvlipcn 24194 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (abs‘(((𝐹 ∘𝑓 − 𝐺)‘𝑥) − ((𝐹 ∘𝑓 − 𝐺)‘𝐶))) ≤ (0 · (abs‘(𝑥 − 𝐶)))) |
71 | 21, 70 | syldan 585 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (abs‘(((𝐹 ∘𝑓 − 𝐺)‘𝑥) − ((𝐹 ∘𝑓 − 𝐺)‘𝐶))) ≤ (0 · (abs‘(𝑥 − 𝐶)))) |
72 | 33 | fveq1d 6448 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐹 ∘𝑓 − 𝐺)‘𝐶) = ((𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) − (𝐺‘𝑥)))‘𝐶)) |
73 | | fveq2 6446 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐶 → (𝐹‘𝑥) = (𝐹‘𝐶)) |
74 | | fveq2 6446 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐶 → (𝐺‘𝑥) = (𝐺‘𝐶)) |
75 | 73, 74 | oveq12d 6940 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐶 → ((𝐹‘𝑥) − (𝐺‘𝑥)) = ((𝐹‘𝐶) − (𝐺‘𝐶))) |
76 | | eqid 2778 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) − (𝐺‘𝑥))) = (𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) − (𝐺‘𝑥))) |
77 | | ovex 6954 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝐶) − (𝐺‘𝐶)) ∈ V |
78 | 75, 76, 77 | fvmpt 6542 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ 𝑋 → ((𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) − (𝐺‘𝑥)))‘𝐶) = ((𝐹‘𝐶) − (𝐺‘𝐶))) |
79 | 19, 78 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) − (𝐺‘𝑥)))‘𝐶) = ((𝐹‘𝐶) − (𝐺‘𝐶))) |
80 | 1, 19 | ffvelrnd 6624 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹‘𝐶) ∈ ℂ) |
81 | | dv11cn.p |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹‘𝐶) = (𝐺‘𝐶)) |
82 | 80, 81 | subeq0bd 10801 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐹‘𝐶) − (𝐺‘𝐶)) = 0) |
83 | 72, 79, 82 | 3eqtrd 2818 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐹 ∘𝑓 − 𝐺)‘𝐶) = 0) |
84 | 83 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐹 ∘𝑓 − 𝐺)‘𝐶) = 0) |
85 | 84 | oveq2d 6938 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((𝐹 ∘𝑓 − 𝐺)‘𝑥) − ((𝐹 ∘𝑓 − 𝐺)‘𝐶)) = (((𝐹 ∘𝑓 − 𝐺)‘𝑥) − 0)) |
86 | 17 | subid1d 10723 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((𝐹 ∘𝑓 − 𝐺)‘𝑥) − 0) = ((𝐹 ∘𝑓 − 𝐺)‘𝑥)) |
87 | 85, 86 | eqtrd 2814 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((𝐹 ∘𝑓 − 𝐺)‘𝑥) − ((𝐹 ∘𝑓 − 𝐺)‘𝐶)) = ((𝐹 ∘𝑓 − 𝐺)‘𝑥)) |
88 | 87 | fveq2d 6450 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (abs‘(((𝐹 ∘𝑓 − 𝐺)‘𝑥) − ((𝐹 ∘𝑓 − 𝐺)‘𝐶))) = (abs‘((𝐹 ∘𝑓 − 𝐺)‘𝑥))) |
89 | 28 | sselda 3821 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ℂ) |
90 | 28, 19 | sseldd 3822 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈ ℂ) |
91 | 90 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ ℂ) |
92 | 89, 91 | subcld 10734 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑥 − 𝐶) ∈ ℂ) |
93 | 92 | abscld 14583 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (abs‘(𝑥 − 𝐶)) ∈ ℝ) |
94 | 93 | recnd 10405 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (abs‘(𝑥 − 𝐶)) ∈ ℂ) |
95 | 94 | mul02d 10574 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (0 · (abs‘(𝑥 − 𝐶))) = 0) |
96 | 71, 88, 95 | 3brtr3d 4917 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (abs‘((𝐹 ∘𝑓 − 𝐺)‘𝑥)) ≤ 0) |
97 | 17 | absge0d 14591 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 0 ≤ (abs‘((𝐹 ∘𝑓
− 𝐺)‘𝑥))) |
98 | 17 | abscld 14583 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (abs‘((𝐹 ∘𝑓 − 𝐺)‘𝑥)) ∈ ℝ) |
99 | | 0re 10378 |
. . . . . . 7
⊢ 0 ∈
ℝ |
100 | | letri3 10462 |
. . . . . . 7
⊢
(((abs‘((𝐹
∘𝑓 − 𝐺)‘𝑥)) ∈ ℝ ∧ 0 ∈ ℝ)
→ ((abs‘((𝐹
∘𝑓 − 𝐺)‘𝑥)) = 0 ↔ ((abs‘((𝐹 ∘𝑓 − 𝐺)‘𝑥)) ≤ 0 ∧ 0 ≤ (abs‘((𝐹 ∘𝑓
− 𝐺)‘𝑥))))) |
101 | 98, 99, 100 | sylancl 580 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((abs‘((𝐹 ∘𝑓 − 𝐺)‘𝑥)) = 0 ↔ ((abs‘((𝐹 ∘𝑓 − 𝐺)‘𝑥)) ≤ 0 ∧ 0 ≤ (abs‘((𝐹 ∘𝑓
− 𝐺)‘𝑥))))) |
102 | 96, 97, 101 | mpbir2and 703 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (abs‘((𝐹 ∘𝑓 − 𝐺)‘𝑥)) = 0) |
103 | 17, 102 | abs00d 14593 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐹 ∘𝑓 − 𝐺)‘𝑥) = 0) |
104 | 65 | adantl 475 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑋 × {0})‘𝑥) = 0) |
105 | 103, 104 | eqtr4d 2817 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐹 ∘𝑓 − 𝐺)‘𝑥) = ((𝑋 × {0})‘𝑥)) |
106 | 10, 13, 105 | eqfnfvd 6577 |
. 2
⊢ (𝜑 → (𝐹 ∘𝑓 − 𝐺) = (𝑋 × {0})) |
107 | | ofsubeq0 11371 |
. . 3
⊢ ((𝑋 ∈ V ∧ 𝐹:𝑋⟶ℂ ∧ 𝐺:𝑋⟶ℂ) → ((𝐹 ∘𝑓 − 𝐺) = (𝑋 × {0}) ↔ 𝐹 = 𝐺)) |
108 | 8, 1, 3, 107 | syl3anc 1439 |
. 2
⊢ (𝜑 → ((𝐹 ∘𝑓 − 𝐺) = (𝑋 × {0}) ↔ 𝐹 = 𝐺)) |
109 | 106, 108 | mpbid 224 |
1
⊢ (𝜑 → 𝐹 = 𝐺) |