Step | Hyp | Ref
| Expression |
1 | | dvaddf.f |
. . . . 5
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) |
2 | 1 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐹:𝑋⟶ℂ) |
3 | | dvaddf.df |
. . . . . 6
⊢ (𝜑 → dom (𝑆 D 𝐹) = 𝑋) |
4 | | dvbsss 23472 |
. . . . . 6
⊢ dom
(𝑆 D 𝐹) ⊆ 𝑆 |
5 | 3, 4 | syl6eqssr 3619 |
. . . . 5
⊢ (𝜑 → 𝑋 ⊆ 𝑆) |
6 | 5 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑋 ⊆ 𝑆) |
7 | | dvaddf.g |
. . . . 5
⊢ (𝜑 → 𝐺:𝑋⟶ℂ) |
8 | 7 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐺:𝑋⟶ℂ) |
9 | | dvaddf.s |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
10 | 9 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑆 ∈ {ℝ, ℂ}) |
11 | 3 | eleq2d 2673 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ dom (𝑆 D 𝐹) ↔ 𝑥 ∈ 𝑋)) |
12 | 11 | biimpar 501 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ dom (𝑆 D 𝐹)) |
13 | | dvaddf.dg |
. . . . . 6
⊢ (𝜑 → dom (𝑆 D 𝐺) = 𝑋) |
14 | 13 | eleq2d 2673 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ dom (𝑆 D 𝐺) ↔ 𝑥 ∈ 𝑋)) |
15 | 14 | biimpar 501 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ dom (𝑆 D 𝐺)) |
16 | 2, 6, 8, 6, 10, 12, 15 | dvmul 23510 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑆 D (𝐹 ∘𝑓 · 𝐺))‘𝑥) = ((((𝑆 D 𝐹)‘𝑥) · (𝐺‘𝑥)) + (((𝑆 D 𝐺)‘𝑥) · (𝐹‘𝑥)))) |
17 | 16 | mpteq2dva 4672 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ((𝑆 D (𝐹 ∘𝑓 · 𝐺))‘𝑥)) = (𝑥 ∈ 𝑋 ↦ ((((𝑆 D 𝐹)‘𝑥) · (𝐺‘𝑥)) + (((𝑆 D 𝐺)‘𝑥) · (𝐹‘𝑥))))) |
18 | | dvfg 23476 |
. . . . 5
⊢ (𝑆 ∈ {ℝ, ℂ}
→ (𝑆 D (𝐹 ∘𝑓
· 𝐺)):dom (𝑆 D (𝐹 ∘𝑓 · 𝐺))⟶ℂ) |
19 | 9, 18 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑆 D (𝐹 ∘𝑓 · 𝐺)):dom (𝑆 D (𝐹 ∘𝑓 · 𝐺))⟶ℂ) |
20 | | recnprss 23474 |
. . . . . . . 8
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
21 | 9, 20 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
22 | | mulcl 9899 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ) |
23 | 22 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ) |
24 | 9, 5 | ssexd 4733 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ V) |
25 | | inidm 3784 |
. . . . . . . 8
⊢ (𝑋 ∩ 𝑋) = 𝑋 |
26 | 23, 1, 7, 24, 24, 25 | off 6810 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ∘𝑓 · 𝐺):𝑋⟶ℂ) |
27 | 21, 26, 5 | dvbss 23471 |
. . . . . 6
⊢ (𝜑 → dom (𝑆 D (𝐹 ∘𝑓 · 𝐺)) ⊆ 𝑋) |
28 | 21 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑆 ⊆ ℂ) |
29 | | fvex 6113 |
. . . . . . . . . . 11
⊢ ((𝑆 D 𝐹)‘𝑥) ∈ V |
30 | 29 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑆 D 𝐹)‘𝑥) ∈ V) |
31 | | fvex 6113 |
. . . . . . . . . . 11
⊢ ((𝑆 D 𝐺)‘𝑥) ∈ V |
32 | 31 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑆 D 𝐺)‘𝑥) ∈ V) |
33 | | dvfg 23476 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈ {ℝ, ℂ}
→ (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ) |
34 | 9, 33 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ) |
35 | 34 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ) |
36 | | ffun 5961 |
. . . . . . . . . . . 12
⊢ ((𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ → Fun (𝑆 D 𝐹)) |
37 | | funfvbrb 6238 |
. . . . . . . . . . . 12
⊢ (Fun
(𝑆 D 𝐹) → (𝑥 ∈ dom (𝑆 D 𝐹) ↔ 𝑥(𝑆 D 𝐹)((𝑆 D 𝐹)‘𝑥))) |
38 | 35, 36, 37 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑥 ∈ dom (𝑆 D 𝐹) ↔ 𝑥(𝑆 D 𝐹)((𝑆 D 𝐹)‘𝑥))) |
39 | 12, 38 | mpbid 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥(𝑆 D 𝐹)((𝑆 D 𝐹)‘𝑥)) |
40 | | dvfg 23476 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈ {ℝ, ℂ}
→ (𝑆 D 𝐺):dom (𝑆 D 𝐺)⟶ℂ) |
41 | 9, 40 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆 D 𝐺):dom (𝑆 D 𝐺)⟶ℂ) |
42 | 41 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑆 D 𝐺):dom (𝑆 D 𝐺)⟶ℂ) |
43 | | ffun 5961 |
. . . . . . . . . . . 12
⊢ ((𝑆 D 𝐺):dom (𝑆 D 𝐺)⟶ℂ → Fun (𝑆 D 𝐺)) |
44 | | funfvbrb 6238 |
. . . . . . . . . . . 12
⊢ (Fun
(𝑆 D 𝐺) → (𝑥 ∈ dom (𝑆 D 𝐺) ↔ 𝑥(𝑆 D 𝐺)((𝑆 D 𝐺)‘𝑥))) |
45 | 42, 43, 44 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑥 ∈ dom (𝑆 D 𝐺) ↔ 𝑥(𝑆 D 𝐺)((𝑆 D 𝐺)‘𝑥))) |
46 | 15, 45 | mpbid 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥(𝑆 D 𝐺)((𝑆 D 𝐺)‘𝑥)) |
47 | | eqid 2610 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
48 | 2, 6, 8, 6, 28, 30, 32, 39, 46, 47 | dvmulbr 23508 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥(𝑆 D (𝐹 ∘𝑓 · 𝐺))((((𝑆 D 𝐹)‘𝑥) · (𝐺‘𝑥)) + (((𝑆 D 𝐺)‘𝑥) · (𝐹‘𝑥)))) |
49 | | reldv 23440 |
. . . . . . . . . 10
⊢ Rel
(𝑆 D (𝐹 ∘𝑓 · 𝐺)) |
50 | 49 | releldmi 5283 |
. . . . . . . . 9
⊢ (𝑥(𝑆 D (𝐹 ∘𝑓 · 𝐺))((((𝑆 D 𝐹)‘𝑥) · (𝐺‘𝑥)) + (((𝑆 D 𝐺)‘𝑥) · (𝐹‘𝑥))) → 𝑥 ∈ dom (𝑆 D (𝐹 ∘𝑓 · 𝐺))) |
51 | 48, 50 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ dom (𝑆 D (𝐹 ∘𝑓 · 𝐺))) |
52 | 51 | ex 449 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝑋 → 𝑥 ∈ dom (𝑆 D (𝐹 ∘𝑓 · 𝐺)))) |
53 | 52 | ssrdv 3574 |
. . . . . 6
⊢ (𝜑 → 𝑋 ⊆ dom (𝑆 D (𝐹 ∘𝑓 · 𝐺))) |
54 | 27, 53 | eqssd 3585 |
. . . . 5
⊢ (𝜑 → dom (𝑆 D (𝐹 ∘𝑓 · 𝐺)) = 𝑋) |
55 | 54 | feq2d 5944 |
. . . 4
⊢ (𝜑 → ((𝑆 D (𝐹 ∘𝑓 · 𝐺)):dom (𝑆 D (𝐹 ∘𝑓 · 𝐺))⟶ℂ ↔ (𝑆 D (𝐹 ∘𝑓 · 𝐺)):𝑋⟶ℂ)) |
56 | 19, 55 | mpbid 221 |
. . 3
⊢ (𝜑 → (𝑆 D (𝐹 ∘𝑓 · 𝐺)):𝑋⟶ℂ) |
57 | 56 | feqmptd 6159 |
. 2
⊢ (𝜑 → (𝑆 D (𝐹 ∘𝑓 · 𝐺)) = (𝑥 ∈ 𝑋 ↦ ((𝑆 D (𝐹 ∘𝑓 · 𝐺))‘𝑥))) |
58 | | ovex 6577 |
. . . 4
⊢ (((𝑆 D 𝐹)‘𝑥) · (𝐺‘𝑥)) ∈ V |
59 | 58 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((𝑆 D 𝐹)‘𝑥) · (𝐺‘𝑥)) ∈ V) |
60 | | ovex 6577 |
. . . 4
⊢ (((𝑆 D 𝐺)‘𝑥) · (𝐹‘𝑥)) ∈ V |
61 | 60 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((𝑆 D 𝐺)‘𝑥) · (𝐹‘𝑥)) ∈ V) |
62 | | fvex 6113 |
. . . . 5
⊢ (𝐺‘𝑥) ∈ V |
63 | 62 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐺‘𝑥) ∈ V) |
64 | 3 | feq2d 5944 |
. . . . . 6
⊢ (𝜑 → ((𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ ↔ (𝑆 D 𝐹):𝑋⟶ℂ)) |
65 | 34, 64 | mpbid 221 |
. . . . 5
⊢ (𝜑 → (𝑆 D 𝐹):𝑋⟶ℂ) |
66 | 65 | feqmptd 6159 |
. . . 4
⊢ (𝜑 → (𝑆 D 𝐹) = (𝑥 ∈ 𝑋 ↦ ((𝑆 D 𝐹)‘𝑥))) |
67 | 7 | feqmptd 6159 |
. . . 4
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝑋 ↦ (𝐺‘𝑥))) |
68 | 24, 30, 63, 66, 67 | offval2 6812 |
. . 3
⊢ (𝜑 → ((𝑆 D 𝐹) ∘𝑓 · 𝐺) = (𝑥 ∈ 𝑋 ↦ (((𝑆 D 𝐹)‘𝑥) · (𝐺‘𝑥)))) |
69 | | fvex 6113 |
. . . . 5
⊢ (𝐹‘𝑥) ∈ V |
70 | 69 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ V) |
71 | 13 | feq2d 5944 |
. . . . . 6
⊢ (𝜑 → ((𝑆 D 𝐺):dom (𝑆 D 𝐺)⟶ℂ ↔ (𝑆 D 𝐺):𝑋⟶ℂ)) |
72 | 41, 71 | mpbid 221 |
. . . . 5
⊢ (𝜑 → (𝑆 D 𝐺):𝑋⟶ℂ) |
73 | 72 | feqmptd 6159 |
. . . 4
⊢ (𝜑 → (𝑆 D 𝐺) = (𝑥 ∈ 𝑋 ↦ ((𝑆 D 𝐺)‘𝑥))) |
74 | 1 | feqmptd 6159 |
. . . 4
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝑋 ↦ (𝐹‘𝑥))) |
75 | 24, 32, 70, 73, 74 | offval2 6812 |
. . 3
⊢ (𝜑 → ((𝑆 D 𝐺) ∘𝑓 · 𝐹) = (𝑥 ∈ 𝑋 ↦ (((𝑆 D 𝐺)‘𝑥) · (𝐹‘𝑥)))) |
76 | 24, 59, 61, 68, 75 | offval2 6812 |
. 2
⊢ (𝜑 → (((𝑆 D 𝐹) ∘𝑓 · 𝐺) ∘𝑓 +
((𝑆 D 𝐺) ∘𝑓 · 𝐹)) = (𝑥 ∈ 𝑋 ↦ ((((𝑆 D 𝐹)‘𝑥) · (𝐺‘𝑥)) + (((𝑆 D 𝐺)‘𝑥) · (𝐹‘𝑥))))) |
77 | 17, 57, 76 | 3eqtr4d 2654 |
1
⊢ (𝜑 → (𝑆 D (𝐹 ∘𝑓 · 𝐺)) = (((𝑆 D 𝐹) ∘𝑓 · 𝐺) ∘𝑓 +
((𝑆 D 𝐺) ∘𝑓 · 𝐹))) |