Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  itgsubsticclem Structured version   Visualization version   GIF version

Theorem itgsubsticclem 43760
Description: lemma for itgsubsticc 43761. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
itgsubsticclem.1 𝐹 = (𝑢 ∈ (𝐾[,]𝐿) ↦ 𝐶)
itgsubsticclem.2 𝐺 = (𝑢 ∈ ℝ ↦ if(𝑢 ∈ (𝐾[,]𝐿), (𝐹𝑢), if(𝑢 < 𝐾, (𝐹𝐾), (𝐹𝐿))))
itgsubsticclem.3 (𝜑𝑋 ∈ ℝ)
itgsubsticclem.4 (𝜑𝑌 ∈ ℝ)
itgsubsticclem.5 (𝜑𝑋𝑌)
itgsubsticclem.6 (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝐾[,]𝐿)))
itgsubsticclem.7 (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ (((𝑋(,)𝑌)–cn→ℂ) ∩ 𝐿1))
itgsubsticclem.8 (𝜑𝐹 ∈ ((𝐾[,]𝐿)–cn→ℂ))
itgsubsticclem.9 (𝜑𝐾 ∈ ℝ)
itgsubsticclem.10 (𝜑𝐿 ∈ ℝ)
itgsubsticclem.11 (𝜑𝐾𝐿)
itgsubsticclem.12 (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵))
itgsubsticclem.13 (𝑢 = 𝐴𝐶 = 𝐸)
itgsubsticclem.14 (𝑥 = 𝑋𝐴 = 𝐾)
itgsubsticclem.15 (𝑥 = 𝑌𝐴 = 𝐿)
Assertion
Ref Expression
itgsubsticclem (𝜑 → ⨜[𝐾𝐿]𝐶 d𝑢 = ⨜[𝑋𝑌](𝐸 · 𝐵) d𝑥)
Distinct variable groups:   𝑢,𝐴   𝑢,𝐸   𝑥,𝐺   𝑢,𝐾,𝑥   𝑢,𝐿,𝑥   𝑢,𝑋,𝑥   𝑢,𝑌,𝑥   𝜑,𝑢,𝑥
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥,𝑢)   𝐶(𝑥,𝑢)   𝐸(𝑥)   𝐹(𝑥,𝑢)   𝐺(𝑢)

