Step | Hyp | Ref
| Expression |
1 | | dv11cn.f |
. . . . 5
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) |
2 | | ffn 6045 |
. . . . 5
⊢ (𝐹:𝑋⟶ℂ → 𝐹 Fn 𝑋) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐹 Fn 𝑋) |
4 | | dv11cn.g |
. . . . 5
⊢ (𝜑 → 𝐺:𝑋⟶ℂ) |
5 | | ffn 6045 |
. . . . 5
⊢ (𝐺:𝑋⟶ℂ → 𝐺 Fn 𝑋) |
6 | 4, 5 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐺 Fn 𝑋) |
7 | | dv11cn.x |
. . . . . 6
⊢ 𝑋 = (𝐴(ball‘(abs ∘ − ))𝑅) |
8 | | ovex 6678 |
. . . . . 6
⊢ (𝐴(ball‘(abs ∘ −
))𝑅) ∈
V |
9 | 7, 8 | eqeltri 2697 |
. . . . 5
⊢ 𝑋 ∈ V |
10 | 9 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ V) |
11 | | inidm 3822 |
. . . 4
⊢ (𝑋 ∩ 𝑋) = 𝑋 |
12 | 3, 6, 10, 10, 11 | offn 6908 |
. . 3
⊢ (𝜑 → (𝐹 ∘𝑓 − 𝐺) Fn 𝑋) |
13 | | 0cn 10032 |
. . . 4
⊢ 0 ∈
ℂ |
14 | | fnconstg 6093 |
. . . 4
⊢ (0 ∈
ℂ → (𝑋 ×
{0}) Fn 𝑋) |
15 | 13, 14 | mp1i 13 |
. . 3
⊢ (𝜑 → (𝑋 × {0}) Fn 𝑋) |
16 | | subcl 10280 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 − 𝑦) ∈ ℂ) |
17 | 16 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 − 𝑦) ∈ ℂ) |
18 | 17, 1, 4, 10, 10, 11 | off 6912 |
. . . . . 6
⊢ (𝜑 → (𝐹 ∘𝑓 − 𝐺):𝑋⟶ℂ) |
19 | 18 | ffvelrnda 6359 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐹 ∘𝑓 − 𝐺)‘𝑥) ∈ ℂ) |
20 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
21 | | dv11cn.c |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ 𝑋) |
22 | 21 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ 𝑋) |
23 | 20, 22 | jca 554 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑥 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) |
24 | | cnxmet 22576 |
. . . . . . . . . . . 12
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
25 | 24 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs ∘ − )
∈ (∞Met‘ℂ)) |
26 | | dv11cn.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℂ) |
27 | | dv11cn.r |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈
ℝ*) |
28 | | blssm 22223 |
. . . . . . . . . . 11
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℝ*) → (𝐴(ball‘(abs ∘ −
))𝑅) ⊆
ℂ) |
29 | 25, 26, 27, 28 | syl3anc 1326 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴(ball‘(abs ∘ − ))𝑅) ⊆
ℂ) |
30 | 7, 29 | syl5eqss 3649 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ⊆ ℂ) |
31 | 1 | ffvelrnda 6359 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ ℂ) |
32 | 4 | ffvelrnda 6359 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐺‘𝑥) ∈ ℂ) |
33 | 1 | feqmptd 6249 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝑋 ↦ (𝐹‘𝑥))) |
34 | 4 | feqmptd 6249 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝑋 ↦ (𝐺‘𝑥))) |
35 | 10, 31, 32, 33, 34 | offval2 6914 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 ∘𝑓 − 𝐺) = (𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) − (𝐺‘𝑥)))) |
36 | 35 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℂ D (𝐹 ∘𝑓
− 𝐺)) = (ℂ D
(𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) − (𝐺‘𝑥))))) |
37 | | cnelprrecn 10029 |
. . . . . . . . . . . . . . 15
⊢ ℂ
∈ {ℝ, ℂ} |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ℂ ∈ {ℝ,
ℂ}) |
39 | | fvexd 6203 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((ℂ D 𝐹)‘𝑥) ∈ V) |
40 | 33 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℂ D 𝐹) = (ℂ D (𝑥 ∈ 𝑋 ↦ (𝐹‘𝑥)))) |
41 | | dvfcn 23672 |
. . . . . . . . . . . . . . . . 17
⊢ (ℂ
D 𝐹):dom (ℂ D 𝐹)⟶ℂ |
42 | | dv11cn.d |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → dom (ℂ D 𝐹) = 𝑋) |
43 | 42 | feq2d 6031 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((ℂ D 𝐹):dom (ℂ D 𝐹)⟶ℂ ↔ (ℂ
D 𝐹):𝑋⟶ℂ)) |
44 | 41, 43 | mpbii 223 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ℂ D 𝐹):𝑋⟶ℂ) |
45 | 44 | feqmptd 6249 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℂ D 𝐹) = (𝑥 ∈ 𝑋 ↦ ((ℂ D 𝐹)‘𝑥))) |
46 | 40, 45 | eqtr3d 2658 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ℂ D (𝑥 ∈ 𝑋 ↦ (𝐹‘𝑥))) = (𝑥 ∈ 𝑋 ↦ ((ℂ D 𝐹)‘𝑥))) |
47 | | dv11cn.e |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℂ D 𝐹) = (ℂ D 𝐺)) |
48 | 34 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℂ D 𝐺) = (ℂ D (𝑥 ∈ 𝑋 ↦ (𝐺‘𝑥)))) |
49 | 47, 45, 48 | 3eqtr3rd 2665 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ℂ D (𝑥 ∈ 𝑋 ↦ (𝐺‘𝑥))) = (𝑥 ∈ 𝑋 ↦ ((ℂ D 𝐹)‘𝑥))) |
50 | 38, 31, 39, 46, 32, 39, 49 | dvmptsub 23730 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℂ D (𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) − (𝐺‘𝑥)))) = (𝑥 ∈ 𝑋 ↦ (((ℂ D 𝐹)‘𝑥) − ((ℂ D 𝐹)‘𝑥)))) |
51 | 44 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((ℂ D 𝐹)‘𝑥) ∈ ℂ) |
52 | 51 | subidd 10380 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((ℂ D 𝐹)‘𝑥) − ((ℂ D 𝐹)‘𝑥)) = 0) |
53 | 52 | mpteq2dva 4744 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (((ℂ D 𝐹)‘𝑥) − ((ℂ D 𝐹)‘𝑥))) = (𝑥 ∈ 𝑋 ↦ 0)) |
54 | | fconstmpt 5163 |
. . . . . . . . . . . . . 14
⊢ (𝑋 × {0}) = (𝑥 ∈ 𝑋 ↦ 0) |
55 | 53, 54 | syl6eqr 2674 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (((ℂ D 𝐹)‘𝑥) − ((ℂ D 𝐹)‘𝑥))) = (𝑋 × {0})) |
56 | 36, 50, 55 | 3eqtrd 2660 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℂ D (𝐹 ∘𝑓
− 𝐺)) = (𝑋 × {0})) |
57 | 56 | dmeqd 5326 |
. . . . . . . . . . 11
⊢ (𝜑 → dom (ℂ D (𝐹 ∘𝑓
− 𝐺)) = dom (𝑋 × {0})) |
58 | | snnzg 4308 |
. . . . . . . . . . . 12
⊢ (0 ∈
ℂ → {0} ≠ ∅) |
59 | | dmxp 5344 |
. . . . . . . . . . . 12
⊢ ({0} ≠
∅ → dom (𝑋
× {0}) = 𝑋) |
60 | 13, 58, 59 | mp2b 10 |
. . . . . . . . . . 11
⊢ dom
(𝑋 × {0}) = 𝑋 |
61 | 57, 60 | syl6eq 2672 |
. . . . . . . . . 10
⊢ (𝜑 → dom (ℂ D (𝐹 ∘𝑓
− 𝐺)) = 𝑋) |
62 | | eqimss2 3658 |
. . . . . . . . . 10
⊢ (dom
(ℂ D (𝐹
∘𝑓 − 𝐺)) = 𝑋 → 𝑋 ⊆ dom (ℂ D (𝐹 ∘𝑓 − 𝐺))) |
63 | 61, 62 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ⊆ dom (ℂ D (𝐹 ∘𝑓 − 𝐺))) |
64 | | 0red 10041 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
ℝ) |
65 | 56 | fveq1d 6193 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((ℂ D (𝐹 ∘𝑓
− 𝐺))‘𝑥) = ((𝑋 × {0})‘𝑥)) |
66 | | c0ex 10034 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
67 | 66 | fvconst2 6469 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑋 → ((𝑋 × {0})‘𝑥) = 0) |
68 | 65, 67 | sylan9eq 2676 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((ℂ D (𝐹 ∘𝑓 − 𝐺))‘𝑥) = 0) |
69 | 68 | abs00bd 14031 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (abs‘((ℂ D (𝐹 ∘𝑓
− 𝐺))‘𝑥)) = 0) |
70 | | 0le0 11110 |
. . . . . . . . . 10
⊢ 0 ≤
0 |
71 | 69, 70 | syl6eqbr 4692 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (abs‘((ℂ D (𝐹 ∘𝑓
− 𝐺))‘𝑥)) ≤ 0) |
72 | 30, 18, 26, 27, 7, 63, 64, 71 | dvlipcn 23757 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (abs‘(((𝐹 ∘𝑓 − 𝐺)‘𝑥) − ((𝐹 ∘𝑓 − 𝐺)‘𝐶))) ≤ (0 · (abs‘(𝑥 − 𝐶)))) |
73 | 23, 72 | syldan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (abs‘(((𝐹 ∘𝑓 − 𝐺)‘𝑥) − ((𝐹 ∘𝑓 − 𝐺)‘𝐶))) ≤ (0 · (abs‘(𝑥 − 𝐶)))) |
74 | 35 | fveq1d 6193 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐹 ∘𝑓 − 𝐺)‘𝐶) = ((𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) − (𝐺‘𝑥)))‘𝐶)) |
75 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐶 → (𝐹‘𝑥) = (𝐹‘𝐶)) |
76 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐶 → (𝐺‘𝑥) = (𝐺‘𝐶)) |
77 | 75, 76 | oveq12d 6668 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐶 → ((𝐹‘𝑥) − (𝐺‘𝑥)) = ((𝐹‘𝐶) − (𝐺‘𝐶))) |
78 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) − (𝐺‘𝑥))) = (𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) − (𝐺‘𝑥))) |
79 | | ovex 6678 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝐶) − (𝐺‘𝐶)) ∈ V |
80 | 77, 78, 79 | fvmpt 6282 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ 𝑋 → ((𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) − (𝐺‘𝑥)))‘𝐶) = ((𝐹‘𝐶) − (𝐺‘𝐶))) |
81 | 21, 80 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) − (𝐺‘𝑥)))‘𝐶) = ((𝐹‘𝐶) − (𝐺‘𝐶))) |
82 | 1, 21 | ffvelrnd 6360 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹‘𝐶) ∈ ℂ) |
83 | | dv11cn.p |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹‘𝐶) = (𝐺‘𝐶)) |
84 | 82, 83 | subeq0bd 10456 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐹‘𝐶) − (𝐺‘𝐶)) = 0) |
85 | 74, 81, 84 | 3eqtrd 2660 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐹 ∘𝑓 − 𝐺)‘𝐶) = 0) |
86 | 85 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐹 ∘𝑓 − 𝐺)‘𝐶) = 0) |
87 | 86 | oveq2d 6666 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((𝐹 ∘𝑓 − 𝐺)‘𝑥) − ((𝐹 ∘𝑓 − 𝐺)‘𝐶)) = (((𝐹 ∘𝑓 − 𝐺)‘𝑥) − 0)) |
88 | 19 | subid1d 10381 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((𝐹 ∘𝑓 − 𝐺)‘𝑥) − 0) = ((𝐹 ∘𝑓 − 𝐺)‘𝑥)) |
89 | 87, 88 | eqtrd 2656 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((𝐹 ∘𝑓 − 𝐺)‘𝑥) − ((𝐹 ∘𝑓 − 𝐺)‘𝐶)) = ((𝐹 ∘𝑓 − 𝐺)‘𝑥)) |
90 | 89 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (abs‘(((𝐹 ∘𝑓 − 𝐺)‘𝑥) − ((𝐹 ∘𝑓 − 𝐺)‘𝐶))) = (abs‘((𝐹 ∘𝑓 − 𝐺)‘𝑥))) |
91 | 30 | sselda 3603 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ℂ) |
92 | 30, 21 | sseldd 3604 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈ ℂ) |
93 | 92 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ ℂ) |
94 | 91, 93 | subcld 10392 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑥 − 𝐶) ∈ ℂ) |
95 | 94 | abscld 14175 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (abs‘(𝑥 − 𝐶)) ∈ ℝ) |
96 | 95 | recnd 10068 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (abs‘(𝑥 − 𝐶)) ∈ ℂ) |
97 | 96 | mul02d 10234 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (0 · (abs‘(𝑥 − 𝐶))) = 0) |
98 | 73, 90, 97 | 3brtr3d 4684 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (abs‘((𝐹 ∘𝑓 − 𝐺)‘𝑥)) ≤ 0) |
99 | 19 | absge0d 14183 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 0 ≤ (abs‘((𝐹 ∘𝑓
− 𝐺)‘𝑥))) |
100 | 19 | abscld 14175 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (abs‘((𝐹 ∘𝑓 − 𝐺)‘𝑥)) ∈ ℝ) |
101 | | 0re 10040 |
. . . . . . 7
⊢ 0 ∈
ℝ |
102 | | letri3 10123 |
. . . . . . 7
⊢
(((abs‘((𝐹
∘𝑓 − 𝐺)‘𝑥)) ∈ ℝ ∧ 0 ∈ ℝ)
→ ((abs‘((𝐹
∘𝑓 − 𝐺)‘𝑥)) = 0 ↔ ((abs‘((𝐹 ∘𝑓 − 𝐺)‘𝑥)) ≤ 0 ∧ 0 ≤ (abs‘((𝐹 ∘𝑓
− 𝐺)‘𝑥))))) |
103 | 100, 101,
102 | sylancl 694 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((abs‘((𝐹 ∘𝑓 − 𝐺)‘𝑥)) = 0 ↔ ((abs‘((𝐹 ∘𝑓 − 𝐺)‘𝑥)) ≤ 0 ∧ 0 ≤ (abs‘((𝐹 ∘𝑓
− 𝐺)‘𝑥))))) |
104 | 98, 99, 103 | mpbir2and 957 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (abs‘((𝐹 ∘𝑓 − 𝐺)‘𝑥)) = 0) |
105 | 19, 104 | abs00d 14185 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐹 ∘𝑓 − 𝐺)‘𝑥) = 0) |
106 | 67 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑋 × {0})‘𝑥) = 0) |
107 | 105, 106 | eqtr4d 2659 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐹 ∘𝑓 − 𝐺)‘𝑥) = ((𝑋 × {0})‘𝑥)) |
108 | 12, 15, 107 | eqfnfvd 6314 |
. 2
⊢ (𝜑 → (𝐹 ∘𝑓 − 𝐺) = (𝑋 × {0})) |
109 | | ofsubeq0 11017 |
. . 3
⊢ ((𝑋 ∈ V ∧ 𝐹:𝑋⟶ℂ ∧ 𝐺:𝑋⟶ℂ) → ((𝐹 ∘𝑓 − 𝐺) = (𝑋 × {0}) ↔ 𝐹 = 𝐺)) |
110 | 10, 1, 4, 109 | syl3anc 1326 |
. 2
⊢ (𝜑 → ((𝐹 ∘𝑓 − 𝐺) = (𝑋 × {0}) ↔ 𝐹 = 𝐺)) |
111 | 108, 110 | mpbid 222 |
1
⊢ (𝜑 → 𝐹 = 𝐺) |