Step | Hyp | Ref
| Expression |
1 | | dvcmul.s |
. . 3
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
2 | | dvcmul.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ ℂ) |
3 | | fconstg 6005 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (𝑋 × {𝐴}):𝑋⟶{𝐴}) |
4 | 2, 3 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑋 × {𝐴}):𝑋⟶{𝐴}) |
5 | 2 | snssd 4281 |
. . . 4
⊢ (𝜑 → {𝐴} ⊆ ℂ) |
6 | 4, 5 | fssd 5970 |
. . 3
⊢ (𝜑 → (𝑋 × {𝐴}):𝑋⟶ℂ) |
7 | | dvcmul.f |
. . 3
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) |
8 | | c0ex 9913 |
. . . . . 6
⊢ 0 ∈
V |
9 | 8 | fconst 6004 |
. . . . 5
⊢ (𝑋 × {0}):𝑋⟶{0} |
10 | | recnprss 23474 |
. . . . . . . . 9
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
11 | 1, 10 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
12 | | fconstg 6005 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (𝑆 × {𝐴}):𝑆⟶{𝐴}) |
13 | 2, 12 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆 × {𝐴}):𝑆⟶{𝐴}) |
14 | 13, 5 | fssd 5970 |
. . . . . . . 8
⊢ (𝜑 → (𝑆 × {𝐴}):𝑆⟶ℂ) |
15 | | ssid 3587 |
. . . . . . . . 9
⊢ 𝑆 ⊆ 𝑆 |
16 | 15 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ⊆ 𝑆) |
17 | | dvcmulf.df |
. . . . . . . . 9
⊢ (𝜑 → dom (𝑆 D 𝐹) = 𝑋) |
18 | | dvbsss 23472 |
. . . . . . . . . 10
⊢ dom
(𝑆 D 𝐹) ⊆ 𝑆 |
19 | 18 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → dom (𝑆 D 𝐹) ⊆ 𝑆) |
20 | 17, 19 | eqsstr3d 3603 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ⊆ 𝑆) |
21 | | eqid 2610 |
. . . . . . . . 9
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
22 | | eqid 2610 |
. . . . . . . . 9
⊢
((TopOpen‘ℂfld) ↾t 𝑆) =
((TopOpen‘ℂfld) ↾t 𝑆) |
23 | 21, 22 | dvres 23481 |
. . . . . . . 8
⊢ (((𝑆 ⊆ ℂ ∧ (𝑆 × {𝐴}):𝑆⟶ℂ) ∧ (𝑆 ⊆ 𝑆 ∧ 𝑋 ⊆ 𝑆)) → (𝑆 D ((𝑆 × {𝐴}) ↾ 𝑋)) = ((𝑆 D (𝑆 × {𝐴})) ↾
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝑋))) |
24 | 11, 14, 16, 20, 23 | syl22anc 1319 |
. . . . . . 7
⊢ (𝜑 → (𝑆 D ((𝑆 × {𝐴}) ↾ 𝑋)) = ((𝑆 D (𝑆 × {𝐴})) ↾
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝑋))) |
25 | 20 | resmptd 5371 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ 𝐴) ↾ 𝑋) = (𝑥 ∈ 𝑋 ↦ 𝐴)) |
26 | | fconstmpt 5085 |
. . . . . . . . . 10
⊢ (𝑆 × {𝐴}) = (𝑥 ∈ 𝑆 ↦ 𝐴) |
27 | 26 | reseq1i 5313 |
. . . . . . . . 9
⊢ ((𝑆 × {𝐴}) ↾ 𝑋) = ((𝑥 ∈ 𝑆 ↦ 𝐴) ↾ 𝑋) |
28 | | fconstmpt 5085 |
. . . . . . . . 9
⊢ (𝑋 × {𝐴}) = (𝑥 ∈ 𝑋 ↦ 𝐴) |
29 | 25, 27, 28 | 3eqtr4g 2669 |
. . . . . . . 8
⊢ (𝜑 → ((𝑆 × {𝐴}) ↾ 𝑋) = (𝑋 × {𝐴})) |
30 | 29 | oveq2d 6565 |
. . . . . . 7
⊢ (𝜑 → (𝑆 D ((𝑆 × {𝐴}) ↾ 𝑋)) = (𝑆 D (𝑋 × {𝐴}))) |
31 | 20 | resmptd 5371 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ 0) ↾ 𝑋) = (𝑥 ∈ 𝑋 ↦ 0)) |
32 | | fconstg 6005 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ → (ℂ
× {𝐴}):ℂ⟶{𝐴}) |
33 | 2, 32 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℂ × {𝐴}):ℂ⟶{𝐴}) |
34 | 33, 5 | fssd 5970 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℂ × {𝐴}):ℂ⟶ℂ) |
35 | | ssid 3587 |
. . . . . . . . . . . . 13
⊢ ℂ
⊆ ℂ |
36 | 35 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℂ ⊆
ℂ) |
37 | | dvconst 23486 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ → (ℂ
D (ℂ × {𝐴})) =
(ℂ × {0})) |
38 | 2, 37 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℂ D (ℂ
× {𝐴})) = (ℂ
× {0})) |
39 | 38 | dmeqd 5248 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom (ℂ D (ℂ
× {𝐴})) = dom
(ℂ × {0})) |
40 | 8 | fconst 6004 |
. . . . . . . . . . . . . . 15
⊢ (ℂ
× {0}):ℂ⟶{0} |
41 | 40 | fdmi 5965 |
. . . . . . . . . . . . . 14
⊢ dom
(ℂ × {0}) = ℂ |
42 | 39, 41 | syl6eq 2660 |
. . . . . . . . . . . . 13
⊢ (𝜑 → dom (ℂ D (ℂ
× {𝐴})) =
ℂ) |
43 | 11, 42 | sseqtr4d 3605 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ⊆ dom (ℂ D (ℂ ×
{𝐴}))) |
44 | | dvres3 23483 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
(ℂ × {𝐴}):ℂ⟶ℂ) ∧ (ℂ
⊆ ℂ ∧ 𝑆
⊆ dom (ℂ D (ℂ × {𝐴})))) → (𝑆 D ((ℂ × {𝐴}) ↾ 𝑆)) = ((ℂ D (ℂ × {𝐴})) ↾ 𝑆)) |
45 | 1, 34, 36, 43, 44 | syl22anc 1319 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑆 D ((ℂ × {𝐴}) ↾ 𝑆)) = ((ℂ D (ℂ × {𝐴})) ↾ 𝑆)) |
46 | | xpssres 5354 |
. . . . . . . . . . . . 13
⊢ (𝑆 ⊆ ℂ →
((ℂ × {𝐴})
↾ 𝑆) = (𝑆 × {𝐴})) |
47 | 11, 46 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((ℂ × {𝐴}) ↾ 𝑆) = (𝑆 × {𝐴})) |
48 | 47 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑆 D ((ℂ × {𝐴}) ↾ 𝑆)) = (𝑆 D (𝑆 × {𝐴}))) |
49 | 38 | reseq1d 5316 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((ℂ D (ℂ
× {𝐴})) ↾ 𝑆) = ((ℂ × {0})
↾ 𝑆)) |
50 | | xpssres 5354 |
. . . . . . . . . . . . 13
⊢ (𝑆 ⊆ ℂ →
((ℂ × {0}) ↾ 𝑆) = (𝑆 × {0})) |
51 | 11, 50 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((ℂ × {0})
↾ 𝑆) = (𝑆 × {0})) |
52 | 49, 51 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (𝜑 → ((ℂ D (ℂ
× {𝐴})) ↾ 𝑆) = (𝑆 × {0})) |
53 | 45, 48, 52 | 3eqtr3d 2652 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆 D (𝑆 × {𝐴})) = (𝑆 × {0})) |
54 | | fconstmpt 5085 |
. . . . . . . . . 10
⊢ (𝑆 × {0}) = (𝑥 ∈ 𝑆 ↦ 0) |
55 | 53, 54 | syl6eq 2660 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆 D (𝑆 × {𝐴})) = (𝑥 ∈ 𝑆 ↦ 0)) |
56 | 21 | cnfldtopon 22396 |
. . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
57 | | resttopon 20775 |
. . . . . . . . . . . . 13
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ 𝑆 ⊆ ℂ)
→ ((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆)) |
58 | 56, 11, 57 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆)) |
59 | | topontop 20541 |
. . . . . . . . . . . 12
⊢
(((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆) →
((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top) |
61 | | toponuni 20542 |
. . . . . . . . . . . . 13
⊢
(((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = ∪
((TopOpen‘ℂfld) ↾t 𝑆)) |
62 | 58, 61 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 = ∪
((TopOpen‘ℂfld) ↾t 𝑆)) |
63 | 20, 62 | sseqtrd 3604 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ⊆ ∪
((TopOpen‘ℂfld) ↾t 𝑆)) |
64 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ ∪ ((TopOpen‘ℂfld)
↾t 𝑆) =
∪ ((TopOpen‘ℂfld)
↾t 𝑆) |
65 | 64 | ntrss2 20671 |
. . . . . . . . . . 11
⊢
((((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top ∧ 𝑋 ⊆ ∪ ((TopOpen‘ℂfld)
↾t 𝑆))
→ ((int‘((TopOpen‘ℂfld) ↾t
𝑆))‘𝑋) ⊆ 𝑋) |
66 | 60, 63, 65 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 →
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝑋) ⊆ 𝑋) |
67 | 11, 7, 20, 22, 21 | dvbssntr 23470 |
. . . . . . . . . . 11
⊢ (𝜑 → dom (𝑆 D 𝐹) ⊆
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝑋)) |
68 | 17, 67 | eqsstr3d 3603 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ⊆
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝑋)) |
69 | 66, 68 | eqssd 3585 |
. . . . . . . . 9
⊢ (𝜑 →
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝑋) = 𝑋) |
70 | 55, 69 | reseq12d 5318 |
. . . . . . . 8
⊢ (𝜑 → ((𝑆 D (𝑆 × {𝐴})) ↾
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝑋)) = ((𝑥 ∈ 𝑆 ↦ 0) ↾ 𝑋)) |
71 | | fconstmpt 5085 |
. . . . . . . . 9
⊢ (𝑋 × {0}) = (𝑥 ∈ 𝑋 ↦ 0) |
72 | 71 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝑋 × {0}) = (𝑥 ∈ 𝑋 ↦ 0)) |
73 | 31, 70, 72 | 3eqtr4d 2654 |
. . . . . . 7
⊢ (𝜑 → ((𝑆 D (𝑆 × {𝐴})) ↾
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝑋)) = (𝑋 × {0})) |
74 | 24, 30, 73 | 3eqtr3d 2652 |
. . . . . 6
⊢ (𝜑 → (𝑆 D (𝑋 × {𝐴})) = (𝑋 × {0})) |
75 | 74 | feq1d 5943 |
. . . . 5
⊢ (𝜑 → ((𝑆 D (𝑋 × {𝐴})):𝑋⟶{0} ↔ (𝑋 × {0}):𝑋⟶{0})) |
76 | 9, 75 | mpbiri 247 |
. . . 4
⊢ (𝜑 → (𝑆 D (𝑋 × {𝐴})):𝑋⟶{0}) |
77 | | fdm 5964 |
. . . 4
⊢ ((𝑆 D (𝑋 × {𝐴})):𝑋⟶{0} → dom (𝑆 D (𝑋 × {𝐴})) = 𝑋) |
78 | 76, 77 | syl 17 |
. . 3
⊢ (𝜑 → dom (𝑆 D (𝑋 × {𝐴})) = 𝑋) |
79 | 1, 6, 7, 78, 17 | dvmulf 23512 |
. 2
⊢ (𝜑 → (𝑆 D ((𝑋 × {𝐴}) ∘𝑓 ·
𝐹)) = (((𝑆 D (𝑋 × {𝐴})) ∘𝑓 ·
𝐹)
∘𝑓 + ((𝑆 D 𝐹) ∘𝑓 ·
(𝑋 × {𝐴})))) |
80 | | sseqin2 3779 |
. . . . . 6
⊢ (𝑋 ⊆ 𝑆 ↔ (𝑆 ∩ 𝑋) = 𝑋) |
81 | 20, 80 | sylib 207 |
. . . . 5
⊢ (𝜑 → (𝑆 ∩ 𝑋) = 𝑋) |
82 | 81 | mpteq1d 4666 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝑆 ∩ 𝑋) ↦ (𝐴 · (𝐹‘𝑥))) = (𝑥 ∈ 𝑋 ↦ (𝐴 · (𝐹‘𝑥)))) |
83 | | ffn 5958 |
. . . . . 6
⊢ ((𝑆 × {𝐴}):𝑆⟶{𝐴} → (𝑆 × {𝐴}) Fn 𝑆) |
84 | 13, 83 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑆 × {𝐴}) Fn 𝑆) |
85 | | ffn 5958 |
. . . . . 6
⊢ (𝐹:𝑋⟶ℂ → 𝐹 Fn 𝑋) |
86 | 7, 85 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐹 Fn 𝑋) |
87 | 1, 20 | ssexd 4733 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ V) |
88 | | eqid 2610 |
. . . . 5
⊢ (𝑆 ∩ 𝑋) = (𝑆 ∩ 𝑋) |
89 | | fvconst2g 6372 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((𝑆 × {𝐴})‘𝑥) = 𝐴) |
90 | 2, 89 | sylan 487 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((𝑆 × {𝐴})‘𝑥) = 𝐴) |
91 | | eqidd 2611 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) = (𝐹‘𝑥)) |
92 | 84, 86, 1, 87, 88, 90, 91 | offval 6802 |
. . . 4
⊢ (𝜑 → ((𝑆 × {𝐴}) ∘𝑓 ·
𝐹) = (𝑥 ∈ (𝑆 ∩ 𝑋) ↦ (𝐴 · (𝐹‘𝑥)))) |
93 | | ffn 5958 |
. . . . . 6
⊢ ((𝑋 × {𝐴}):𝑋⟶{𝐴} → (𝑋 × {𝐴}) Fn 𝑋) |
94 | 4, 93 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑋 × {𝐴}) Fn 𝑋) |
95 | | inidm 3784 |
. . . . 5
⊢ (𝑋 ∩ 𝑋) = 𝑋 |
96 | | fvconst2g 6372 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑋) → ((𝑋 × {𝐴})‘𝑥) = 𝐴) |
97 | 2, 96 | sylan 487 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑋 × {𝐴})‘𝑥) = 𝐴) |
98 | 94, 86, 87, 87, 95, 97, 91 | offval 6802 |
. . . 4
⊢ (𝜑 → ((𝑋 × {𝐴}) ∘𝑓 ·
𝐹) = (𝑥 ∈ 𝑋 ↦ (𝐴 · (𝐹‘𝑥)))) |
99 | 82, 92, 98 | 3eqtr4d 2654 |
. . 3
⊢ (𝜑 → ((𝑆 × {𝐴}) ∘𝑓 ·
𝐹) = ((𝑋 × {𝐴}) ∘𝑓 ·
𝐹)) |
100 | 99 | oveq2d 6565 |
. 2
⊢ (𝜑 → (𝑆 D ((𝑆 × {𝐴}) ∘𝑓 ·
𝐹)) = (𝑆 D ((𝑋 × {𝐴}) ∘𝑓 ·
𝐹))) |
101 | 81 | mpteq1d 4666 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝑆 ∩ 𝑋) ↦ (𝐴 · ((𝑆 D 𝐹)‘𝑥))) = (𝑥 ∈ 𝑋 ↦ (𝐴 · ((𝑆 D 𝐹)‘𝑥)))) |
102 | | dvfg 23476 |
. . . . . . 7
⊢ (𝑆 ∈ {ℝ, ℂ}
→ (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ) |
103 | 1, 102 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ) |
104 | 17 | feq2d 5944 |
. . . . . 6
⊢ (𝜑 → ((𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ ↔ (𝑆 D 𝐹):𝑋⟶ℂ)) |
105 | 103, 104 | mpbid 221 |
. . . . 5
⊢ (𝜑 → (𝑆 D 𝐹):𝑋⟶ℂ) |
106 | | ffn 5958 |
. . . . 5
⊢ ((𝑆 D 𝐹):𝑋⟶ℂ → (𝑆 D 𝐹) Fn 𝑋) |
107 | 105, 106 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑆 D 𝐹) Fn 𝑋) |
108 | | eqidd 2611 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑆 D 𝐹)‘𝑥) = ((𝑆 D 𝐹)‘𝑥)) |
109 | 84, 107, 1, 87, 88, 90, 108 | offval 6802 |
. . 3
⊢ (𝜑 → ((𝑆 × {𝐴}) ∘𝑓 ·
(𝑆 D 𝐹)) = (𝑥 ∈ (𝑆 ∩ 𝑋) ↦ (𝐴 · ((𝑆 D 𝐹)‘𝑥)))) |
110 | | 0cnd 9912 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 0 ∈ ℂ) |
111 | | ovex 6577 |
. . . . . 6
⊢ (((𝑆 D 𝐹)‘𝑥) · 𝐴) ∈ V |
112 | 111 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((𝑆 D 𝐹)‘𝑥) · 𝐴) ∈ V) |
113 | 74 | oveq1d 6564 |
. . . . . . 7
⊢ (𝜑 → ((𝑆 D (𝑋 × {𝐴})) ∘𝑓 ·
𝐹) = ((𝑋 × {0}) ∘𝑓
· 𝐹)) |
114 | | 0cnd 9912 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
ℂ) |
115 | | mul02 10093 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℂ → (0
· 𝑥) =
0) |
116 | 115 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (0 · 𝑥) = 0) |
117 | 87, 7, 114, 114, 116 | caofid2 6826 |
. . . . . . 7
⊢ (𝜑 → ((𝑋 × {0}) ∘𝑓
· 𝐹) = (𝑋 × {0})) |
118 | 113, 117 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → ((𝑆 D (𝑋 × {𝐴})) ∘𝑓 ·
𝐹) = (𝑋 × {0})) |
119 | 118, 71 | syl6eq 2660 |
. . . . 5
⊢ (𝜑 → ((𝑆 D (𝑋 × {𝐴})) ∘𝑓 ·
𝐹) = (𝑥 ∈ 𝑋 ↦ 0)) |
120 | | fvex 6113 |
. . . . . . 7
⊢ ((𝑆 D 𝐹)‘𝑥) ∈ V |
121 | 120 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑆 D 𝐹)‘𝑥) ∈ V) |
122 | 2 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) |
123 | 105 | feqmptd 6159 |
. . . . . 6
⊢ (𝜑 → (𝑆 D 𝐹) = (𝑥 ∈ 𝑋 ↦ ((𝑆 D 𝐹)‘𝑥))) |
124 | 28 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝑋 × {𝐴}) = (𝑥 ∈ 𝑋 ↦ 𝐴)) |
125 | 87, 121, 122, 123, 124 | offval2 6812 |
. . . . 5
⊢ (𝜑 → ((𝑆 D 𝐹) ∘𝑓 ·
(𝑋 × {𝐴})) = (𝑥 ∈ 𝑋 ↦ (((𝑆 D 𝐹)‘𝑥) · 𝐴))) |
126 | 87, 110, 112, 119, 125 | offval2 6812 |
. . . 4
⊢ (𝜑 → (((𝑆 D (𝑋 × {𝐴})) ∘𝑓 ·
𝐹)
∘𝑓 + ((𝑆 D 𝐹) ∘𝑓 ·
(𝑋 × {𝐴}))) = (𝑥 ∈ 𝑋 ↦ (0 + (((𝑆 D 𝐹)‘𝑥) · 𝐴)))) |
127 | 105 | ffvelrnda 6267 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑆 D 𝐹)‘𝑥) ∈ ℂ) |
128 | 127, 122 | mulcld 9939 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((𝑆 D 𝐹)‘𝑥) · 𝐴) ∈ ℂ) |
129 | 128 | addid2d 10116 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (0 + (((𝑆 D 𝐹)‘𝑥) · 𝐴)) = (((𝑆 D 𝐹)‘𝑥) · 𝐴)) |
130 | 127, 122 | mulcomd 9940 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((𝑆 D 𝐹)‘𝑥) · 𝐴) = (𝐴 · ((𝑆 D 𝐹)‘𝑥))) |
131 | 129, 130 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (0 + (((𝑆 D 𝐹)‘𝑥) · 𝐴)) = (𝐴 · ((𝑆 D 𝐹)‘𝑥))) |
132 | 131 | mpteq2dva 4672 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (0 + (((𝑆 D 𝐹)‘𝑥) · 𝐴))) = (𝑥 ∈ 𝑋 ↦ (𝐴 · ((𝑆 D 𝐹)‘𝑥)))) |
133 | 126, 132 | eqtrd 2644 |
. . 3
⊢ (𝜑 → (((𝑆 D (𝑋 × {𝐴})) ∘𝑓 ·
𝐹)
∘𝑓 + ((𝑆 D 𝐹) ∘𝑓 ·
(𝑋 × {𝐴}))) = (𝑥 ∈ 𝑋 ↦ (𝐴 · ((𝑆 D 𝐹)‘𝑥)))) |
134 | 101, 109,
133 | 3eqtr4d 2654 |
. 2
⊢ (𝜑 → ((𝑆 × {𝐴}) ∘𝑓 ·
(𝑆 D 𝐹)) = (((𝑆 D (𝑋 × {𝐴})) ∘𝑓 ·
𝐹)
∘𝑓 + ((𝑆 D 𝐹) ∘𝑓 ·
(𝑋 × {𝐴})))) |
135 | 79, 100, 134 | 3eqtr4d 2654 |
1
⊢ (𝜑 → (𝑆 D ((𝑆 × {𝐴}) ∘𝑓 ·
𝐹)) = ((𝑆 × {𝐴}) ∘𝑓 ·
(𝑆 D 𝐹))) |