Proof of Theorem itgsubsticclem
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 fveq2 6809 . . . 4 (𝑢 = 𝑤 → (𝐺𝑢) = (𝐺𝑤))
2 nfcv 2905 . . . 4 𝑤(𝐺𝑢)
3 itgsubsticclem.2 . . . . . 6 𝐺 = (𝑢 ∈ ℝ ↦ if(𝑢 ∈ (𝐾[,]𝐿), (𝐹𝑢), if(𝑢 < 𝐾, (𝐹𝐾), (𝐹𝐿))))
4 nfmpt1 5193 . . . . . 6 𝑢(𝑢 ∈ ℝ ↦ if(𝑢 ∈ (𝐾[,]𝐿), (𝐹𝑢), if(𝑢 < 𝐾, (𝐹𝐾), (𝐹𝐿))))
53, 4nfcxfr 2903 . . . . 5 𝑢𝐺
6 nfcv 2905 . . . . 5 𝑢𝑤
75, 6nffv 6819 . . . 4 𝑢(𝐺𝑤)
81, 2, 7cbvditg 25089 . . 3 ⨜[𝐾𝐿](𝐺𝑢) d𝑢 = ⨜[𝐾𝐿](𝐺𝑤) d𝑤
9 itgsubsticclem.11 . . . 4 (𝜑𝐾𝐿)
10 itgsubsticclem.9 . . . . . . . . 9 (𝜑𝐾 ∈ ℝ)
11 itgsubsticclem.10 . . . . . . . . 9 (𝜑𝐿 ∈ ℝ)
1210, 11iccssred 13236 . . . . . . . 8 (𝜑 → (𝐾[,]𝐿) ⊆ ℝ)
1312adantr 481 . . . . . . 7 ((𝜑𝑢 ∈ (𝐾(,)𝐿)) → (𝐾[,]𝐿) ⊆ ℝ)
14 ioossicc 13235 . . . . . . . . 9 (𝐾(,)𝐿) ⊆ (𝐾[,]𝐿)
1514sseli 3926 . . . . . . . 8 (𝑢 ∈ (𝐾(,)𝐿) → 𝑢 ∈ (𝐾[,]𝐿))
1615adantl 482 . . . . . . 7 ((𝜑𝑢 ∈ (𝐾(,)𝐿)) → 𝑢 ∈ (𝐾[,]𝐿))
1713, 16sseldd 3931 . . . . . 6 ((𝜑𝑢 ∈ (𝐾(,)𝐿)) → 𝑢 ∈ ℝ)
1816iftrued 4477 . . . . . . 7 ((𝜑𝑢 ∈ (𝐾(,)𝐿)) → if(𝑢 ∈ (𝐾[,]𝐿), (𝐹𝑢), if(𝑢 < 𝐾, (𝐹𝐾), (𝐹𝐿))) = (𝐹𝑢))
19 itgsubsticclem.1 . . . . . . . . . . . . 13 𝐹 = (𝑢 ∈ (𝐾[,]𝐿) ↦ 𝐶)
2019a1i 11 . . . . . . . . . . . 12 (𝜑𝐹 = (𝑢 ∈ (𝐾[,]𝐿) ↦ 𝐶))
21 itgsubsticclem.8 . . . . . . . . . . . . 13 (𝜑𝐹 ∈ ((𝐾[,]𝐿)–cn→ℂ))
22 cncff 24127 . . . . . . . . . . . . 13 (𝐹 ∈ ((𝐾[,]𝐿)–cn→ℂ) → 𝐹:(𝐾[,]𝐿)⟶ℂ)
2321, 22syl 17 . . . . . . . . . . . 12 (𝜑𝐹:(𝐾[,]𝐿)⟶ℂ)
2420, 23feq1dd 42938 . . . . . . . . . . 11 (𝜑 → (𝑢 ∈ (𝐾[,]𝐿) ↦ 𝐶):(𝐾[,]𝐿)⟶ℂ)
2524fvmptelcdm 7024 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝐾[,]𝐿)) → 𝐶 ∈ ℂ)
2616, 25syldan 591 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝐾(,)𝐿)) → 𝐶 ∈ ℂ)
2719fvmpt2 6923 . . . . . . . . 9 ((𝑢 ∈ (𝐾[,]𝐿) ∧ 𝐶 ∈ ℂ) → (𝐹𝑢) = 𝐶)
2816, 26, 27syl2anc 584 . . . . . . . 8 ((𝜑𝑢 ∈ (𝐾(,)𝐿)) → (𝐹𝑢) = 𝐶)
2928, 26eqeltrd 2838 . . . . . . 7 ((𝜑𝑢 ∈ (𝐾(,)𝐿)) → (𝐹𝑢) ∈ ℂ)
3018, 29eqeltrd 2838 . . . . . 6 ((𝜑𝑢 ∈ (𝐾(,)𝐿)) → if(𝑢 ∈ (𝐾[,]𝐿), (𝐹𝑢), if(𝑢 < 𝐾, (𝐹𝐾), (𝐹𝐿))) ∈ ℂ)
313fvmpt2 6923 . . . . . 6 ((𝑢 ∈ ℝ ∧ if(𝑢 ∈ (𝐾[,]𝐿), (𝐹𝑢), if(𝑢 < 𝐾, (𝐹𝐾), (𝐹𝐿))) ∈ ℂ) → (𝐺𝑢) = if(𝑢 ∈ (𝐾[,]𝐿), (𝐹𝑢), if(𝑢 < 𝐾, (𝐹𝐾), (𝐹𝐿))))
3217, 30, 31syl2anc 584 . . . . 5 ((𝜑𝑢 ∈ (𝐾(,)𝐿)) → (𝐺𝑢) = if(𝑢 ∈ (𝐾[,]𝐿), (𝐹𝑢), if(𝑢 < 𝐾, (𝐹𝐾), (𝐹𝐿))))
3332, 18, 283eqtrd 2781 . . . 4 ((𝜑𝑢 ∈ (𝐾(,)𝐿)) → (𝐺𝑢) = 𝐶)
349, 33ditgeq3d 43749 . . 3 (𝜑 → ⨜[𝐾𝐿](𝐺𝑢) d𝑢 = ⨜[𝐾𝐿]𝐶 d𝑢)
35 itgsubsticclem.3 . . . 4 (𝜑𝑋 ∈ ℝ)
36 itgsubsticclem.4 . . . 4 (𝜑𝑌 ∈ ℝ)
37 itgsubsticclem.5 . . . 4 (𝜑𝑋𝑌)
38 mnfxr 11102 . . . . 5 -∞ ∈ ℝ*
3938a1i 11 . . . 4 (𝜑 → -∞ ∈ ℝ*)
40 pnfxr 11099 . . . . 5 +∞ ∈ ℝ*
4140a1i 11 . . . 4 (𝜑 → +∞ ∈ ℝ*)
42 ioomax 13224 . . . . . . . . 9 (-∞(,)+∞) = ℝ
4342eqcomi 2746 . . . . . . . 8 ℝ = (-∞(,)+∞)
4443a1i 11 . . . . . . 7 (𝜑 → ℝ = (-∞(,)+∞))
4512, 44sseqtrd 3970 . . . . . 6 (𝜑 → (𝐾[,]𝐿) ⊆ (-∞(,)+∞))
46 ax-resscn 10998 . . . . . . 7 ℝ ⊆ ℂ
4744, 46eqsstrrdi 3985 . . . . . 6 (𝜑 → (-∞(,)+∞) ⊆ ℂ)
48 cncfss 24133 . . . . . 6 (((𝐾[,]𝐿) ⊆ (-∞(,)+∞) ∧ (-∞(,)+∞) ⊆ ℂ) → ((𝑋[,]𝑌)–cn→(𝐾[,]𝐿)) ⊆ ((𝑋[,]𝑌)–cn→(-∞(,)+∞)))
4945, 47, 48syl2anc 584 . . . . 5 (𝜑 → ((𝑋[,]𝑌)–cn→(𝐾[,]𝐿)) ⊆ ((𝑋[,]𝑌)–cn→(-∞(,)+∞)))
50 itgsubsticclem.6 . . . . 5 (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝐾[,]𝐿)))
5149, 50sseldd 3931 . . . 4 (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(-∞(,)+∞)))
52 itgsubsticclem.7 . . . 4 (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ (((𝑋(,)𝑌)–cn→ℂ) ∩ 𝐿1))
53 nfmpt1 5193 . . . . . . . . . . 11 𝑢(𝑢 ∈ (𝐾[,]𝐿) ↦ 𝐶)
5419, 53nfcxfr 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)
5857cnfldtop 24018 . . . . . . . . . . 11 (TopOpen‘ℂfld) ∈ Top
5958a1i 11 . . . . . . . . . 10 (𝜑 → (TopOpen‘ℂfld) ∈ Top)
6012, 46sstrdi 3942 . . . . . . . . . . . . 13 (𝜑 → (𝐾[,]𝐿) ⊆ ℂ)
61 ssid 3952 . . . . . . . . . . . . 13 ℂ ⊆ ℂ
62 eqid 2737 . . . . . . . . . . . . . 14 ((TopOpen‘ℂfld) ↾t (𝐾[,]𝐿)) = ((TopOpen‘ℂfld) ↾t (𝐾[,]𝐿))
63 unicntop 24020 . . . . . . . . . . . . . . . . 17 ℂ = (TopOpen‘ℂfld)
6463restid 17211 . . . . . . . . . . . . . . . 16 ((TopOpen‘ℂfld) ∈ Top → ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld))
6558, 64ax-mp 5 . . . . . . . . . . . . . . 15 ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld)
6665eqcomi 2746 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
6757, 62, 66cncfcn 24144 . . . . . . . . . . . . 13 (((𝐾[,]𝐿) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐾[,]𝐿)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝐾[,]𝐿)) Cn (TopOpen‘ℂfld)))
6860, 61, 67sylancl 586 . . . . . . . . . . . 12 (𝜑 → ((𝐾[,]𝐿)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝐾[,]𝐿)) Cn (TopOpen‘ℂfld)))
69 reex 11032 . . . . . . . . . . . . . . . 16 ℝ ∈ V
7069a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → ℝ ∈ V)
71 restabs 22387 . . . . . . . . . . . . . . 15 (((TopOpen‘ℂfld) ∈ Top ∧ (𝐾[,]𝐿) ⊆ ℝ ∧ ℝ ∈ V) → (((TopOpen‘ℂfld) ↾t ℝ) ↾t (𝐾[,]𝐿)) = ((TopOpen‘ℂfld) ↾t (𝐾[,]𝐿)))
7259, 12, 70, 71syl3anc 1370 . . . . . . . . . . . . . 14 (𝜑 → (((TopOpen‘ℂfld) ↾t ℝ) ↾t (𝐾[,]𝐿)) = ((TopOpen‘ℂfld) ↾t (𝐾[,]𝐿)))
7357tgioo2 24037 . . . . . . . . . . . . . . . . 17 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
7473eqcomi 2746 . . . . . . . . . . . . . . . 16 ((TopOpen‘ℂfld) ↾t ℝ) = (topGen‘ran (,))
7574a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → ((TopOpen‘ℂfld) ↾t ℝ) = (topGen‘ran (,)))
7675oveq1d 7328 . . . . . . . . . . . . . 14 (𝜑 → (((TopOpen‘ℂfld) ↾t ℝ) ↾t (𝐾[,]𝐿)) = ((topGen‘ran (,)) ↾t (𝐾[,]𝐿)))
7772, 76eqtr3d 2779 . . . . . . . . . . . . 13 (𝜑 → ((TopOpen‘ℂfld) ↾t (𝐾[,]𝐿)) = ((topGen‘ran (,)) ↾t (𝐾[,]𝐿)))
7877oveq1d 7328 . . . . . . . . . . . 12 (𝜑 → (((TopOpen‘ℂfld) ↾t (𝐾[,]𝐿)) Cn (TopOpen‘ℂfld)) = (((topGen‘ran (,)) ↾t (𝐾[,]𝐿)) Cn (TopOpen‘ℂfld)))
7968, 78eqtrd 2777 . . . . . . . . . . 11 (𝜑 → ((𝐾[,]𝐿)–cn→ℂ) = (((topGen‘ran (,)) ↾t (𝐾[,]𝐿)) Cn (TopOpen‘ℂfld)))
8021, 79eleqtrd 2840 . . . . . . . . . 10 (𝜑𝐹 ∈ (((topGen‘ran (,)) ↾t (𝐾[,]𝐿)) Cn (TopOpen‘ℂfld)))
8154, 55, 56, 3, 10, 11, 9, 59, 80icccncfext 43672 . . . . . . . . 9 (𝜑 → (𝐺 ∈ ((topGen‘ran (,)) Cn ((TopOpen‘ℂfld) ↾t ran 𝐹)) ∧ (𝐺 ↾ (𝐾[,]𝐿)) = 𝐹))
8281simpld 495 . . . . . . . 8 (𝜑𝐺 ∈ ((topGen‘ran (,)) Cn ((TopOpen‘ℂfld) ↾t ran 𝐹)))
83 uniretop 23997 . . . . . . . . 9 ℝ = (topGen‘ran (,))
84 eqid 2737 . . . . . . . . 9 ((TopOpen‘ℂfld) ↾t ran 𝐹) = ((TopOpen‘ℂfld) ↾t ran 𝐹)
8583, 84cnf 22468 . . . . . . . 8 (𝐺 ∈ ((topGen‘ran (,)) Cn ((TopOpen‘ℂfld) ↾t ran 𝐹)) → 𝐺:ℝ⟶ ((TopOpen‘ℂfld) ↾t ran 𝐹))
8682, 85syl 17 . . . . . . 7 (𝜑𝐺:ℝ⟶ ((TopOpen‘ℂfld) ↾t ran 𝐹))
8744feq2d 6621 . . . . . . 7 (𝜑 → (𝐺:ℝ⟶ ((TopOpen‘ℂfld) ↾t ran 𝐹) ↔ 𝐺:(-∞(,)+∞)⟶ ((TopOpen‘ℂfld) ↾t ran 𝐹)))
8886, 87mpbid 231 . . . . . 6 (𝜑𝐺:(-∞(,)+∞)⟶ ((TopOpen‘ℂfld) ↾t ran 𝐹))
8988feqmptd 6874 . . . . 5 (𝜑𝐺 = (𝑤 ∈ (-∞(,)+∞) ↦ (𝐺𝑤)))
9023frnd 6643 . . . . . . 7 (𝜑 → ran 𝐹 ⊆ ℂ)
91 cncfss 24133 . . . . . . 7 ((ran 𝐹 ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((-∞(,)+∞)–cn→ran 𝐹) ⊆ ((-∞(,)+∞)–cn→ℂ))
9290, 61, 91sylancl 586 . . . . . 6 (𝜑 → ((-∞(,)+∞)–cn→ran 𝐹) ⊆ ((-∞(,)+∞)–cn→ℂ))
9343oveq2i 7324 . . . . . . . . . . 11 ((TopOpen‘ℂfld) ↾t ℝ) = ((TopOpen‘ℂfld) ↾t (-∞(,)+∞))
9473, 93eqtri 2765 . . . . . . . . . 10 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t (-∞(,)+∞))
95 eqid 2737 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t ran 𝐹) = ((TopOpen‘ℂfld) ↾t ran 𝐹)
9657, 94, 95cncfcn 24144 . . . . . . . . 9 (((-∞(,)+∞) ⊆ ℂ ∧ ran 𝐹 ⊆ ℂ) → ((-∞(,)+∞)–cn→ran 𝐹) = ((topGen‘ran (,)) Cn ((TopOpen‘ℂfld) ↾t ran 𝐹)))
9747, 90, 96syl2anc 584 . . . . . . . 8 (𝜑 → ((-∞(,)+∞)–cn→ran 𝐹) = ((topGen‘ran (,)) Cn ((TopOpen‘ℂfld) ↾t ran 𝐹)))
9897eqcomd 2743 . . . . . . 7 (𝜑 → ((topGen‘ran (,)) Cn ((TopOpen‘ℂfld) ↾t ran 𝐹)) = ((-∞(,)+∞)–cn→ran 𝐹))
9982, 98eleqtrd 2840 . . . . . 6 (𝜑𝐺 ∈ ((-∞(,)+∞)–cn→ran 𝐹))
10092, 99sseldd 3931 . . . . 5 (𝜑𝐺 ∈ ((-∞(,)+∞)–cn→ℂ))
10189, 100eqeltrrd 2839 . . . 4 (𝜑 → (𝑤 ∈ (-∞(,)+∞) ↦ (𝐺𝑤)) ∈ ((-∞(,)+∞)–cn→ℂ))
102 itgsubsticclem.12 . . . 4 (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵))
103 fveq2 6809 . . . 4 (𝑤 = 𝐴 → (𝐺𝑤) = (𝐺𝐴))
104 itgsubsticclem.14 . . . 4 (𝑥 = 𝑋𝐴 = 𝐾)
105 itgsubsticclem.15 . . . 4 (𝑥 = 𝑌𝐴 = 𝐿)
10635, 36, 37, 39, 41, 51, 52, 101, 102, 103, 104, 105itgsubst 25284 . . 3 (𝜑 → ⨜[𝐾𝐿](𝐺𝑤) d𝑤 = ⨜[𝑋𝑌]((𝐺𝐴) · 𝐵) d𝑥)
1078, 34, 1063eqtr3a 2801 . 2 (𝜑 → ⨜[𝐾𝐿]𝐶 d𝑢 = ⨜[𝑋𝑌]((𝐺𝐴) · 𝐵) d𝑥)
1083a1i 11 . . . . 5 ((𝜑𝑥 ∈ (𝑋(,)𝑌)) → 𝐺 = (𝑢 ∈ ℝ ↦ if(𝑢 ∈ (𝐾[,]𝐿), (𝐹𝑢), if(𝑢 < 𝐾, (𝐹𝐾), (𝐹𝐿)))))
109 simpr 485 . . . . . . . 8 (((𝜑𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 = 𝐴) → 𝑢 = 𝐴)
11057cnfldtopon 24017 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
11135, 36iccssred 13236 . . . . . . . . . . . . . . 15 (𝜑 → (𝑋[,]𝑌) ⊆ ℝ)
112111, 46sstrdi 3942 . . . . . . . . . . . . . 14 (𝜑 → (𝑋[,]𝑌) ⊆ ℂ)
113 resttopon 22383 . . . . . . . . . . . . . 14 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (𝑋[,]𝑌) ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t (𝑋[,]𝑌)) ∈ (TopOn‘(𝑋[,]𝑌)))
114110, 112, 113sylancr 587 . . . . . . . . . . . . 13 (𝜑 → ((TopOpen‘ℂfld) ↾t (𝑋[,]𝑌)) ∈ (TopOn‘(𝑋[,]𝑌)))
115 resttopon 22383 . . . . . . . . . . . . . 14 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (𝐾[,]𝐿) ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t (𝐾[,]𝐿)) ∈ (TopOn‘(𝐾[,]𝐿)))
116110, 60, 115sylancr 587 . . . . . . . . . . . . 13 (𝜑 → ((TopOpen‘ℂfld) ↾t (𝐾[,]𝐿)) ∈ (TopOn‘(𝐾[,]𝐿)))
117 eqid 2737 . . . . . . . . . . . . . . . 16 ((TopOpen‘ℂfld) ↾t (𝑋[,]𝑌)) = ((TopOpen‘ℂfld) ↾t (𝑋[,]𝑌))
11857, 117, 62cncfcn 24144 . . . . . . . . . . . . . . 15 (((𝑋[,]𝑌) ⊆ ℂ ∧ (𝐾[,]𝐿) ⊆ ℂ) → ((𝑋[,]𝑌)–cn→(𝐾[,]𝐿)) = (((TopOpen‘ℂfld) ↾t (𝑋[,]𝑌)) Cn ((TopOpen‘ℂfld) ↾t (𝐾[,]𝐿))))
119112, 60, 118syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → ((𝑋[,]𝑌)–cn→(𝐾[,]𝐿)) = (((TopOpen‘ℂfld) ↾t (𝑋[,]𝑌)) Cn ((TopOpen‘ℂfld) ↾t (𝐾[,]𝐿))))
12050, 119eleqtrd 2840 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ (((TopOpen‘ℂfld) ↾t (𝑋[,]𝑌)) Cn ((TopOpen‘ℂfld) ↾t (𝐾[,]𝐿))))
121 cnf2 22471 . . . . . . . . . . . . 13 ((((TopOpen‘ℂfld) ↾t (𝑋[,]𝑌)) ∈ (TopOn‘(𝑋[,]𝑌)) ∧ ((TopOpen‘ℂfld) ↾t (𝐾[,]𝐿)) ∈ (TopOn‘(𝐾[,]𝐿)) ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ (((TopOpen‘ℂfld) ↾t (𝑋[,]𝑌)) Cn ((TopOpen‘ℂfld) ↾t (𝐾[,]𝐿)))) → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝐾[,]𝐿))
122114, 116, 120, 121syl3anc 1370 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝐾[,]𝐿))
123122adantr 481 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝑋(,)𝑌)) → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝐾[,]𝐿))
124 eqid 2737 . . . . . . . . . . . 12 (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) = (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)
125124fmpt 7021 . . . . . . . . . . 11 (∀𝑥 ∈ (𝑋[,]𝑌)𝐴 ∈ (𝐾[,]𝐿) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝐾[,]𝐿))
126123, 125sylibr 233 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝑋(,)𝑌)) → ∀𝑥 ∈ (𝑋[,]𝑌)𝐴 ∈ (𝐾[,]𝐿))
127 ioossicc 13235 . . . . . . . . . . . 12 (𝑋(,)𝑌) ⊆ (𝑋[,]𝑌)
128127sseli 3926 . . . . . . . . . . 11 (𝑥 ∈ (𝑋(,)𝑌) → 𝑥 ∈ (𝑋[,]𝑌))
129128adantl 482 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝑋(,)𝑌)) → 𝑥 ∈ (𝑋[,]𝑌))
130 rsp 3227 . . . . . . . . . 10 (∀𝑥 ∈ (𝑋[,]𝑌)𝐴 ∈ (𝐾[,]𝐿) → (𝑥 ∈ (𝑋[,]𝑌) → 𝐴 ∈ (𝐾[,]𝐿)))
131126, 129, 130sylc 65 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝑋(,)𝑌)) → 𝐴 ∈ (𝐾[,]𝐿))
132131adantr 481 . . . . . . . 8 (((𝜑𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 = 𝐴) → 𝐴 ∈ (𝐾[,]𝐿))
133109, 132eqeltrd 2838 . . . . . . 7 (((𝜑𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 = 𝐴) → 𝑢 ∈ (𝐾[,]𝐿))
134133iftrued 4477 . . . . . 6 (((𝜑𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 = 𝐴) → if(𝑢 ∈ (𝐾[,]𝐿), (𝐹𝑢), if(𝑢 < 𝐾, (𝐹𝐾), (𝐹𝐿))) = (𝐹𝑢))
135 simpll 764 . . . . . . . 8 (((𝜑𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 = 𝐴) → 𝜑)
136135, 133, 25syl2anc 584 . . . . . . 7 (((𝜑𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 = 𝐴) → 𝐶 ∈ ℂ)
137133, 136, 27syl2anc 584 . . . . . 6 (((𝜑𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 = 𝐴) → (𝐹𝑢) = 𝐶)
138 itgsubsticclem.13 . . . . . . 7 (𝑢 = 𝐴𝐶 = 𝐸)
139138adantl 482 . . . . . 6 (((𝜑𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 = 𝐴) → 𝐶 = 𝐸)
140134, 137, 1393eqtrd 2781 . . . . 5 (((𝜑𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 = 𝐴) → if(𝑢 ∈ (𝐾[,]𝐿), (𝐹𝑢), if(𝑢 < 𝐾, (𝐹𝐾), (𝐹𝐿))) = 𝐸)
14112adantr 481 . . . . . 6 ((𝜑𝑥 ∈ (𝑋(,)𝑌)) → (𝐾[,]𝐿) ⊆ ℝ)
142141, 131sseldd 3931 . . . . 5 ((𝜑𝑥 ∈ (𝑋(,)𝑌)) → 𝐴 ∈ ℝ)
143 elex 3459 . . . . . . . 8 (𝐴 ∈ (𝐾[,]𝐿) → 𝐴 ∈ V)
144131, 143syl 17 . . . . . . 7 ((𝜑𝑥 ∈ (𝑋(,)𝑌)) → 𝐴 ∈ V)
145 isset 3454 . . . . . . 7 (𝐴 ∈ V ↔ ∃𝑢 𝑢 = 𝐴)
146144, 145sylib 217 . . . . . 6 ((𝜑𝑥 ∈ (𝑋(,)𝑌)) → ∃𝑢 𝑢 = 𝐴)
147139, 136eqeltrrd 2839 . . . . . 6 (((𝜑𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 = 𝐴) → 𝐸 ∈ ℂ)
148146, 147exlimddv 1937 . . . . 5 ((𝜑𝑥 ∈ (𝑋(,)𝑌)) → 𝐸 ∈ ℂ)
149108, 140, 142, 148fvmptd 6919 . . . 4 ((𝜑𝑥 ∈ (𝑋(,)𝑌)) → (𝐺𝐴) = 𝐸)
150149oveq1d 7328 . . 3 ((𝜑𝑥 ∈ (𝑋(,)𝑌)) → ((𝐺𝐴) · 𝐵) = (𝐸 · 𝐵))
15137, 150ditgeq3d 43749 . 2 (𝜑 → ⨜[𝑋𝑌]((𝐺𝐴) · 𝐵) d𝑥 = ⨜[𝑋𝑌](𝐸 · 𝐵) d𝑥)
152107, 151eqtrd 2777 1 (𝜑 → ⨜[𝐾𝐿]𝐶 d𝑢 = ⨜[𝑋𝑌](𝐸 · 𝐵) d𝑥)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1540  wex 1780  wcel 2105  wral 3062  Vcvv 3441  cin 3895  wss 3896  ifcif 4469   cuni 4848   class class class wbr 5085  cmpt 5168  ran crn 5606  cres 5607  wf 6459  cfv 6463  (class class class)co 7313  cc 10939  cr 10940   · cmul 10946  +∞cpnf 11076  -∞cmnf 11077  *cxr 11078   < clt 11079  cle 11080  (,)cioo 13149  [,]cicc 13152  t crest 17198  TopOpenctopn 17199  topGenctg 17215  fldccnfld 20668  Topctop 22113  TopOnctopon 22130   Cn ccn 22446  cnccncf 24110  𝐿1cibl 24852  cdit 25081   D cdv 25098
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-rep 5222  ax-sep 5236  ax-nul 5243  ax-pow 5301  ax-pr 5365  ax-un 7626  ax-inf2 9467  ax-cc 10261  ax-cnex 10997  ax-resscn 10998  ax-1cn 10999  ax-icn 11000  ax-addcl 11001  ax-addrcl 11002  ax-mulcl 11003  ax-mulrcl 11004  ax-mulcom 11005  ax-addass 11006  ax-mulass 11007  ax-distr 11008  ax-i2m1 11009  ax-1ne0 11010  ax-1rid 11011  ax-rnegex 11012  ax-rrecex 11013  ax-cnre 11014  ax-pre-lttri 11015  ax-pre-lttrn 11016  ax-pre-ltadd 11017  ax-pre-mulgt0 11018  ax-pre-sup 11019  ax-addf 11020  ax-mulf 11021
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3726  df-csb 3842  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-pss 3915  df-symdif 4186  df-nul 4267  df-if 4470  df-pw 4545  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4849  df-int 4891  df-iun 4937  df-iin 4938  df-disj 5051  df-br 5086  df-opab 5148  df-mpt 5169  df-tr 5203  df-id 5505  df-eprel 5511  df-po 5519  df-so 5520  df-fr 5560  df-se 5561  df-we 5562  df-xp 5611  df-rel 5612  df-cnv 5613  df-co 5614  df-dm 5615  df-rn 5616  df-res 5617  df-ima 5618  df-pred 6222  df-ord 6289  df-on 6290  df-lim 6291  df-suc 6292  df-iota 6415  df-fun 6465  df-fn 6466  df-f 6467  df-f1 6468  df-fo 6469  df-f1o 6470  df-fv 6471  df-isom 6472  df-riota 7270  df-ov 7316  df-oprab 7317  df-mpo 7318  df-of 7571  df-ofr 7572  df-om 7756  df-1st 7874  df-2nd 7875  df-supp 8023  df-frecs 8142  df-wrecs 8173  df-recs 8247  df-rdg 8286  df-1o 8342  df-2o 8343  df-oadd 8346  df-omul 8347  df-er 8544  df-map 8663  df-pm 8664  df-ixp 8732  df-en 8780  df-dom 8781  df-sdom 8782  df-fin 8783  df-fsupp 9197  df-fi 9238  df-sup 9269  df-inf 9270  df-oi 9337  df-dju 9727  df-card 9765  df-acn 9768  df-pnf 11081  df-mnf 11082  df-xr 11083  df-ltxr 11084  df-le 11085  df-sub 11277  df-neg 11278  df-div 11703  df-nn 12044  df-2 12106  df-3 12107  df-4 12108  df-5 12109  df-6 12110  df-7 12111  df-8 12112  df-9 12113  df-n0 12304  df-z 12390  df-dec 12508  df-uz 12653  df-q 12759  df-rp 12801  df-xneg 12918  df-xadd 12919  df-xmul 12920  df-ioo 13153  df-ioc 13154  df-ico 13155  df-icc 13156  df-fz 13310  df-fzo 13453  df-fl 13582  df-mod 13660  df-seq 13792  df-exp 13853  df-hash 14115  df-cj 14879  df-re 14880  df-im 14881  df-sqrt 15015  df-abs 15016  df-limsup 15249  df-clim 15266  df-rlim 15267  df-sum 15467  df-struct 16915  df-sets 16932  df-slot 16950  df-ndx 16962  df-base 16980  df-ress 17009  df-plusg 17042  df-mulr 17043  df-starv 17044  df-sca 17045  df-vsca 17046  df-ip 17047  df-tset 17048  df-ple 17049  df-ds 17051  df-unif 17052  df-hom 17053  df-cco 17054  df-rest 17200  df-topn 17201  df-0g 17219  df-gsum 17220  df-topgen 17221  df-pt 17222  df-prds 17225  df-xrs 17280  df-qtop 17285  df-imas 17286  df-xps 17288  df-mre 17362  df-mrc 17363  df-acs 17365  df-mgm 18393  df-sgrp 18442  df-mnd 18453  df-submnd 18498  df-mulg 18768  df-cntz 18990  df-cmn 19455  df-psmet 20660  df-xmet 20661  df-met 20662  df-bl 20663  df-mopn 20664  df-fbas 20665  df-fg 20666  df-cnfld 20669  df-top 22114  df-topon 22131  df-topsp 22153  df-bases 22167  df-cld 22241  df-ntr 22242  df-cls 22243  df-nei 22320  df-lp 22358  df-perf 22359  df-cn 22449  df-cnp 22450  df-haus 22537  df-cmp 22609  df-tx 22784  df-hmeo 22977  df-fil 23068  df-fm 23160  df-flim 23161  df-flf 23162  df-xms 23544  df-ms 23545  df-tms 23546  df-cncf 24112  df-ovol 24699  df-vol 24700  df-mbf 24854  df-itg1 24855  df-itg2 24856  df-ibl 24857  df-itg 24858  df-0p 24905  df-ditg 25082  df-limc 25101  df-dv 25102
This theorem is referenced by:  itgsubsticc  43761
  Copyright terms: Public domain W3C validator