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