Step | Hyp | Ref
| Expression |
1 | | dvf 23671 |
. . . . 5
⊢ (ℝ
D 𝐺):dom (ℝ D 𝐺)⟶ℂ |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝜑 → (ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ) |
3 | | ffun 6048 |
. . . 4
⊢ ((ℝ
D 𝐺):dom (ℝ D 𝐺)⟶ℂ → Fun
(ℝ D 𝐺)) |
4 | 2, 3 | syl 17 |
. . 3
⊢ (𝜑 → Fun (ℝ D 𝐺)) |
5 | | ax-resscn 9993 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
6 | 5 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℝ ⊆
ℂ) |
7 | | ftc1cn.g |
. . . . . . 7
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) |
8 | | ftc1cn.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) |
9 | | ftc1cn.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℝ) |
10 | | ftc1cn.le |
. . . . . . 7
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
11 | | ssid 3624 |
. . . . . . . 8
⊢ (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵) |
12 | 11 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵)) |
13 | | ioossre 12235 |
. . . . . . . 8
⊢ (𝐴(,)𝐵) ⊆ ℝ |
14 | 13 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ) |
15 | | ftc1cn.i |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈
𝐿1) |
16 | | ftc1cn.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
17 | | cncff 22696 |
. . . . . . . 8
⊢ (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ) → 𝐹:(𝐴(,)𝐵)⟶ℂ) |
18 | 16, 17 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℂ) |
19 | 7, 8, 9, 10, 12, 14, 15, 18 | ftc1lem2 23799 |
. . . . . 6
⊢ (𝜑 → 𝐺:(𝐴[,]𝐵)⟶ℂ) |
20 | | iccssre 12255 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
21 | 8, 9, 20 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
22 | | eqid 2622 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
23 | 22 | tgioo2 22606 |
. . . . . 6
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
24 | 6, 19, 21, 23, 22 | dvbssntr 23664 |
. . . . 5
⊢ (𝜑 → dom (ℝ D 𝐺) ⊆
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) |
25 | | iccntr 22624 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
26 | 8, 9, 25 | syl2anc 693 |
. . . . 5
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
27 | 24, 26 | sseqtrd 3641 |
. . . 4
⊢ (𝜑 → dom (ℝ D 𝐺) ⊆ (𝐴(,)𝐵)) |
28 | 8 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ) |
29 | 9 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ) |
30 | 10 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝐴 ≤ 𝐵) |
31 | 11 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵)) |
32 | 13 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐴(,)𝐵) ⊆ ℝ) |
33 | 15 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝐹 ∈
𝐿1) |
34 | | simpr 477 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ (𝐴(,)𝐵)) |
35 | 13, 5 | sstri 3612 |
. . . . . . . . . . . 12
⊢ (𝐴(,)𝐵) ⊆ ℂ |
36 | | ssid 3624 |
. . . . . . . . . . . 12
⊢ ℂ
⊆ ℂ |
37 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld)
↾t (𝐴(,)𝐵)) |
38 | 22 | cnfldtop 22587 |
. . . . . . . . . . . . . . 15
⊢
(TopOpen‘ℂfld) ∈ Top |
39 | 22 | cnfldtopon 22586 |
. . . . . . . . . . . . . . . . 17
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
40 | 39 | toponunii 20721 |
. . . . . . . . . . . . . . . 16
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
41 | 40 | restid 16094 |
. . . . . . . . . . . . . . 15
⊢
((TopOpen‘ℂfld) ∈ Top →
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) |
42 | 38, 41 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) |
43 | 42 | eqcomi 2631 |
. . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
44 | 22, 37, 43 | cncfcn 22712 |
. . . . . . . . . . . 12
⊢ (((𝐴(,)𝐵) ⊆ ℂ ∧ ℂ ⊆
ℂ) → ((𝐴(,)𝐵)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) |
45 | 35, 36, 44 | mp2an 708 |
. . . . . . . . . . 11
⊢ ((𝐴(,)𝐵)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld)) |
46 | 16, 45 | syl6eleq 2711 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) |
47 | 46 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝐹 ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) |
48 | 35 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℂ) |
49 | | resttopon 20965 |
. . . . . . . . . . . . 13
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ (𝐴(,)𝐵) ⊆ ℂ) →
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵))) |
50 | 39, 48, 49 | sylancr 695 |
. . . . . . . . . . . 12
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵))) |
51 | | toponuni 20719 |
. . . . . . . . . . . 12
⊢
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵)) → (𝐴(,)𝐵) = ∪
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵))) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴(,)𝐵) = ∪
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵))) |
53 | 52 | eleq2d 2687 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↔ 𝑦 ∈ ∪
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)))) |
54 | 53 | biimpa 501 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ ∪
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵))) |
55 | | eqid 2622 |
. . . . . . . . . 10
⊢ ∪ ((TopOpen‘ℂfld)
↾t (𝐴(,)𝐵)) = ∪
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) |
56 | 55 | cncnpi 21082 |
. . . . . . . . 9
⊢ ((𝐹 ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld))
∧ 𝑦 ∈ ∪ ((TopOpen‘ℂfld)
↾t (𝐴(,)𝐵))) → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) |
57 | 47, 54, 56 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) |
58 | 7, 28, 29, 30, 31, 32, 33, 34, 57, 23, 37, 22 | ftc1 23805 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝑦(ℝ D 𝐺)(𝐹‘𝑦)) |
59 | | vex 3203 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
60 | | fvex 6201 |
. . . . . . . 8
⊢ (𝐹‘𝑦) ∈ V |
61 | 59, 60 | breldm 5329 |
. . . . . . 7
⊢ (𝑦(ℝ D 𝐺)(𝐹‘𝑦) → 𝑦 ∈ dom (ℝ D 𝐺)) |
62 | 58, 61 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ dom (ℝ D 𝐺)) |
63 | 62 | ex 450 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) → 𝑦 ∈ dom (ℝ D 𝐺))) |
64 | 63 | ssrdv 3609 |
. . . 4
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ dom (ℝ D 𝐺)) |
65 | 27, 64 | eqssd 3620 |
. . 3
⊢ (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵)) |
66 | | df-fn 5891 |
. . 3
⊢ ((ℝ
D 𝐺) Fn (𝐴(,)𝐵) ↔ (Fun (ℝ D 𝐺) ∧ dom (ℝ D 𝐺) = (𝐴(,)𝐵))) |
67 | 4, 65, 66 | sylanbrc 698 |
. 2
⊢ (𝜑 → (ℝ D 𝐺) Fn (𝐴(,)𝐵)) |
68 | | ffn 6045 |
. . 3
⊢ (𝐹:(𝐴(,)𝐵)⟶ℂ → 𝐹 Fn (𝐴(,)𝐵)) |
69 | 18, 68 | syl 17 |
. 2
⊢ (𝜑 → 𝐹 Fn (𝐴(,)𝐵)) |
70 | 4 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → Fun (ℝ D 𝐺)) |
71 | | funbrfv 6234 |
. . 3
⊢ (Fun
(ℝ D 𝐺) → (𝑦(ℝ D 𝐺)(𝐹‘𝑦) → ((ℝ D 𝐺)‘𝑦) = (𝐹‘𝑦))) |
72 | 70, 58, 71 | sylc 65 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑦) = (𝐹‘𝑦)) |
73 | 67, 69, 72 | eqfnfvd 6314 |
1
⊢ (𝜑 → (ℝ D 𝐺) = 𝐹) |