| Step | Hyp | Ref
| Expression |
| 1 | | dvcmul.s |
. . 3
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
| 2 | | dvcmul.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 3 | | fconstg 6795 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (𝑋 × {𝐴}):𝑋⟶{𝐴}) |
| 4 | 2, 3 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑋 × {𝐴}):𝑋⟶{𝐴}) |
| 5 | 2 | snssd 4809 |
. . . 4
⊢ (𝜑 → {𝐴} ⊆ ℂ) |
| 6 | 4, 5 | fssd 6753 |
. . 3
⊢ (𝜑 → (𝑋 × {𝐴}):𝑋⟶ℂ) |
| 7 | | dvcmul.f |
. . 3
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) |
| 8 | | c0ex 11255 |
. . . . . 6
⊢ 0 ∈
V |
| 9 | 8 | fconst 6794 |
. . . . 5
⊢ (𝑋 × {0}):𝑋⟶{0} |
| 10 | | recnprss 25939 |
. . . . . . . . 9
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
| 11 | 1, 10 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
| 12 | | fconstg 6795 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (𝑆 × {𝐴}):𝑆⟶{𝐴}) |
| 13 | 2, 12 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆 × {𝐴}):𝑆⟶{𝐴}) |
| 14 | 13, 5 | fssd 6753 |
. . . . . . . 8
⊢ (𝜑 → (𝑆 × {𝐴}):𝑆⟶ℂ) |
| 15 | | ssidd 4007 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ⊆ 𝑆) |
| 16 | | dvcmulf.df |
. . . . . . . . 9
⊢ (𝜑 → dom (𝑆 D 𝐹) = 𝑋) |
| 17 | | dvbsss 25937 |
. . . . . . . . . 10
⊢ dom
(𝑆 D 𝐹) ⊆ 𝑆 |
| 18 | 17 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → dom (𝑆 D 𝐹) ⊆ 𝑆) |
| 19 | 16, 18 | eqsstrrd 4019 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ⊆ 𝑆) |
| 20 | | eqid 2737 |
. . . . . . . . 9
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 21 | | eqid 2737 |
. . . . . . . . 9
⊢
((TopOpen‘ℂfld) ↾t 𝑆) =
((TopOpen‘ℂfld) ↾t 𝑆) |
| 22 | 20, 21 | dvres 25946 |
. . . . . . . 8
⊢ (((𝑆 ⊆ ℂ ∧ (𝑆 × {𝐴}):𝑆⟶ℂ) ∧ (𝑆 ⊆ 𝑆 ∧ 𝑋 ⊆ 𝑆)) → (𝑆 D ((𝑆 × {𝐴}) ↾ 𝑋)) = ((𝑆 D (𝑆 × {𝐴})) ↾
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝑋))) |
| 23 | 11, 14, 15, 19, 22 | syl22anc 839 |
. . . . . . 7
⊢ (𝜑 → (𝑆 D ((𝑆 × {𝐴}) ↾ 𝑋)) = ((𝑆 D (𝑆 × {𝐴})) ↾
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝑋))) |
| 24 | 19 | resmptd 6058 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ 𝐴) ↾ 𝑋) = (𝑥 ∈ 𝑋 ↦ 𝐴)) |
| 25 | | fconstmpt 5747 |
. . . . . . . . . 10
⊢ (𝑆 × {𝐴}) = (𝑥 ∈ 𝑆 ↦ 𝐴) |
| 26 | 25 | reseq1i 5993 |
. . . . . . . . 9
⊢ ((𝑆 × {𝐴}) ↾ 𝑋) = ((𝑥 ∈ 𝑆 ↦ 𝐴) ↾ 𝑋) |
| 27 | | fconstmpt 5747 |
. . . . . . . . 9
⊢ (𝑋 × {𝐴}) = (𝑥 ∈ 𝑋 ↦ 𝐴) |
| 28 | 24, 26, 27 | 3eqtr4g 2802 |
. . . . . . . 8
⊢ (𝜑 → ((𝑆 × {𝐴}) ↾ 𝑋) = (𝑋 × {𝐴})) |
| 29 | 28 | oveq2d 7447 |
. . . . . . 7
⊢ (𝜑 → (𝑆 D ((𝑆 × {𝐴}) ↾ 𝑋)) = (𝑆 D (𝑋 × {𝐴}))) |
| 30 | 19 | resmptd 6058 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ 0) ↾ 𝑋) = (𝑥 ∈ 𝑋 ↦ 0)) |
| 31 | | fconstg 6795 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ → (ℂ
× {𝐴}):ℂ⟶{𝐴}) |
| 32 | 2, 31 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℂ × {𝐴}):ℂ⟶{𝐴}) |
| 33 | 32, 5 | fssd 6753 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℂ × {𝐴}):ℂ⟶ℂ) |
| 34 | | ssidd 4007 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℂ ⊆
ℂ) |
| 35 | | dvconst 25952 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ → (ℂ
D (ℂ × {𝐴})) =
(ℂ × {0})) |
| 36 | 2, 35 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℂ D (ℂ
× {𝐴})) = (ℂ
× {0})) |
| 37 | 36 | dmeqd 5916 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom (ℂ D (ℂ
× {𝐴})) = dom
(ℂ × {0})) |
| 38 | 8 | fconst 6794 |
. . . . . . . . . . . . . . 15
⊢ (ℂ
× {0}):ℂ⟶{0} |
| 39 | 38 | fdmi 6747 |
. . . . . . . . . . . . . 14
⊢ dom
(ℂ × {0}) = ℂ |
| 40 | 37, 39 | eqtrdi 2793 |
. . . . . . . . . . . . 13
⊢ (𝜑 → dom (ℂ D (ℂ
× {𝐴})) =
ℂ) |
| 41 | 11, 40 | sseqtrrd 4021 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ⊆ dom (ℂ D (ℂ ×
{𝐴}))) |
| 42 | | dvres3 25948 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
(ℂ × {𝐴}):ℂ⟶ℂ) ∧ (ℂ
⊆ ℂ ∧ 𝑆
⊆ dom (ℂ D (ℂ × {𝐴})))) → (𝑆 D ((ℂ × {𝐴}) ↾ 𝑆)) = ((ℂ D (ℂ × {𝐴})) ↾ 𝑆)) |
| 43 | 1, 33, 34, 41, 42 | syl22anc 839 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑆 D ((ℂ × {𝐴}) ↾ 𝑆)) = ((ℂ D (ℂ × {𝐴})) ↾ 𝑆)) |
| 44 | | xpssres 6036 |
. . . . . . . . . . . . 13
⊢ (𝑆 ⊆ ℂ →
((ℂ × {𝐴})
↾ 𝑆) = (𝑆 × {𝐴})) |
| 45 | 11, 44 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((ℂ × {𝐴}) ↾ 𝑆) = (𝑆 × {𝐴})) |
| 46 | 45 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑆 D ((ℂ × {𝐴}) ↾ 𝑆)) = (𝑆 D (𝑆 × {𝐴}))) |
| 47 | 36 | reseq1d 5996 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((ℂ D (ℂ
× {𝐴})) ↾ 𝑆) = ((ℂ × {0})
↾ 𝑆)) |
| 48 | | xpssres 6036 |
. . . . . . . . . . . . 13
⊢ (𝑆 ⊆ ℂ →
((ℂ × {0}) ↾ 𝑆) = (𝑆 × {0})) |
| 49 | 11, 48 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((ℂ × {0})
↾ 𝑆) = (𝑆 × {0})) |
| 50 | 47, 49 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (𝜑 → ((ℂ D (ℂ
× {𝐴})) ↾ 𝑆) = (𝑆 × {0})) |
| 51 | 43, 46, 50 | 3eqtr3d 2785 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆 D (𝑆 × {𝐴})) = (𝑆 × {0})) |
| 52 | | fconstmpt 5747 |
. . . . . . . . . 10
⊢ (𝑆 × {0}) = (𝑥 ∈ 𝑆 ↦ 0) |
| 53 | 51, 52 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆 D (𝑆 × {𝐴})) = (𝑥 ∈ 𝑆 ↦ 0)) |
| 54 | 20 | cnfldtopon 24803 |
. . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
| 55 | | resttopon 23169 |
. . . . . . . . . . . . 13
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ 𝑆 ⊆ ℂ)
→ ((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆)) |
| 56 | 54, 11, 55 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆)) |
| 57 | | topontop 22919 |
. . . . . . . . . . . 12
⊢
(((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆) →
((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top) |
| 58 | 56, 57 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top) |
| 59 | | toponuni 22920 |
. . . . . . . . . . . . 13
⊢
(((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = ∪
((TopOpen‘ℂfld) ↾t 𝑆)) |
| 60 | 56, 59 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 = ∪
((TopOpen‘ℂfld) ↾t 𝑆)) |
| 61 | 19, 60 | sseqtrd 4020 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ⊆ ∪
((TopOpen‘ℂfld) ↾t 𝑆)) |
| 62 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ ∪ ((TopOpen‘ℂfld)
↾t 𝑆) =
∪ ((TopOpen‘ℂfld)
↾t 𝑆) |
| 63 | 62 | ntrss2 23065 |
. . . . . . . . . . 11
⊢
((((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top ∧ 𝑋 ⊆ ∪ ((TopOpen‘ℂfld)
↾t 𝑆))
→ ((int‘((TopOpen‘ℂfld) ↾t
𝑆))‘𝑋) ⊆ 𝑋) |
| 64 | 58, 61, 63 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 →
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝑋) ⊆ 𝑋) |
| 65 | 11, 7, 19, 21, 20 | dvbssntr 25935 |
. . . . . . . . . . 11
⊢ (𝜑 → dom (𝑆 D 𝐹) ⊆
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝑋)) |
| 66 | 16, 65 | eqsstrrd 4019 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ⊆
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝑋)) |
| 67 | 64, 66 | eqssd 4001 |
. . . . . . . . 9
⊢ (𝜑 →
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝑋) = 𝑋) |
| 68 | 53, 67 | reseq12d 5998 |
. . . . . . . 8
⊢ (𝜑 → ((𝑆 D (𝑆 × {𝐴})) ↾
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝑋)) = ((𝑥 ∈ 𝑆 ↦ 0) ↾ 𝑋)) |
| 69 | | fconstmpt 5747 |
. . . . . . . . 9
⊢ (𝑋 × {0}) = (𝑥 ∈ 𝑋 ↦ 0) |
| 70 | 69 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝑋 × {0}) = (𝑥 ∈ 𝑋 ↦ 0)) |
| 71 | 30, 68, 70 | 3eqtr4d 2787 |
. . . . . . 7
⊢ (𝜑 → ((𝑆 D (𝑆 × {𝐴})) ↾
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝑋)) = (𝑋 × {0})) |
| 72 | 23, 29, 71 | 3eqtr3d 2785 |
. . . . . 6
⊢ (𝜑 → (𝑆 D (𝑋 × {𝐴})) = (𝑋 × {0})) |
| 73 | 72 | feq1d 6720 |
. . . . 5
⊢ (𝜑 → ((𝑆 D (𝑋 × {𝐴})):𝑋⟶{0} ↔ (𝑋 × {0}):𝑋⟶{0})) |
| 74 | 9, 73 | mpbiri 258 |
. . . 4
⊢ (𝜑 → (𝑆 D (𝑋 × {𝐴})):𝑋⟶{0}) |
| 75 | 74 | fdmd 6746 |
. . 3
⊢ (𝜑 → dom (𝑆 D (𝑋 × {𝐴})) = 𝑋) |
| 76 | 1, 6, 7, 75, 16 | dvmulf 25980 |
. 2
⊢ (𝜑 → (𝑆 D ((𝑋 × {𝐴}) ∘f · 𝐹)) = (((𝑆 D (𝑋 × {𝐴})) ∘f · 𝐹) ∘f + ((𝑆 D 𝐹) ∘f · (𝑋 × {𝐴})))) |
| 77 | | sseqin2 4223 |
. . . . . 6
⊢ (𝑋 ⊆ 𝑆 ↔ (𝑆 ∩ 𝑋) = 𝑋) |
| 78 | 19, 77 | sylib 218 |
. . . . 5
⊢ (𝜑 → (𝑆 ∩ 𝑋) = 𝑋) |
| 79 | 78 | mpteq1d 5237 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝑆 ∩ 𝑋) ↦ (𝐴 · (𝐹‘𝑥))) = (𝑥 ∈ 𝑋 ↦ (𝐴 · (𝐹‘𝑥)))) |
| 80 | 13 | ffnd 6737 |
. . . . 5
⊢ (𝜑 → (𝑆 × {𝐴}) Fn 𝑆) |
| 81 | 7 | ffnd 6737 |
. . . . 5
⊢ (𝜑 → 𝐹 Fn 𝑋) |
| 82 | 1, 19 | ssexd 5324 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ V) |
| 83 | | eqid 2737 |
. . . . 5
⊢ (𝑆 ∩ 𝑋) = (𝑆 ∩ 𝑋) |
| 84 | | fvconst2g 7222 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((𝑆 × {𝐴})‘𝑥) = 𝐴) |
| 85 | 2, 84 | sylan 580 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((𝑆 × {𝐴})‘𝑥) = 𝐴) |
| 86 | | eqidd 2738 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) = (𝐹‘𝑥)) |
| 87 | 80, 81, 1, 82, 83, 85, 86 | offval 7706 |
. . . 4
⊢ (𝜑 → ((𝑆 × {𝐴}) ∘f · 𝐹) = (𝑥 ∈ (𝑆 ∩ 𝑋) ↦ (𝐴 · (𝐹‘𝑥)))) |
| 88 | 4 | ffnd 6737 |
. . . . 5
⊢ (𝜑 → (𝑋 × {𝐴}) Fn 𝑋) |
| 89 | | inidm 4227 |
. . . . 5
⊢ (𝑋 ∩ 𝑋) = 𝑋 |
| 90 | | fvconst2g 7222 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑋) → ((𝑋 × {𝐴})‘𝑥) = 𝐴) |
| 91 | 2, 90 | sylan 580 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑋 × {𝐴})‘𝑥) = 𝐴) |
| 92 | 88, 81, 82, 82, 89, 91, 86 | offval 7706 |
. . . 4
⊢ (𝜑 → ((𝑋 × {𝐴}) ∘f · 𝐹) = (𝑥 ∈ 𝑋 ↦ (𝐴 · (𝐹‘𝑥)))) |
| 93 | 79, 87, 92 | 3eqtr4d 2787 |
. . 3
⊢ (𝜑 → ((𝑆 × {𝐴}) ∘f · 𝐹) = ((𝑋 × {𝐴}) ∘f · 𝐹)) |
| 94 | 93 | oveq2d 7447 |
. 2
⊢ (𝜑 → (𝑆 D ((𝑆 × {𝐴}) ∘f · 𝐹)) = (𝑆 D ((𝑋 × {𝐴}) ∘f · 𝐹))) |
| 95 | 78 | mpteq1d 5237 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝑆 ∩ 𝑋) ↦ (𝐴 · ((𝑆 D 𝐹)‘𝑥))) = (𝑥 ∈ 𝑋 ↦ (𝐴 · ((𝑆 D 𝐹)‘𝑥)))) |
| 96 | | dvfg 25941 |
. . . . . . 7
⊢ (𝑆 ∈ {ℝ, ℂ}
→ (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ) |
| 97 | 1, 96 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ) |
| 98 | 16 | feq2d 6722 |
. . . . . 6
⊢ (𝜑 → ((𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ ↔ (𝑆 D 𝐹):𝑋⟶ℂ)) |
| 99 | 97, 98 | mpbid 232 |
. . . . 5
⊢ (𝜑 → (𝑆 D 𝐹):𝑋⟶ℂ) |
| 100 | 99 | ffnd 6737 |
. . . 4
⊢ (𝜑 → (𝑆 D 𝐹) Fn 𝑋) |
| 101 | | eqidd 2738 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑆 D 𝐹)‘𝑥) = ((𝑆 D 𝐹)‘𝑥)) |
| 102 | 80, 100, 1, 82, 83, 85, 101 | offval 7706 |
. . 3
⊢ (𝜑 → ((𝑆 × {𝐴}) ∘f · (𝑆 D 𝐹)) = (𝑥 ∈ (𝑆 ∩ 𝑋) ↦ (𝐴 · ((𝑆 D 𝐹)‘𝑥)))) |
| 103 | | 0cnd 11254 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 0 ∈ ℂ) |
| 104 | | ovexd 7466 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((𝑆 D 𝐹)‘𝑥) · 𝐴) ∈ V) |
| 105 | 72 | oveq1d 7446 |
. . . . . . 7
⊢ (𝜑 → ((𝑆 D (𝑋 × {𝐴})) ∘f · 𝐹) = ((𝑋 × {0}) ∘f ·
𝐹)) |
| 106 | | 0cnd 11254 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
ℂ) |
| 107 | | mul02 11439 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℂ → (0
· 𝑥) =
0) |
| 108 | 107 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (0 · 𝑥) = 0) |
| 109 | 82, 7, 106, 106, 108 | caofid2 7733 |
. . . . . . 7
⊢ (𝜑 → ((𝑋 × {0}) ∘f ·
𝐹) = (𝑋 × {0})) |
| 110 | 105, 109 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → ((𝑆 D (𝑋 × {𝐴})) ∘f · 𝐹) = (𝑋 × {0})) |
| 111 | 110, 69 | eqtrdi 2793 |
. . . . 5
⊢ (𝜑 → ((𝑆 D (𝑋 × {𝐴})) ∘f · 𝐹) = (𝑥 ∈ 𝑋 ↦ 0)) |
| 112 | | fvexd 6921 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑆 D 𝐹)‘𝑥) ∈ V) |
| 113 | 2 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) |
| 114 | 99 | feqmptd 6977 |
. . . . . 6
⊢ (𝜑 → (𝑆 D 𝐹) = (𝑥 ∈ 𝑋 ↦ ((𝑆 D 𝐹)‘𝑥))) |
| 115 | 27 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝑋 × {𝐴}) = (𝑥 ∈ 𝑋 ↦ 𝐴)) |
| 116 | 82, 112, 113, 114, 115 | offval2 7717 |
. . . . 5
⊢ (𝜑 → ((𝑆 D 𝐹) ∘f · (𝑋 × {𝐴})) = (𝑥 ∈ 𝑋 ↦ (((𝑆 D 𝐹)‘𝑥) · 𝐴))) |
| 117 | 82, 103, 104, 111, 116 | offval2 7717 |
. . . 4
⊢ (𝜑 → (((𝑆 D (𝑋 × {𝐴})) ∘f · 𝐹) ∘f + ((𝑆 D 𝐹) ∘f · (𝑋 × {𝐴}))) = (𝑥 ∈ 𝑋 ↦ (0 + (((𝑆 D 𝐹)‘𝑥) · 𝐴)))) |
| 118 | 99 | ffvelcdmda 7104 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑆 D 𝐹)‘𝑥) ∈ ℂ) |
| 119 | 118, 113 | mulcld 11281 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((𝑆 D 𝐹)‘𝑥) · 𝐴) ∈ ℂ) |
| 120 | 119 | addlidd 11462 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (0 + (((𝑆 D 𝐹)‘𝑥) · 𝐴)) = (((𝑆 D 𝐹)‘𝑥) · 𝐴)) |
| 121 | 118, 113 | mulcomd 11282 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((𝑆 D 𝐹)‘𝑥) · 𝐴) = (𝐴 · ((𝑆 D 𝐹)‘𝑥))) |
| 122 | 120, 121 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (0 + (((𝑆 D 𝐹)‘𝑥) · 𝐴)) = (𝐴 · ((𝑆 D 𝐹)‘𝑥))) |
| 123 | 122 | mpteq2dva 5242 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (0 + (((𝑆 D 𝐹)‘𝑥) · 𝐴))) = (𝑥 ∈ 𝑋 ↦ (𝐴 · ((𝑆 D 𝐹)‘𝑥)))) |
| 124 | 117, 123 | eqtrd 2777 |
. . 3
⊢ (𝜑 → (((𝑆 D (𝑋 × {𝐴})) ∘f · 𝐹) ∘f + ((𝑆 D 𝐹) ∘f · (𝑋 × {𝐴}))) = (𝑥 ∈ 𝑋 ↦ (𝐴 · ((𝑆 D 𝐹)‘𝑥)))) |
| 125 | 95, 102, 124 | 3eqtr4d 2787 |
. 2
⊢ (𝜑 → ((𝑆 × {𝐴}) ∘f · (𝑆 D 𝐹)) = (((𝑆 D (𝑋 × {𝐴})) ∘f · 𝐹) ∘f + ((𝑆 D 𝐹) ∘f · (𝑋 × {𝐴})))) |
| 126 | 76, 94, 125 | 3eqtr4d 2787 |
1
⊢ (𝜑 → (𝑆 D ((𝑆 × {𝐴}) ∘f · 𝐹)) = ((𝑆 × {𝐴}) ∘f · (𝑆 D 𝐹))) |