| Step | Hyp | Ref
| Expression |
| 1 | | fveq2 6906 |
. . . 4
⊢ (𝑢 = 𝑤 → (𝐺‘𝑢) = (𝐺‘𝑤)) |
| 2 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑤(𝐺‘𝑢) |
| 3 | | itgsubsticclem.2 |
. . . . . 6
⊢ 𝐺 = (𝑢 ∈ ℝ ↦ if(𝑢 ∈ (𝐾[,]𝐿), (𝐹‘𝑢), if(𝑢 < 𝐾, (𝐹‘𝐾), (𝐹‘𝐿)))) |
| 4 | | nfmpt1 5250 |
. . . . . 6
⊢
Ⅎ𝑢(𝑢 ∈ ℝ ↦ if(𝑢 ∈ (𝐾[,]𝐿), (𝐹‘𝑢), if(𝑢 < 𝐾, (𝐹‘𝐾), (𝐹‘𝐿)))) |
| 5 | 3, 4 | nfcxfr 2903 |
. . . . 5
⊢
Ⅎ𝑢𝐺 |
| 6 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑢𝑤 |
| 7 | 5, 6 | nffv 6916 |
. . . 4
⊢
Ⅎ𝑢(𝐺‘𝑤) |
| 8 | 1, 2, 7 | cbvditg 25889 |
. . 3
⊢
⨜[𝐾 →
𝐿](𝐺‘𝑢) d𝑢 = ⨜[𝐾 → 𝐿](𝐺‘𝑤) d𝑤 |
| 9 | | itgsubsticclem.11 |
. . . 4
⊢ (𝜑 → 𝐾 ≤ 𝐿) |
| 10 | | itgsubsticclem.9 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ ℝ) |
| 11 | | itgsubsticclem.10 |
. . . . . . . . 9
⊢ (𝜑 → 𝐿 ∈ ℝ) |
| 12 | 10, 11 | iccssred 13474 |
. . . . . . . 8
⊢ (𝜑 → (𝐾[,]𝐿) ⊆ ℝ) |
| 13 | 12 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐾(,)𝐿)) → (𝐾[,]𝐿) ⊆ ℝ) |
| 14 | | ioossicc 13473 |
. . . . . . . . 9
⊢ (𝐾(,)𝐿) ⊆ (𝐾[,]𝐿) |
| 15 | 14 | sseli 3979 |
. . . . . . . 8
⊢ (𝑢 ∈ (𝐾(,)𝐿) → 𝑢 ∈ (𝐾[,]𝐿)) |
| 16 | 15 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐾(,)𝐿)) → 𝑢 ∈ (𝐾[,]𝐿)) |
| 17 | 13, 16 | sseldd 3984 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐾(,)𝐿)) → 𝑢 ∈ ℝ) |
| 18 | 16 | iftrued 4533 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐾(,)𝐿)) → if(𝑢 ∈ (𝐾[,]𝐿), (𝐹‘𝑢), if(𝑢 < 𝐾, (𝐹‘𝐾), (𝐹‘𝐿))) = (𝐹‘𝑢)) |
| 19 | | itgsubsticclem.1 |
. . . . . . . . . . . . 13
⊢ 𝐹 = (𝑢 ∈ (𝐾[,]𝐿) ↦ 𝐶) |
| 20 | 19 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 = (𝑢 ∈ (𝐾[,]𝐿) ↦ 𝐶)) |
| 21 | | itgsubsticclem.8 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ ((𝐾[,]𝐿)–cn→ℂ)) |
| 22 | | cncff 24919 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ ((𝐾[,]𝐿)–cn→ℂ) → 𝐹:(𝐾[,]𝐿)⟶ℂ) |
| 23 | 21, 22 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:(𝐾[,]𝐿)⟶ℂ) |
| 24 | 20, 23 | feq1dd 6721 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑢 ∈ (𝐾[,]𝐿) ↦ 𝐶):(𝐾[,]𝐿)⟶ℂ) |
| 25 | 24 | fvmptelcdm 7133 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐾[,]𝐿)) → 𝐶 ∈ ℂ) |
| 26 | 16, 25 | syldan 591 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐾(,)𝐿)) → 𝐶 ∈ ℂ) |
| 27 | 19 | fvmpt2 7027 |
. . . . . . . . 9
⊢ ((𝑢 ∈ (𝐾[,]𝐿) ∧ 𝐶 ∈ ℂ) → (𝐹‘𝑢) = 𝐶) |
| 28 | 16, 26, 27 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐾(,)𝐿)) → (𝐹‘𝑢) = 𝐶) |
| 29 | 28, 26 | eqeltrd 2841 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐾(,)𝐿)) → (𝐹‘𝑢) ∈ ℂ) |
| 30 | 18, 29 | eqeltrd 2841 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐾(,)𝐿)) → if(𝑢 ∈ (𝐾[,]𝐿), (𝐹‘𝑢), if(𝑢 < 𝐾, (𝐹‘𝐾), (𝐹‘𝐿))) ∈ ℂ) |
| 31 | 3 | fvmpt2 7027 |
. . . . . 6
⊢ ((𝑢 ∈ ℝ ∧ if(𝑢 ∈ (𝐾[,]𝐿), (𝐹‘𝑢), if(𝑢 < 𝐾, (𝐹‘𝐾), (𝐹‘𝐿))) ∈ ℂ) → (𝐺‘𝑢) = if(𝑢 ∈ (𝐾[,]𝐿), (𝐹‘𝑢), if(𝑢 < 𝐾, (𝐹‘𝐾), (𝐹‘𝐿)))) |
| 32 | 17, 30, 31 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐾(,)𝐿)) → (𝐺‘𝑢) = if(𝑢 ∈ (𝐾[,]𝐿), (𝐹‘𝑢), if(𝑢 < 𝐾, (𝐹‘𝐾), (𝐹‘𝐿)))) |
| 33 | 32, 18, 28 | 3eqtrd 2781 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐾(,)𝐿)) → (𝐺‘𝑢) = 𝐶) |
| 34 | 9, 33 | ditgeq3d 45979 |
. . 3
⊢ (𝜑 → ⨜[𝐾 → 𝐿](𝐺‘𝑢) d𝑢 = ⨜[𝐾 → 𝐿]𝐶 d𝑢) |
| 35 | | itgsubsticclem.3 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ ℝ) |
| 36 | | itgsubsticclem.4 |
. . . 4
⊢ (𝜑 → 𝑌 ∈ ℝ) |
| 37 | | itgsubsticclem.5 |
. . . 4
⊢ (𝜑 → 𝑋 ≤ 𝑌) |
| 38 | | mnfxr 11318 |
. . . . 5
⊢ -∞
∈ ℝ* |
| 39 | 38 | a1i 11 |
. . . 4
⊢ (𝜑 → -∞ ∈
ℝ*) |
| 40 | | pnfxr 11315 |
. . . . 5
⊢ +∞
∈ ℝ* |
| 41 | 40 | a1i 11 |
. . . 4
⊢ (𝜑 → +∞ ∈
ℝ*) |
| 42 | | ioomax 13462 |
. . . . . . . . 9
⊢
(-∞(,)+∞) = ℝ |
| 43 | 42 | eqcomi 2746 |
. . . . . . . 8
⊢ ℝ =
(-∞(,)+∞) |
| 44 | 43 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ =
(-∞(,)+∞)) |
| 45 | 12, 44 | sseqtrd 4020 |
. . . . . 6
⊢ (𝜑 → (𝐾[,]𝐿) ⊆
(-∞(,)+∞)) |
| 46 | | ax-resscn 11212 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
| 47 | 44, 46 | eqsstrrdi 4029 |
. . . . . 6
⊢ (𝜑 → (-∞(,)+∞)
⊆ ℂ) |
| 48 | | cncfss 24925 |
. . . . . 6
⊢ (((𝐾[,]𝐿) ⊆ (-∞(,)+∞) ∧
(-∞(,)+∞) ⊆ ℂ) → ((𝑋[,]𝑌)–cn→(𝐾[,]𝐿)) ⊆ ((𝑋[,]𝑌)–cn→(-∞(,)+∞))) |
| 49 | 45, 47, 48 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → ((𝑋[,]𝑌)–cn→(𝐾[,]𝐿)) ⊆ ((𝑋[,]𝑌)–cn→(-∞(,)+∞))) |
| 50 | | itgsubsticclem.6 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝐾[,]𝐿))) |
| 51 | 49, 50 | sseldd 3984 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(-∞(,)+∞))) |
| 52 | | itgsubsticclem.7 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ (((𝑋(,)𝑌)–cn→ℂ) ∩
𝐿1)) |
| 53 | | nfmpt1 5250 |
. . . . . . . . . . 11
⊢
Ⅎ𝑢(𝑢 ∈ (𝐾[,]𝐿) ↦ 𝐶) |
| 54 | 19, 53 | nfcxfr 2903 |
. . . . . . . . . 10
⊢
Ⅎ𝑢𝐹 |
| 55 | | eqid 2737 |
. . . . . . . . . 10
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
| 56 | | eqid 2737 |
. . . . . . . . . 10
⊢ ∪ (TopOpen‘ℂfld) = ∪ (TopOpen‘ℂfld) |
| 57 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 58 | 57 | cnfldtop 24804 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) ∈ Top |
| 59 | 58 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 →
(TopOpen‘ℂfld) ∈ Top) |
| 60 | 12, 46 | sstrdi 3996 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐾[,]𝐿) ⊆ ℂ) |
| 61 | | ssid 4006 |
. . . . . . . . . . . . 13
⊢ ℂ
⊆ ℂ |
| 62 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
((TopOpen‘ℂfld) ↾t (𝐾[,]𝐿)) = ((TopOpen‘ℂfld)
↾t (𝐾[,]𝐿)) |
| 63 | | unicntop 24806 |
. . . . . . . . . . . . . . . . 17
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
| 64 | 63 | restid 17478 |
. . . . . . . . . . . . . . . 16
⊢
((TopOpen‘ℂfld) ∈ Top →
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) |
| 65 | 58, 64 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) |
| 66 | 65 | eqcomi 2746 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
| 67 | 57, 62, 66 | cncfcn 24936 |
. . . . . . . . . . . . 13
⊢ (((𝐾[,]𝐿) ⊆ ℂ ∧ ℂ ⊆
ℂ) → ((𝐾[,]𝐿)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (𝐾[,]𝐿)) Cn
(TopOpen‘ℂfld))) |
| 68 | 60, 61, 67 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐾[,]𝐿)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (𝐾[,]𝐿)) Cn
(TopOpen‘ℂfld))) |
| 69 | | reex 11246 |
. . . . . . . . . . . . . . . 16
⊢ ℝ
∈ V |
| 70 | 69 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ℝ ∈
V) |
| 71 | | restabs 23173 |
. . . . . . . . . . . . . . 15
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ (𝐾[,]𝐿) ⊆ ℝ ∧ ℝ ∈ V)
→ (((TopOpen‘ℂfld) ↾t ℝ)
↾t (𝐾[,]𝐿)) = ((TopOpen‘ℂfld)
↾t (𝐾[,]𝐿))) |
| 72 | 59, 12, 70, 71 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(((TopOpen‘ℂfld) ↾t ℝ)
↾t (𝐾[,]𝐿)) = ((TopOpen‘ℂfld)
↾t (𝐾[,]𝐿))) |
| 73 | | tgioo4 24826 |
. . . . . . . . . . . . . . . . 17
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
| 74 | 73 | eqcomi 2746 |
. . . . . . . . . . . . . . . 16
⊢
((TopOpen‘ℂfld) ↾t ℝ) =
(topGen‘ran (,)) |
| 75 | 74 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t ℝ) =
(topGen‘ran (,))) |
| 76 | 75 | oveq1d 7446 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(((TopOpen‘ℂfld) ↾t ℝ)
↾t (𝐾[,]𝐿)) = ((topGen‘ran (,))
↾t (𝐾[,]𝐿))) |
| 77 | 72, 76 | eqtr3d 2779 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t (𝐾[,]𝐿)) = ((topGen‘ran (,))
↾t (𝐾[,]𝐿))) |
| 78 | 77 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(((TopOpen‘ℂfld) ↾t (𝐾[,]𝐿)) Cn (TopOpen‘ℂfld))
= (((topGen‘ran (,)) ↾t (𝐾[,]𝐿)) Cn
(TopOpen‘ℂfld))) |
| 79 | 68, 78 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐾[,]𝐿)–cn→ℂ) = (((topGen‘ran (,))
↾t (𝐾[,]𝐿)) Cn
(TopOpen‘ℂfld))) |
| 80 | 21, 79 | eleqtrd 2843 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ (((topGen‘ran (,))
↾t (𝐾[,]𝐿)) Cn
(TopOpen‘ℂfld))) |
| 81 | 54, 55, 56, 3, 10, 11, 9, 59, 80 | icccncfext 45902 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺 ∈ ((topGen‘ran (,)) Cn
((TopOpen‘ℂfld) ↾t ran 𝐹)) ∧ (𝐺 ↾ (𝐾[,]𝐿)) = 𝐹)) |
| 82 | 81 | simpld 494 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ ((topGen‘ran (,)) Cn
((TopOpen‘ℂfld) ↾t ran 𝐹))) |
| 83 | | uniretop 24783 |
. . . . . . . . 9
⊢ ℝ =
∪ (topGen‘ran (,)) |
| 84 | | eqid 2737 |
. . . . . . . . 9
⊢ ∪ ((TopOpen‘ℂfld)
↾t ran 𝐹)
= ∪ ((TopOpen‘ℂfld)
↾t ran 𝐹) |
| 85 | 83, 84 | cnf 23254 |
. . . . . . . 8
⊢ (𝐺 ∈ ((topGen‘ran (,))
Cn ((TopOpen‘ℂfld) ↾t ran 𝐹)) → 𝐺:ℝ⟶∪
((TopOpen‘ℂfld) ↾t ran 𝐹)) |
| 86 | 82, 85 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐺:ℝ⟶∪
((TopOpen‘ℂfld) ↾t ran 𝐹)) |
| 87 | 44 | feq2d 6722 |
. . . . . . 7
⊢ (𝜑 → (𝐺:ℝ⟶∪
((TopOpen‘ℂfld) ↾t ran 𝐹) ↔ 𝐺:(-∞(,)+∞)⟶∪ ((TopOpen‘ℂfld)
↾t ran 𝐹))) |
| 88 | 86, 87 | mpbid 232 |
. . . . . 6
⊢ (𝜑 → 𝐺:(-∞(,)+∞)⟶∪ ((TopOpen‘ℂfld)
↾t ran 𝐹)) |
| 89 | 88 | feqmptd 6977 |
. . . . 5
⊢ (𝜑 → 𝐺 = (𝑤 ∈ (-∞(,)+∞) ↦ (𝐺‘𝑤))) |
| 90 | 23 | frnd 6744 |
. . . . . . 7
⊢ (𝜑 → ran 𝐹 ⊆ ℂ) |
| 91 | | cncfss 24925 |
. . . . . . 7
⊢ ((ran
𝐹 ⊆ ℂ ∧
ℂ ⊆ ℂ) → ((-∞(,)+∞)–cn→ran 𝐹) ⊆ ((-∞(,)+∞)–cn→ℂ)) |
| 92 | 90, 61, 91 | sylancl 586 |
. . . . . 6
⊢ (𝜑 →
((-∞(,)+∞)–cn→ran
𝐹) ⊆
((-∞(,)+∞)–cn→ℂ)) |
| 93 | 43 | oveq2i 7442 |
. . . . . . . . . . 11
⊢
((TopOpen‘ℂfld) ↾t ℝ) =
((TopOpen‘ℂfld) ↾t
(-∞(,)+∞)) |
| 94 | 73, 93 | eqtri 2765 |
. . . . . . . . . 10
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t (-∞(,)+∞)) |
| 95 | | eqid 2737 |
. . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ↾t ran 𝐹) =
((TopOpen‘ℂfld) ↾t ran 𝐹) |
| 96 | 57, 94, 95 | cncfcn 24936 |
. . . . . . . . 9
⊢
(((-∞(,)+∞) ⊆ ℂ ∧ ran 𝐹 ⊆ ℂ) →
((-∞(,)+∞)–cn→ran
𝐹) = ((topGen‘ran
(,)) Cn ((TopOpen‘ℂfld) ↾t ran 𝐹))) |
| 97 | 47, 90, 96 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 →
((-∞(,)+∞)–cn→ran
𝐹) = ((topGen‘ran
(,)) Cn ((TopOpen‘ℂfld) ↾t ran 𝐹))) |
| 98 | 97 | eqcomd 2743 |
. . . . . . 7
⊢ (𝜑 → ((topGen‘ran (,)) Cn
((TopOpen‘ℂfld) ↾t ran 𝐹)) =
((-∞(,)+∞)–cn→ran
𝐹)) |
| 99 | 82, 98 | eleqtrd 2843 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ ((-∞(,)+∞)–cn→ran 𝐹)) |
| 100 | 92, 99 | sseldd 3984 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ ((-∞(,)+∞)–cn→ℂ)) |
| 101 | 89, 100 | eqeltrrd 2842 |
. . . 4
⊢ (𝜑 → (𝑤 ∈ (-∞(,)+∞) ↦ (𝐺‘𝑤)) ∈ ((-∞(,)+∞)–cn→ℂ)) |
| 102 | | itgsubsticclem.12 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) |
| 103 | | fveq2 6906 |
. . . 4
⊢ (𝑤 = 𝐴 → (𝐺‘𝑤) = (𝐺‘𝐴)) |
| 104 | | itgsubsticclem.14 |
. . . 4
⊢ (𝑥 = 𝑋 → 𝐴 = 𝐾) |
| 105 | | itgsubsticclem.15 |
. . . 4
⊢ (𝑥 = 𝑌 → 𝐴 = 𝐿) |
| 106 | 35, 36, 37, 39, 41, 51, 52, 101, 102, 103, 104, 105 | itgsubst 26090 |
. . 3
⊢ (𝜑 → ⨜[𝐾 → 𝐿](𝐺‘𝑤) d𝑤 = ⨜[𝑋 → 𝑌]((𝐺‘𝐴) · 𝐵) d𝑥) |
| 107 | 8, 34, 106 | 3eqtr3a 2801 |
. 2
⊢ (𝜑 → ⨜[𝐾 → 𝐿]𝐶 d𝑢 = ⨜[𝑋 → 𝑌]((𝐺‘𝐴) · 𝐵) d𝑥) |
| 108 | 3 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐺 = (𝑢 ∈ ℝ ↦ if(𝑢 ∈ (𝐾[,]𝐿), (𝐹‘𝑢), if(𝑢 < 𝐾, (𝐹‘𝐾), (𝐹‘𝐿))))) |
| 109 | | simpr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 = 𝐴) → 𝑢 = 𝐴) |
| 110 | 57 | cnfldtopon 24803 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
| 111 | 35, 36 | iccssred 13474 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑋[,]𝑌) ⊆ ℝ) |
| 112 | 111, 46 | sstrdi 3996 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋[,]𝑌) ⊆ ℂ) |
| 113 | | resttopon 23169 |
. . . . . . . . . . . . . 14
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ (𝑋[,]𝑌) ⊆ ℂ) →
((TopOpen‘ℂfld) ↾t (𝑋[,]𝑌)) ∈ (TopOn‘(𝑋[,]𝑌))) |
| 114 | 110, 112,
113 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t (𝑋[,]𝑌)) ∈ (TopOn‘(𝑋[,]𝑌))) |
| 115 | | resttopon 23169 |
. . . . . . . . . . . . . 14
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ (𝐾[,]𝐿) ⊆ ℂ) →
((TopOpen‘ℂfld) ↾t (𝐾[,]𝐿)) ∈ (TopOn‘(𝐾[,]𝐿))) |
| 116 | 110, 60, 115 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t (𝐾[,]𝐿)) ∈ (TopOn‘(𝐾[,]𝐿))) |
| 117 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
((TopOpen‘ℂfld) ↾t (𝑋[,]𝑌)) = ((TopOpen‘ℂfld)
↾t (𝑋[,]𝑌)) |
| 118 | 57, 117, 62 | cncfcn 24936 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋[,]𝑌) ⊆ ℂ ∧ (𝐾[,]𝐿) ⊆ ℂ) → ((𝑋[,]𝑌)–cn→(𝐾[,]𝐿)) = (((TopOpen‘ℂfld)
↾t (𝑋[,]𝑌)) Cn ((TopOpen‘ℂfld)
↾t (𝐾[,]𝐿)))) |
| 119 | 112, 60, 118 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑋[,]𝑌)–cn→(𝐾[,]𝐿)) = (((TopOpen‘ℂfld)
↾t (𝑋[,]𝑌)) Cn ((TopOpen‘ℂfld)
↾t (𝐾[,]𝐿)))) |
| 120 | 50, 119 | eleqtrd 2843 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈
(((TopOpen‘ℂfld) ↾t (𝑋[,]𝑌)) Cn ((TopOpen‘ℂfld)
↾t (𝐾[,]𝐿)))) |
| 121 | | cnf2 23257 |
. . . . . . . . . . . . 13
⊢
((((TopOpen‘ℂfld) ↾t (𝑋[,]𝑌)) ∈ (TopOn‘(𝑋[,]𝑌)) ∧
((TopOpen‘ℂfld) ↾t (𝐾[,]𝐿)) ∈ (TopOn‘(𝐾[,]𝐿)) ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈
(((TopOpen‘ℂfld) ↾t (𝑋[,]𝑌)) Cn ((TopOpen‘ℂfld)
↾t (𝐾[,]𝐿)))) → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝐾[,]𝐿)) |
| 122 | 114, 116,
120, 121 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝐾[,]𝐿)) |
| 123 | 122 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝐾[,]𝐿)) |
| 124 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) = (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) |
| 125 | 124 | fmpt 7130 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
(𝑋[,]𝑌)𝐴 ∈ (𝐾[,]𝐿) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝐾[,]𝐿)) |
| 126 | 123, 125 | sylibr 234 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ∀𝑥 ∈ (𝑋[,]𝑌)𝐴 ∈ (𝐾[,]𝐿)) |
| 127 | | ioossicc 13473 |
. . . . . . . . . . . 12
⊢ (𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) |
| 128 | 127 | sseli 3979 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝑋(,)𝑌) → 𝑥 ∈ (𝑋[,]𝑌)) |
| 129 | 128 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝑥 ∈ (𝑋[,]𝑌)) |
| 130 | | rsp 3247 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
(𝑋[,]𝑌)𝐴 ∈ (𝐾[,]𝐿) → (𝑥 ∈ (𝑋[,]𝑌) → 𝐴 ∈ (𝐾[,]𝐿))) |
| 131 | 126, 129,
130 | sylc 65 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐴 ∈ (𝐾[,]𝐿)) |
| 132 | 131 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 = 𝐴) → 𝐴 ∈ (𝐾[,]𝐿)) |
| 133 | 109, 132 | eqeltrd 2841 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 = 𝐴) → 𝑢 ∈ (𝐾[,]𝐿)) |
| 134 | 133 | iftrued 4533 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 = 𝐴) → if(𝑢 ∈ (𝐾[,]𝐿), (𝐹‘𝑢), if(𝑢 < 𝐾, (𝐹‘𝐾), (𝐹‘𝐿))) = (𝐹‘𝑢)) |
| 135 | | simpll 767 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 = 𝐴) → 𝜑) |
| 136 | 135, 133,
25 | syl2anc 584 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 = 𝐴) → 𝐶 ∈ ℂ) |
| 137 | 133, 136,
27 | syl2anc 584 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 = 𝐴) → (𝐹‘𝑢) = 𝐶) |
| 138 | | itgsubsticclem.13 |
. . . . . . 7
⊢ (𝑢 = 𝐴 → 𝐶 = 𝐸) |
| 139 | 138 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 = 𝐴) → 𝐶 = 𝐸) |
| 140 | 134, 137,
139 | 3eqtrd 2781 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 = 𝐴) → if(𝑢 ∈ (𝐾[,]𝐿), (𝐹‘𝑢), if(𝑢 < 𝐾, (𝐹‘𝐾), (𝐹‘𝐿))) = 𝐸) |
| 141 | 12 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝐾[,]𝐿) ⊆ ℝ) |
| 142 | 141, 131 | sseldd 3984 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐴 ∈ ℝ) |
| 143 | | elex 3501 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝐾[,]𝐿) → 𝐴 ∈ V) |
| 144 | 131, 143 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐴 ∈ V) |
| 145 | | isset 3494 |
. . . . . . 7
⊢ (𝐴 ∈ V ↔ ∃𝑢 𝑢 = 𝐴) |
| 146 | 144, 145 | sylib 218 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ∃𝑢 𝑢 = 𝐴) |
| 147 | 139, 136 | eqeltrrd 2842 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 = 𝐴) → 𝐸 ∈ ℂ) |
| 148 | 146, 147 | exlimddv 1935 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐸 ∈ ℂ) |
| 149 | 108, 140,
142, 148 | fvmptd 7023 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝐺‘𝐴) = 𝐸) |
| 150 | 149 | oveq1d 7446 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ((𝐺‘𝐴) · 𝐵) = (𝐸 · 𝐵)) |
| 151 | 37, 150 | ditgeq3d 45979 |
. 2
⊢ (𝜑 → ⨜[𝑋 → 𝑌]((𝐺‘𝐴) · 𝐵) d𝑥 = ⨜[𝑋 → 𝑌](𝐸 · 𝐵) d𝑥) |
| 152 | 107, 151 | eqtrd 2777 |
1
⊢ (𝜑 → ⨜[𝐾 → 𝐿]𝐶 d𝑢 = ⨜[𝑋 → 𝑌](𝐸 · 𝐵) d𝑥) |