Step | Hyp | Ref
| Expression |
1 | | dvcof.f |
. . . . 5
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) |
2 | 1 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝐹:𝑋⟶ℂ) |
3 | | dvcof.df |
. . . . . 6
⊢ (𝜑 → dom (𝑆 D 𝐹) = 𝑋) |
4 | | dvbsss 23666 |
. . . . . 6
⊢ dom
(𝑆 D 𝐹) ⊆ 𝑆 |
5 | 3, 4 | syl6eqssr 3656 |
. . . . 5
⊢ (𝜑 → 𝑋 ⊆ 𝑆) |
6 | 5 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑋 ⊆ 𝑆) |
7 | | dvcof.g |
. . . . 5
⊢ (𝜑 → 𝐺:𝑌⟶𝑋) |
8 | 7 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝐺:𝑌⟶𝑋) |
9 | | dvcof.dg |
. . . . . 6
⊢ (𝜑 → dom (𝑇 D 𝐺) = 𝑌) |
10 | | dvbsss 23666 |
. . . . . 6
⊢ dom
(𝑇 D 𝐺) ⊆ 𝑇 |
11 | 9, 10 | syl6eqssr 3656 |
. . . . 5
⊢ (𝜑 → 𝑌 ⊆ 𝑇) |
12 | 11 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑌 ⊆ 𝑇) |
13 | | dvcof.s |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
14 | 13 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑆 ∈ {ℝ, ℂ}) |
15 | | dvcof.t |
. . . . 5
⊢ (𝜑 → 𝑇 ∈ {ℝ, ℂ}) |
16 | 15 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑇 ∈ {ℝ, ℂ}) |
17 | 7 | ffvelrnda 6359 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝐺‘𝑥) ∈ 𝑋) |
18 | 3 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → dom (𝑆 D 𝐹) = 𝑋) |
19 | 17, 18 | eleqtrrd 2704 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝐺‘𝑥) ∈ dom (𝑆 D 𝐹)) |
20 | 9 | eleq2d 2687 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ dom (𝑇 D 𝐺) ↔ 𝑥 ∈ 𝑌)) |
21 | 20 | biimpar 502 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑥 ∈ dom (𝑇 D 𝐺)) |
22 | 2, 6, 8, 12, 14, 16, 19, 21 | dvco 23710 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ((𝑇 D (𝐹 ∘ 𝐺))‘𝑥) = (((𝑆 D 𝐹)‘(𝐺‘𝑥)) · ((𝑇 D 𝐺)‘𝑥))) |
23 | 22 | mpteq2dva 4744 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑌 ↦ ((𝑇 D (𝐹 ∘ 𝐺))‘𝑥)) = (𝑥 ∈ 𝑌 ↦ (((𝑆 D 𝐹)‘(𝐺‘𝑥)) · ((𝑇 D 𝐺)‘𝑥)))) |
24 | | dvfg 23670 |
. . . . 5
⊢ (𝑇 ∈ {ℝ, ℂ}
→ (𝑇 D (𝐹 ∘ 𝐺)):dom (𝑇 D (𝐹 ∘ 𝐺))⟶ℂ) |
25 | 15, 24 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑇 D (𝐹 ∘ 𝐺)):dom (𝑇 D (𝐹 ∘ 𝐺))⟶ℂ) |
26 | | recnprss 23668 |
. . . . . . . 8
⊢ (𝑇 ∈ {ℝ, ℂ}
→ 𝑇 ⊆
ℂ) |
27 | 15, 26 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ⊆ ℂ) |
28 | | fco 6058 |
. . . . . . . 8
⊢ ((𝐹:𝑋⟶ℂ ∧ 𝐺:𝑌⟶𝑋) → (𝐹 ∘ 𝐺):𝑌⟶ℂ) |
29 | 1, 7, 28 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ∘ 𝐺):𝑌⟶ℂ) |
30 | 27, 29, 11 | dvbss 23665 |
. . . . . 6
⊢ (𝜑 → dom (𝑇 D (𝐹 ∘ 𝐺)) ⊆ 𝑌) |
31 | | recnprss 23668 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
32 | 14, 31 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑆 ⊆ ℂ) |
33 | 16, 26 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑇 ⊆ ℂ) |
34 | | fvexd 6203 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ((𝑆 D 𝐹)‘(𝐺‘𝑥)) ∈ V) |
35 | | fvexd 6203 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ((𝑇 D 𝐺)‘𝑥) ∈ V) |
36 | | dvfg 23670 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ {ℝ, ℂ}
→ (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ) |
37 | | ffun 6048 |
. . . . . . . . . . . 12
⊢ ((𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ → Fun (𝑆 D 𝐹)) |
38 | | funfvbrb 6330 |
. . . . . . . . . . . 12
⊢ (Fun
(𝑆 D 𝐹) → ((𝐺‘𝑥) ∈ dom (𝑆 D 𝐹) ↔ (𝐺‘𝑥)(𝑆 D 𝐹)((𝑆 D 𝐹)‘(𝐺‘𝑥)))) |
39 | 14, 36, 37, 38 | 4syl 19 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ((𝐺‘𝑥) ∈ dom (𝑆 D 𝐹) ↔ (𝐺‘𝑥)(𝑆 D 𝐹)((𝑆 D 𝐹)‘(𝐺‘𝑥)))) |
40 | 19, 39 | mpbid 222 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝐺‘𝑥)(𝑆 D 𝐹)((𝑆 D 𝐹)‘(𝐺‘𝑥))) |
41 | | dvfg 23670 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ {ℝ, ℂ}
→ (𝑇 D 𝐺):dom (𝑇 D 𝐺)⟶ℂ) |
42 | | ffun 6048 |
. . . . . . . . . . . 12
⊢ ((𝑇 D 𝐺):dom (𝑇 D 𝐺)⟶ℂ → Fun (𝑇 D 𝐺)) |
43 | | funfvbrb 6330 |
. . . . . . . . . . . 12
⊢ (Fun
(𝑇 D 𝐺) → (𝑥 ∈ dom (𝑇 D 𝐺) ↔ 𝑥(𝑇 D 𝐺)((𝑇 D 𝐺)‘𝑥))) |
44 | 16, 41, 42, 43 | 4syl 19 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝑥 ∈ dom (𝑇 D 𝐺) ↔ 𝑥(𝑇 D 𝐺)((𝑇 D 𝐺)‘𝑥))) |
45 | 21, 44 | mpbid 222 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑥(𝑇 D 𝐺)((𝑇 D 𝐺)‘𝑥)) |
46 | | eqid 2622 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
47 | 2, 6, 8, 12, 32, 33, 34, 35, 40, 45, 46 | dvcobr 23709 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑥(𝑇 D (𝐹 ∘ 𝐺))(((𝑆 D 𝐹)‘(𝐺‘𝑥)) · ((𝑇 D 𝐺)‘𝑥))) |
48 | | reldv 23634 |
. . . . . . . . . 10
⊢ Rel
(𝑇 D (𝐹 ∘ 𝐺)) |
49 | 48 | releldmi 5362 |
. . . . . . . . 9
⊢ (𝑥(𝑇 D (𝐹 ∘ 𝐺))(((𝑆 D 𝐹)‘(𝐺‘𝑥)) · ((𝑇 D 𝐺)‘𝑥)) → 𝑥 ∈ dom (𝑇 D (𝐹 ∘ 𝐺))) |
50 | 47, 49 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑥 ∈ dom (𝑇 D (𝐹 ∘ 𝐺))) |
51 | 50 | ex 450 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝑌 → 𝑥 ∈ dom (𝑇 D (𝐹 ∘ 𝐺)))) |
52 | 51 | ssrdv 3609 |
. . . . . 6
⊢ (𝜑 → 𝑌 ⊆ dom (𝑇 D (𝐹 ∘ 𝐺))) |
53 | 30, 52 | eqssd 3620 |
. . . . 5
⊢ (𝜑 → dom (𝑇 D (𝐹 ∘ 𝐺)) = 𝑌) |
54 | 53 | feq2d 6031 |
. . . 4
⊢ (𝜑 → ((𝑇 D (𝐹 ∘ 𝐺)):dom (𝑇 D (𝐹 ∘ 𝐺))⟶ℂ ↔ (𝑇 D (𝐹 ∘ 𝐺)):𝑌⟶ℂ)) |
55 | 25, 54 | mpbid 222 |
. . 3
⊢ (𝜑 → (𝑇 D (𝐹 ∘ 𝐺)):𝑌⟶ℂ) |
56 | 55 | feqmptd 6249 |
. 2
⊢ (𝜑 → (𝑇 D (𝐹 ∘ 𝐺)) = (𝑥 ∈ 𝑌 ↦ ((𝑇 D (𝐹 ∘ 𝐺))‘𝑥))) |
57 | 15, 11 | ssexd 4805 |
. . 3
⊢ (𝜑 → 𝑌 ∈ V) |
58 | 7 | feqmptd 6249 |
. . . 4
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝑌 ↦ (𝐺‘𝑥))) |
59 | 13, 36 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ) |
60 | 3 | feq2d 6031 |
. . . . . 6
⊢ (𝜑 → ((𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ ↔ (𝑆 D 𝐹):𝑋⟶ℂ)) |
61 | 59, 60 | mpbid 222 |
. . . . 5
⊢ (𝜑 → (𝑆 D 𝐹):𝑋⟶ℂ) |
62 | 61 | feqmptd 6249 |
. . . 4
⊢ (𝜑 → (𝑆 D 𝐹) = (𝑦 ∈ 𝑋 ↦ ((𝑆 D 𝐹)‘𝑦))) |
63 | | fveq2 6191 |
. . . 4
⊢ (𝑦 = (𝐺‘𝑥) → ((𝑆 D 𝐹)‘𝑦) = ((𝑆 D 𝐹)‘(𝐺‘𝑥))) |
64 | 17, 58, 62, 63 | fmptco 6396 |
. . 3
⊢ (𝜑 → ((𝑆 D 𝐹) ∘ 𝐺) = (𝑥 ∈ 𝑌 ↦ ((𝑆 D 𝐹)‘(𝐺‘𝑥)))) |
65 | 15, 41 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑇 D 𝐺):dom (𝑇 D 𝐺)⟶ℂ) |
66 | 9 | feq2d 6031 |
. . . . 5
⊢ (𝜑 → ((𝑇 D 𝐺):dom (𝑇 D 𝐺)⟶ℂ ↔ (𝑇 D 𝐺):𝑌⟶ℂ)) |
67 | 65, 66 | mpbid 222 |
. . . 4
⊢ (𝜑 → (𝑇 D 𝐺):𝑌⟶ℂ) |
68 | 67 | feqmptd 6249 |
. . 3
⊢ (𝜑 → (𝑇 D 𝐺) = (𝑥 ∈ 𝑌 ↦ ((𝑇 D 𝐺)‘𝑥))) |
69 | 57, 34, 35, 64, 68 | offval2 6914 |
. 2
⊢ (𝜑 → (((𝑆 D 𝐹) ∘ 𝐺) ∘𝑓 ·
(𝑇 D 𝐺)) = (𝑥 ∈ 𝑌 ↦ (((𝑆 D 𝐹)‘(𝐺‘𝑥)) · ((𝑇 D 𝐺)‘𝑥)))) |
70 | 23, 56, 69 | 3eqtr4d 2666 |
1
⊢ (𝜑 → (𝑇 D (𝐹 ∘ 𝐺)) = (((𝑆 D 𝐹) ∘ 𝐺) ∘𝑓 ·
(𝑇 D 𝐺))) |