Step | Hyp | Ref
| Expression |
1 | | ax-resscn 7825 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
2 | | fss 5332 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶ℝ ∧ ℝ ⊆
ℂ) → 𝐹:𝐴⟶ℂ) |
3 | 1, 2 | mpan2 422 |
. . . . . 6
⊢ (𝐹:𝐴⟶ℝ → 𝐹:𝐴⟶ℂ) |
4 | 3 | adantr 274 |
. . . . 5
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → 𝐹:𝐴⟶ℂ) |
5 | | ffdm 5341 |
. . . . . 6
⊢ (𝐹:𝐴⟶ℂ → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ 𝐴)) |
6 | 5 | simpld 111 |
. . . . 5
⊢ (𝐹:𝐴⟶ℂ → 𝐹:dom 𝐹⟶ℂ) |
7 | 4, 6 | syl 14 |
. . . 4
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → 𝐹:dom 𝐹⟶ℂ) |
8 | | simpl 108 |
. . . . . 6
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → 𝐹:𝐴⟶ℝ) |
9 | 8 | fdmd 5327 |
. . . . 5
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → dom 𝐹 = 𝐴) |
10 | | simpr 109 |
. . . . 5
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → 𝐴 ⊆ ℝ) |
11 | 9, 10 | eqsstrd 3164 |
. . . 4
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → dom 𝐹 ⊆
ℝ) |
12 | | cnex 7857 |
. . . . 5
⊢ ℂ
∈ V |
13 | | reex 7867 |
. . . . 5
⊢ ℝ
∈ V |
14 | 12, 13 | elpm2 6626 |
. . . 4
⊢ (𝐹 ∈ (ℂ
↑pm ℝ) ↔ (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℝ)) |
15 | 7, 11, 14 | sylanbrc 414 |
. . 3
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → 𝐹 ∈ (ℂ ↑pm
ℝ)) |
16 | | dvfpm 13100 |
. . 3
⊢ (𝐹 ∈ (ℂ
↑pm ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ) |
17 | | ffn 5320 |
. . 3
⊢ ((ℝ
D 𝐹):dom (ℝ D 𝐹)⟶ℂ → (ℝ
D 𝐹) Fn dom (ℝ D
𝐹)) |
18 | 15, 16, 17 | 3syl 17 |
. 2
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → (ℝ D 𝐹) Fn dom (ℝ D 𝐹)) |
19 | 15, 16 | syl 14 |
. . . . 5
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ) |
20 | 19 | ffvelrnda 5603 |
. . . 4
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ dom (ℝ D 𝐹)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ) |
21 | | fvco3 5540 |
. . . . . 6
⊢
(((ℝ D 𝐹):dom
(ℝ D 𝐹)⟶ℂ ∧ 𝑥 ∈ dom (ℝ D 𝐹)) → ((∗ ∘ (ℝ D
𝐹))‘𝑥) = (∗‘((ℝ D
𝐹)‘𝑥))) |
22 | 19, 21 | sylan 281 |
. . . . 5
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ dom (ℝ D 𝐹)) → ((∗ ∘ (ℝ D
𝐹))‘𝑥) = (∗‘((ℝ D
𝐹)‘𝑥))) |
23 | | dvcj 13115 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) → (ℝ D
(∗ ∘ 𝐹)) =
(∗ ∘ (ℝ D 𝐹))) |
24 | 3, 23 | sylan 281 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → (ℝ D
(∗ ∘ 𝐹)) =
(∗ ∘ (ℝ D 𝐹))) |
25 | | ffvelrn 5601 |
. . . . . . . . . . . . 13
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ ℝ) |
26 | 25 | adantlr 469 |
. . . . . . . . . . . 12
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ ℝ) |
27 | 26 | cjred 10875 |
. . . . . . . . . . 11
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ 𝑦 ∈ 𝐴) → (∗‘(𝐹‘𝑦)) = (𝐹‘𝑦)) |
28 | 27 | mpteq2dva 4055 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → (𝑦 ∈ 𝐴 ↦ (∗‘(𝐹‘𝑦))) = (𝑦 ∈ 𝐴 ↦ (𝐹‘𝑦))) |
29 | 26 | recnd 7907 |
. . . . . . . . . . 11
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ ℂ) |
30 | 8 | feqmptd 5522 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → 𝐹 = (𝑦 ∈ 𝐴 ↦ (𝐹‘𝑦))) |
31 | | cjf 10751 |
. . . . . . . . . . . . 13
⊢
∗:ℂ⟶ℂ |
32 | 31 | a1i 9 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) →
∗:ℂ⟶ℂ) |
33 | 32 | feqmptd 5522 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → ∗ = (𝑧 ∈ ℂ ↦
(∗‘𝑧))) |
34 | | fveq2 5469 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝐹‘𝑦) → (∗‘𝑧) = (∗‘(𝐹‘𝑦))) |
35 | 29, 30, 33, 34 | fmptco 5634 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → (∗ ∘
𝐹) = (𝑦 ∈ 𝐴 ↦ (∗‘(𝐹‘𝑦)))) |
36 | 28, 35, 30 | 3eqtr4d 2200 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → (∗ ∘
𝐹) = 𝐹) |
37 | 36 | oveq2d 5841 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → (ℝ D
(∗ ∘ 𝐹)) =
(ℝ D 𝐹)) |
38 | 24, 37 | eqtr3d 2192 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → (∗ ∘
(ℝ D 𝐹)) = (ℝ D
𝐹)) |
39 | 38 | fveq1d 5471 |
. . . . . 6
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → ((∗ ∘
(ℝ D 𝐹))‘𝑥) = ((ℝ D 𝐹)‘𝑥)) |
40 | 39 | adantr 274 |
. . . . 5
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ dom (ℝ D 𝐹)) → ((∗ ∘ (ℝ D
𝐹))‘𝑥) = ((ℝ D 𝐹)‘𝑥)) |
41 | 22, 40 | eqtr3d 2192 |
. . . 4
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ dom (ℝ D 𝐹)) → (∗‘((ℝ D 𝐹)‘𝑥)) = ((ℝ D 𝐹)‘𝑥)) |
42 | 20, 41 | cjrebd 10850 |
. . 3
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ dom (ℝ D 𝐹)) → ((ℝ D 𝐹)‘𝑥) ∈ ℝ) |
43 | 42 | ralrimiva 2530 |
. 2
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → ∀𝑥 ∈ dom (ℝ D 𝐹)((ℝ D 𝐹)‘𝑥) ∈ ℝ) |
44 | | ffnfv 5626 |
. 2
⊢ ((ℝ
D 𝐹):dom (ℝ D 𝐹)⟶ℝ ↔
((ℝ D 𝐹) Fn dom
(ℝ D 𝐹) ∧
∀𝑥 ∈ dom
(ℝ D 𝐹)((ℝ D
𝐹)‘𝑥) ∈ ℝ)) |
45 | 18, 43, 44 | sylanbrc 414 |
1
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |