Step | Hyp | Ref
| Expression |
1 | | dvaddf.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
2 | | dvaddf.df |
. . . . 5
⊢ (𝜑 → dom (𝑆 D 𝐹) = 𝑋) |
3 | | dvbsss 23472 |
. . . . 5
⊢ dom
(𝑆 D 𝐹) ⊆ 𝑆 |
4 | 2, 3 | syl6eqssr 3619 |
. . . 4
⊢ (𝜑 → 𝑋 ⊆ 𝑆) |
5 | 1, 4 | ssexd 4733 |
. . 3
⊢ (𝜑 → 𝑋 ∈ V) |
6 | | dvfg 23476 |
. . . . . 6
⊢ (𝑆 ∈ {ℝ, ℂ}
→ (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ) |
7 | 1, 6 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ) |
8 | 2 | feq2d 5944 |
. . . . 5
⊢ (𝜑 → ((𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ ↔ (𝑆 D 𝐹):𝑋⟶ℂ)) |
9 | 7, 8 | mpbid 221 |
. . . 4
⊢ (𝜑 → (𝑆 D 𝐹):𝑋⟶ℂ) |
10 | | ffn 5958 |
. . . 4
⊢ ((𝑆 D 𝐹):𝑋⟶ℂ → (𝑆 D 𝐹) Fn 𝑋) |
11 | 9, 10 | syl 17 |
. . 3
⊢ (𝜑 → (𝑆 D 𝐹) Fn 𝑋) |
12 | | dvfg 23476 |
. . . . . 6
⊢ (𝑆 ∈ {ℝ, ℂ}
→ (𝑆 D 𝐺):dom (𝑆 D 𝐺)⟶ℂ) |
13 | 1, 12 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑆 D 𝐺):dom (𝑆 D 𝐺)⟶ℂ) |
14 | | dvaddf.dg |
. . . . . 6
⊢ (𝜑 → dom (𝑆 D 𝐺) = 𝑋) |
15 | 14 | feq2d 5944 |
. . . . 5
⊢ (𝜑 → ((𝑆 D 𝐺):dom (𝑆 D 𝐺)⟶ℂ ↔ (𝑆 D 𝐺):𝑋⟶ℂ)) |
16 | 13, 15 | mpbid 221 |
. . . 4
⊢ (𝜑 → (𝑆 D 𝐺):𝑋⟶ℂ) |
17 | | ffn 5958 |
. . . 4
⊢ ((𝑆 D 𝐺):𝑋⟶ℂ → (𝑆 D 𝐺) Fn 𝑋) |
18 | 16, 17 | syl 17 |
. . 3
⊢ (𝜑 → (𝑆 D 𝐺) Fn 𝑋) |
19 | | dvfg 23476 |
. . . . . 6
⊢ (𝑆 ∈ {ℝ, ℂ}
→ (𝑆 D (𝐹 ∘𝑓 +
𝐺)):dom (𝑆 D (𝐹 ∘𝑓 + 𝐺))⟶ℂ) |
20 | 1, 19 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑆 D (𝐹 ∘𝑓 + 𝐺)):dom (𝑆 D (𝐹 ∘𝑓 + 𝐺))⟶ℂ) |
21 | | recnprss 23474 |
. . . . . . . . 9
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
22 | 1, 21 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
23 | | addcl 9897 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + 𝑦) ∈ ℂ) |
24 | 23 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 + 𝑦) ∈ ℂ) |
25 | | dvaddf.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) |
26 | | dvaddf.g |
. . . . . . . . 9
⊢ (𝜑 → 𝐺:𝑋⟶ℂ) |
27 | | inidm 3784 |
. . . . . . . . 9
⊢ (𝑋 ∩ 𝑋) = 𝑋 |
28 | 24, 25, 26, 5, 5, 27 | off 6810 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺):𝑋⟶ℂ) |
29 | 22, 28, 4 | dvbss 23471 |
. . . . . . 7
⊢ (𝜑 → dom (𝑆 D (𝐹 ∘𝑓 + 𝐺)) ⊆ 𝑋) |
30 | 25 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐹:𝑋⟶ℂ) |
31 | 4 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑋 ⊆ 𝑆) |
32 | 26 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐺:𝑋⟶ℂ) |
33 | 22 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑆 ⊆ ℂ) |
34 | | fvex 6113 |
. . . . . . . . . . . 12
⊢ ((𝑆 D 𝐹)‘𝑥) ∈ V |
35 | 34 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑆 D 𝐹)‘𝑥) ∈ V) |
36 | | fvex 6113 |
. . . . . . . . . . . 12
⊢ ((𝑆 D 𝐺)‘𝑥) ∈ V |
37 | 36 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑆 D 𝐺)‘𝑥) ∈ V) |
38 | 2 | eleq2d 2673 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ dom (𝑆 D 𝐹) ↔ 𝑥 ∈ 𝑋)) |
39 | 38 | biimpar 501 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ dom (𝑆 D 𝐹)) |
40 | 1 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑆 ∈ {ℝ, ℂ}) |
41 | | ffun 5961 |
. . . . . . . . . . . . 13
⊢ ((𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ → Fun (𝑆 D 𝐹)) |
42 | | funfvbrb 6238 |
. . . . . . . . . . . . 13
⊢ (Fun
(𝑆 D 𝐹) → (𝑥 ∈ dom (𝑆 D 𝐹) ↔ 𝑥(𝑆 D 𝐹)((𝑆 D 𝐹)‘𝑥))) |
43 | 40, 6, 41, 42 | 4syl 19 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑥 ∈ dom (𝑆 D 𝐹) ↔ 𝑥(𝑆 D 𝐹)((𝑆 D 𝐹)‘𝑥))) |
44 | 39, 43 | mpbid 221 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥(𝑆 D 𝐹)((𝑆 D 𝐹)‘𝑥)) |
45 | 14 | eleq2d 2673 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ dom (𝑆 D 𝐺) ↔ 𝑥 ∈ 𝑋)) |
46 | 45 | biimpar 501 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ dom (𝑆 D 𝐺)) |
47 | | ffun 5961 |
. . . . . . . . . . . . 13
⊢ ((𝑆 D 𝐺):dom (𝑆 D 𝐺)⟶ℂ → Fun (𝑆 D 𝐺)) |
48 | | funfvbrb 6238 |
. . . . . . . . . . . . 13
⊢ (Fun
(𝑆 D 𝐺) → (𝑥 ∈ dom (𝑆 D 𝐺) ↔ 𝑥(𝑆 D 𝐺)((𝑆 D 𝐺)‘𝑥))) |
49 | 40, 12, 47, 48 | 4syl 19 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑥 ∈ dom (𝑆 D 𝐺) ↔ 𝑥(𝑆 D 𝐺)((𝑆 D 𝐺)‘𝑥))) |
50 | 46, 49 | mpbid 221 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥(𝑆 D 𝐺)((𝑆 D 𝐺)‘𝑥)) |
51 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
52 | 30, 31, 32, 31, 33, 35, 37, 44, 50, 51 | dvaddbr 23507 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥(𝑆 D (𝐹 ∘𝑓 + 𝐺))(((𝑆 D 𝐹)‘𝑥) + ((𝑆 D 𝐺)‘𝑥))) |
53 | | reldv 23440 |
. . . . . . . . . . 11
⊢ Rel
(𝑆 D (𝐹 ∘𝑓 + 𝐺)) |
54 | 53 | releldmi 5283 |
. . . . . . . . . 10
⊢ (𝑥(𝑆 D (𝐹 ∘𝑓 + 𝐺))(((𝑆 D 𝐹)‘𝑥) + ((𝑆 D 𝐺)‘𝑥)) → 𝑥 ∈ dom (𝑆 D (𝐹 ∘𝑓 + 𝐺))) |
55 | 52, 54 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ dom (𝑆 D (𝐹 ∘𝑓 + 𝐺))) |
56 | 55 | ex 449 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝑋 → 𝑥 ∈ dom (𝑆 D (𝐹 ∘𝑓 + 𝐺)))) |
57 | 56 | ssrdv 3574 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ⊆ dom (𝑆 D (𝐹 ∘𝑓 + 𝐺))) |
58 | 29, 57 | eqssd 3585 |
. . . . . 6
⊢ (𝜑 → dom (𝑆 D (𝐹 ∘𝑓 + 𝐺)) = 𝑋) |
59 | 58 | feq2d 5944 |
. . . . 5
⊢ (𝜑 → ((𝑆 D (𝐹 ∘𝑓 + 𝐺)):dom (𝑆 D (𝐹 ∘𝑓 + 𝐺))⟶ℂ ↔ (𝑆 D (𝐹 ∘𝑓 + 𝐺)):𝑋⟶ℂ)) |
60 | 20, 59 | mpbid 221 |
. . . 4
⊢ (𝜑 → (𝑆 D (𝐹 ∘𝑓 + 𝐺)):𝑋⟶ℂ) |
61 | | ffn 5958 |
. . . 4
⊢ ((𝑆 D (𝐹 ∘𝑓 + 𝐺)):𝑋⟶ℂ → (𝑆 D (𝐹 ∘𝑓 + 𝐺)) Fn 𝑋) |
62 | 60, 61 | syl 17 |
. . 3
⊢ (𝜑 → (𝑆 D (𝐹 ∘𝑓 + 𝐺)) Fn 𝑋) |
63 | | eqidd 2611 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑆 D 𝐹)‘𝑥) = ((𝑆 D 𝐹)‘𝑥)) |
64 | | eqidd 2611 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑆 D 𝐺)‘𝑥) = ((𝑆 D 𝐺)‘𝑥)) |
65 | 30, 31, 32, 31, 40, 39, 46 | dvadd 23509 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑆 D (𝐹 ∘𝑓 + 𝐺))‘𝑥) = (((𝑆 D 𝐹)‘𝑥) + ((𝑆 D 𝐺)‘𝑥))) |
66 | 65 | eqcomd 2616 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((𝑆 D 𝐹)‘𝑥) + ((𝑆 D 𝐺)‘𝑥)) = ((𝑆 D (𝐹 ∘𝑓 + 𝐺))‘𝑥)) |
67 | 5, 11, 18, 62, 63, 64, 66 | offveq 6816 |
. 2
⊢ (𝜑 → ((𝑆 D 𝐹) ∘𝑓 + (𝑆 D 𝐺)) = (𝑆 D (𝐹 ∘𝑓 + 𝐺))) |
68 | 67 | eqcomd 2616 |
1
⊢ (𝜑 → (𝑆 D (𝐹 ∘𝑓 + 𝐺)) = ((𝑆 D 𝐹) ∘𝑓 + (𝑆 D 𝐺))) |