Metamath Proof Explorer

Theorem itgsubsticclem

Description: lemma for itgsubsticc . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses 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 itgsubsticclem ( 𝜑 → ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 = ⨜ [ 𝑋 → 𝑌 ] ( 𝐸 · 𝐵 ) d 𝑥 )

Proof

Step Hyp Ref Expression
1 itgsubsticclem.1 ⊢ 𝐹 = ( 𝑢 ∈ ( 𝐾 [,] 𝐿 ) ↦ 𝐶 )
2 itgsubsticclem.2 ⊢ 𝐺 = ( 𝑢 ∈ ℝ ↦ if ( 𝑢 ∈ ( 𝐾 [,] 𝐿 ) , ( 𝐹 ‘ 𝑢 ) , if ( 𝑢 < 𝐾 , ( 𝐹 ‘ 𝐾 ) , ( 𝐹 ‘ 𝐿 ) ) ) )
3 itgsubsticclem.3 ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
4 itgsubsticclem.4 ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
5 itgsubsticclem.5 ⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
6 itgsubsticclem.6 ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ( 𝐾 [,] 𝐿 ) ) )
7 itgsubsticclem.7 ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ ( ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) ∩ 𝐿1 ) )
8 itgsubsticclem.8 ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐾 [,] 𝐿 ) –cn→ ℂ ) )
9 itgsubsticclem.9 ⊢ ( 𝜑 → 𝐾 ∈ ℝ )
10 itgsubsticclem.10 ⊢ ( 𝜑 → 𝐿 ∈ ℝ )
11 itgsubsticclem.11 ⊢ ( 𝜑 → 𝐾 ≤ 𝐿 )
12 itgsubsticclem.12 ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) )
13 itgsubsticclem.13 ⊢ ( 𝑢 = 𝐴 → 𝐶 = 𝐸 )
14 itgsubsticclem.14 ⊢ ( 𝑥 = 𝑋 → 𝐴 = 𝐾 )
15 itgsubsticclem.15 ⊢ ( 𝑥 = 𝑌 → 𝐴 = 𝐿 )
16 fveq2 ⊢ ( 𝑢 = 𝑤 → ( 𝐺 ‘ 𝑢 ) = ( 𝐺 ‘ 𝑤 ) )
17 nfcv ⊢ Ⅎ 𝑤 ( 𝐺 ‘ 𝑢 )
18 nfmpt1 ⊢ Ⅎ 𝑢 ( 𝑢 ∈ ℝ ↦ if ( 𝑢 ∈ ( 𝐾 [,] 𝐿 ) , ( 𝐹 ‘ 𝑢 ) , if ( 𝑢 < 𝐾 , ( 𝐹 ‘ 𝐾 ) , ( 𝐹 ‘ 𝐿 ) ) ) )
19 2 18 nfcxfr ⊢ Ⅎ 𝑢 𝐺
20 nfcv ⊢ Ⅎ 𝑢 𝑤
21 19 20 nffv ⊢ Ⅎ 𝑢 ( 𝐺 ‘ 𝑤 )
22 16 17 21 cbvditg ⊢ ⨜ [ 𝐾 → 𝐿 ] ( 𝐺 ‘ 𝑢 ) d 𝑢 = ⨜ [ 𝐾 → 𝐿 ] ( 𝐺 ‘ 𝑤 ) d 𝑤
23 9 10 iccssred ⊢ ( 𝜑 → ( 𝐾 [,] 𝐿 ) ⊆ ℝ )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐾 (,) 𝐿 ) ) → ( 𝐾 [,] 𝐿 ) ⊆ ℝ )
25 ioossicc ⊢ ( 𝐾 (,) 𝐿 ) ⊆ ( 𝐾 [,] 𝐿 )
26 25 sseli ⊢ ( 𝑢 ∈ ( 𝐾 (,) 𝐿 ) → 𝑢 ∈ ( 𝐾 [,] 𝐿 ) )
27 26 adantl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐾 (,) 𝐿 ) ) → 𝑢 ∈ ( 𝐾 [,] 𝐿 ) )
28 24 27 sseldd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐾 (,) 𝐿 ) ) → 𝑢 ∈ ℝ )
29 27 iftrued ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐾 (,) 𝐿 ) ) → if ( 𝑢 ∈ ( 𝐾 [,] 𝐿 ) , ( 𝐹 ‘ 𝑢 ) , if ( 𝑢 < 𝐾 , ( 𝐹 ‘ 𝐾 ) , ( 𝐹 ‘ 𝐿 ) ) ) = ( 𝐹 ‘ 𝑢 ) )
30 1 a1i ⊢ ( 𝜑 → 𝐹 = ( 𝑢 ∈ ( 𝐾 [,] 𝐿 ) ↦ 𝐶 ) )
31 cncff ⊢ ( 𝐹 ∈ ( ( 𝐾 [,] 𝐿 ) –cn→ ℂ ) → 𝐹 : ( 𝐾 [,] 𝐿 ) ⟶ ℂ )
32 8 31 syl ⊢ ( 𝜑 → 𝐹 : ( 𝐾 [,] 𝐿 ) ⟶ ℂ )
33 30 32 feq1dd ⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝐾 [,] 𝐿 ) ↦ 𝐶 ) : ( 𝐾 [,] 𝐿 ) ⟶ ℂ )
34 33 fvmptelrn ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐾 [,] 𝐿 ) ) → 𝐶 ∈ ℂ )
35 27 34 syldan ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐾 (,) 𝐿 ) ) → 𝐶 ∈ ℂ )
36 1 fvmpt2 ⊢ ( ( 𝑢 ∈ ( 𝐾 [,] 𝐿 ) ∧ 𝐶 ∈ ℂ ) → ( 𝐹 ‘ 𝑢 ) = 𝐶 )
37 27 35 36 syl2anc ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐾 (,) 𝐿 ) ) → ( 𝐹 ‘ 𝑢 ) = 𝐶 )
38 37 35 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐾 (,) 𝐿 ) ) → ( 𝐹 ‘ 𝑢 ) ∈ ℂ )
39 29 38 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐾 (,) 𝐿 ) ) → if ( 𝑢 ∈ ( 𝐾 [,] 𝐿 ) , ( 𝐹 ‘ 𝑢 ) , if ( 𝑢 < 𝐾 , ( 𝐹 ‘ 𝐾 ) , ( 𝐹 ‘ 𝐿 ) ) ) ∈ ℂ )
40 2 fvmpt2 ⊢ ( ( 𝑢 ∈ ℝ ∧ if ( 𝑢 ∈ ( 𝐾 [,] 𝐿 ) , ( 𝐹 ‘ 𝑢 ) , if ( 𝑢 < 𝐾 , ( 𝐹 ‘ 𝐾 ) , ( 𝐹 ‘ 𝐿 ) ) ) ∈ ℂ ) → ( 𝐺 ‘ 𝑢 ) = if ( 𝑢 ∈ ( 𝐾 [,] 𝐿 ) , ( 𝐹 ‘ 𝑢 ) , if ( 𝑢 < 𝐾 , ( 𝐹 ‘ 𝐾 ) , ( 𝐹 ‘ 𝐿 ) ) ) )
41 28 39 40 syl2anc ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐾 (,) 𝐿 ) ) → ( 𝐺 ‘ 𝑢 ) = if ( 𝑢 ∈ ( 𝐾 [,] 𝐿 ) , ( 𝐹 ‘ 𝑢 ) , if ( 𝑢 < 𝐾 , ( 𝐹 ‘ 𝐾 ) , ( 𝐹 ‘ 𝐿 ) ) ) )
42 41 29 37 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐾 (,) 𝐿 ) ) → ( 𝐺 ‘ 𝑢 ) = 𝐶 )
43 11 42 ditgeq3d ⊢ ( 𝜑 → ⨜ [ 𝐾 → 𝐿 ] ( 𝐺 ‘ 𝑢 ) d 𝑢 = ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 )
44 mnfxr ⊢ -∞ ∈ ℝ*
45 44 a1i ⊢ ( 𝜑 → -∞ ∈ ℝ* )
46 pnfxr ⊢ +∞ ∈ ℝ*
47 46 a1i ⊢ ( 𝜑 → +∞ ∈ ℝ* )
48 ioomax ⊢ ( -∞ (,) +∞ ) = ℝ
49 48 eqcomi ⊢ ℝ = ( -∞ (,) +∞ )
50 49 a1i ⊢ ( 𝜑 → ℝ = ( -∞ (,) +∞ ) )
51 23 50 sseqtrd ⊢ ( 𝜑 → ( 𝐾 [,] 𝐿 ) ⊆ ( -∞ (,) +∞ ) )
52 ax-resscn ⊢ ℝ ⊆ ℂ
53 50 52 eqsstrrdi ⊢ ( 𝜑 → ( -∞ (,) +∞ ) ⊆ ℂ )
54 cncfss ⊢ ( ( ( 𝐾 [,] 𝐿 ) ⊆ ( -∞ (,) +∞ ) ∧ ( -∞ (,) +∞ ) ⊆ ℂ ) → ( ( 𝑋 [,] 𝑌 ) –cn→ ( 𝐾 [,] 𝐿 ) ) ⊆ ( ( 𝑋 [,] 𝑌 ) –cn→ ( -∞ (,) +∞ ) ) )
55 51 53 54 syl2anc ⊢ ( 𝜑 → ( ( 𝑋 [,] 𝑌 ) –cn→ ( 𝐾 [,] 𝐿 ) ) ⊆ ( ( 𝑋 [,] 𝑌 ) –cn→ ( -∞ (,) +∞ ) ) )
56 55 6 sseldd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ( -∞ (,) +∞ ) ) )
57 nfmpt1 ⊢ Ⅎ 𝑢 ( 𝑢 ∈ ( 𝐾 [,] 𝐿 ) ↦ 𝐶 )
58 1 57 nfcxfr ⊢ Ⅎ 𝑢 𝐹
59 eqid ⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
60 eqid ⊢ ∪ ( TopOpen ‘ ℂfld ) = ∪ ( TopOpen ‘ ℂfld )
61 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
62 61 cnfldtop ⊢ ( TopOpen ‘ ℂfld ) ∈ Top
63 62 a1i ⊢ ( 𝜑 → ( TopOpen ‘ ℂfld ) ∈ Top )
64 23 52 sstrdi ⊢ ( 𝜑 → ( 𝐾 [,] 𝐿 ) ⊆ ℂ )
65 ssid ⊢ ℂ ⊆ ℂ
66 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐾 [,] 𝐿 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐾 [,] 𝐿 ) )
67 unicntop ⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
68 67 restid ⊢ ( ( TopOpen ‘ ℂfld ) ∈ Top → ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld ) )
69 62 68 ax-mp ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld )
70 69 eqcomi ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
71 61 66 70 cncfcn ⊢ ( ( ( 𝐾 [,] 𝐿 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( 𝐾 [,] 𝐿 ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐾 [,] 𝐿 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
72 64 65 71 sylancl ⊢ ( 𝜑 → ( ( 𝐾 [,] 𝐿 ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐾 [,] 𝐿 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
73 reex ⊢ ℝ ∈ V
74 73 a1i ⊢ ( 𝜑 → ℝ ∈ V )
75 restabs ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ ( 𝐾 [,] 𝐿 ) ⊆ ℝ ∧ ℝ ∈ V ) → ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ↾t ( 𝐾 [,] 𝐿 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐾 [,] 𝐿 ) ) )
76 63 23 74 75 syl3anc ⊢ ( 𝜑 → ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ↾t ( 𝐾 [,] 𝐿 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐾 [,] 𝐿 ) ) )
77 61 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
78 77 eqcomi ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) = ( topGen ‘ ran (,) )
79 78 a1i ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) = ( topGen ‘ ran (,) ) )
80 79 oveq1d ⊢ ( 𝜑 → ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ↾t ( 𝐾 [,] 𝐿 ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 𝐾 [,] 𝐿 ) ) )
81 76 80 eqtr3d ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐾 [,] 𝐿 ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 𝐾 [,] 𝐿 ) ) )
82 81 oveq1d ⊢ ( 𝜑 → ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐾 [,] 𝐿 ) ) Cn ( TopOpen ‘ ℂfld ) ) = ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐾 [,] 𝐿 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
83 72 82 eqtrd ⊢ ( 𝜑 → ( ( 𝐾 [,] 𝐿 ) –cn→ ℂ ) = ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐾 [,] 𝐿 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
84 8 83 eleqtrd ⊢ ( 𝜑 → 𝐹 ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐾 [,] 𝐿 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
85 58 59 60 2 9 10 11 63 84 icccncfext ⊢ ( 𝜑 → ( 𝐺 ∈ ( ( topGen ‘ ran (,) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ran 𝐹 ) ) ∧ ( 𝐺 ↾ ( 𝐾 [,] 𝐿 ) ) = 𝐹 ) )
86 85 simpld ⊢ ( 𝜑 → 𝐺 ∈ ( ( topGen ‘ ran (,) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ran 𝐹 ) ) )
87 uniretop ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
88 eqid ⊢ ∪ ( ( TopOpen ‘ ℂfld ) ↾t ran 𝐹 ) = ∪ ( ( TopOpen ‘ ℂfld ) ↾t ran 𝐹 )
89 87 88 cnf ⊢ ( 𝐺 ∈ ( ( topGen ‘ ran (,) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ran 𝐹 ) ) → 𝐺 : ℝ ⟶ ∪ ( ( TopOpen ‘ ℂfld ) ↾t ran 𝐹 ) )
90 86 89 syl ⊢ ( 𝜑 → 𝐺 : ℝ ⟶ ∪ ( ( TopOpen ‘ ℂfld ) ↾t ran 𝐹 ) )
91 50 feq2d ⊢ ( 𝜑 → ( 𝐺 : ℝ ⟶ ∪ ( ( TopOpen ‘ ℂfld ) ↾t ran 𝐹 ) ↔ 𝐺 : ( -∞ (,) +∞ ) ⟶ ∪ ( ( TopOpen ‘ ℂfld ) ↾t ran 𝐹 ) ) )
92 90 91 mpbid ⊢ ( 𝜑 → 𝐺 : ( -∞ (,) +∞ ) ⟶ ∪ ( ( TopOpen ‘ ℂfld ) ↾t ran 𝐹 ) )
93 92 feqmptd ⊢ ( 𝜑 → 𝐺 = ( 𝑤 ∈ ( -∞ (,) +∞ ) ↦ ( 𝐺 ‘ 𝑤 ) ) )
94 32 frnd ⊢ ( 𝜑 → ran 𝐹 ⊆ ℂ )
95 cncfss ⊢ ( ( ran 𝐹 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( -∞ (,) +∞ ) –cn→ ran 𝐹 ) ⊆ ( ( -∞ (,) +∞ ) –cn→ ℂ ) )
96 94 65 95 sylancl ⊢ ( 𝜑 → ( ( -∞ (,) +∞ ) –cn→ ran 𝐹 ) ⊆ ( ( -∞ (,) +∞ ) –cn→ ℂ ) )
97 49 oveq2i ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) = ( ( TopOpen ‘ ℂfld ) ↾t ( -∞ (,) +∞ ) )
98 77 97 eqtri ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( -∞ (,) +∞ ) )
99 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ran 𝐹 ) = ( ( TopOpen ‘ ℂfld ) ↾t ran 𝐹 )
100 61 98 99 cncfcn ⊢ ( ( ( -∞ (,) +∞ ) ⊆ ℂ ∧ ran 𝐹 ⊆ ℂ ) → ( ( -∞ (,) +∞ ) –cn→ ran 𝐹 ) = ( ( topGen ‘ ran (,) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ran 𝐹 ) ) )
101 53 94 100 syl2anc ⊢ ( 𝜑 → ( ( -∞ (,) +∞ ) –cn→ ran 𝐹 ) = ( ( topGen ‘ ran (,) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ran 𝐹 ) ) )
102 101 eqcomd ⊢ ( 𝜑 → ( ( topGen ‘ ran (,) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ran 𝐹 ) ) = ( ( -∞ (,) +∞ ) –cn→ ran 𝐹 ) )
103 86 102 eleqtrd ⊢ ( 𝜑 → 𝐺 ∈ ( ( -∞ (,) +∞ ) –cn→ ran 𝐹 ) )
104 96 103 sseldd ⊢ ( 𝜑 → 𝐺 ∈ ( ( -∞ (,) +∞ ) –cn→ ℂ ) )
105 93 104 eqeltrrd ⊢ ( 𝜑 → ( 𝑤 ∈ ( -∞ (,) +∞ ) ↦ ( 𝐺 ‘ 𝑤 ) ) ∈ ( ( -∞ (,) +∞ ) –cn→ ℂ ) )
106 fveq2 ⊢ ( 𝑤 = 𝐴 → ( 𝐺 ‘ 𝑤 ) = ( 𝐺 ‘ 𝐴 ) )
107 3 4 5 45 47 56 7 105 12 106 14 15 itgsubst ⊢ ( 𝜑 → ⨜ [ 𝐾 → 𝐿 ] ( 𝐺 ‘ 𝑤 ) d 𝑤 = ⨜ [ 𝑋 → 𝑌 ] ( ( 𝐺 ‘ 𝐴 ) · 𝐵 ) d 𝑥 )
108 22 43 107 3eqtr3a ⊢ ( 𝜑 → ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 = ⨜ [ 𝑋 → 𝑌 ] ( ( 𝐺 ‘ 𝐴 ) · 𝐵 ) d 𝑥 )
109 2 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐺 = ( 𝑢 ∈ ℝ ↦ if ( 𝑢 ∈ ( 𝐾 [,] 𝐿 ) , ( 𝐹 ‘ 𝑢 ) , if ( 𝑢 < 𝐾 , ( 𝐹 ‘ 𝐾 ) , ( 𝐹 ‘ 𝐿 ) ) ) ) )
110 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑢 = 𝐴 ) → 𝑢 = 𝐴 )
111 61 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
112 3 4 iccssred ⊢ ( 𝜑 → ( 𝑋 [,] 𝑌 ) ⊆ ℝ )
113 112 52 sstrdi ⊢ ( 𝜑 → ( 𝑋 [,] 𝑌 ) ⊆ ℂ )
114 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ( 𝑋 [,] 𝑌 ) ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝑋 [,] 𝑌 ) ) ∈ ( TopOn ‘ ( 𝑋 [,] 𝑌 ) ) )
115 111 113 114 sylancr ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝑋 [,] 𝑌 ) ) ∈ ( TopOn ‘ ( 𝑋 [,] 𝑌 ) ) )
116 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ( 𝐾 [,] 𝐿 ) ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐾 [,] 𝐿 ) ) ∈ ( TopOn ‘ ( 𝐾 [,] 𝐿 ) ) )
117 111 64 116 sylancr ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐾 [,] 𝐿 ) ) ∈ ( TopOn ‘ ( 𝐾 [,] 𝐿 ) ) )
118 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝑋 [,] 𝑌 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝑋 [,] 𝑌 ) )
119 61 118 66 cncfcn ⊢ ( ( ( 𝑋 [,] 𝑌 ) ⊆ ℂ ∧ ( 𝐾 [,] 𝐿 ) ⊆ ℂ ) → ( ( 𝑋 [,] 𝑌 ) –cn→ ( 𝐾 [,] 𝐿 ) ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝑋 [,] 𝑌 ) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐾 [,] 𝐿 ) ) ) )
120 113 64 119 syl2anc ⊢ ( 𝜑 → ( ( 𝑋 [,] 𝑌 ) –cn→ ( 𝐾 [,] 𝐿 ) ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝑋 [,] 𝑌 ) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐾 [,] 𝐿 ) ) ) )
121 6 120 eleqtrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝑋 [,] 𝑌 ) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐾 [,] 𝐿 ) ) ) )
122 cnf2 ⊢ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝑋 [,] 𝑌 ) ) ∈ ( TopOn ‘ ( 𝑋 [,] 𝑌 ) ) ∧ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐾 [,] 𝐿 ) ) ∈ ( TopOn ‘ ( 𝐾 [,] 𝐿 ) ) ∧ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝑋 [,] 𝑌 ) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐾 [,] 𝐿 ) ) ) ) → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ( 𝐾 [,] 𝐿 ) )
123 115 117 121 122 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ( 𝐾 [,] 𝐿 ) )
124 123 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ( 𝐾 [,] 𝐿 ) )
125 eqid ⊢ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) = ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 )
126 125 fmpt ⊢ ( ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) 𝐴 ∈ ( 𝐾 [,] 𝐿 ) ↔ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ( 𝐾 [,] 𝐿 ) )
127 124 126 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) 𝐴 ∈ ( 𝐾 [,] 𝐿 ) )
128 ioossicc ⊢ ( 𝑋 (,) 𝑌 ) ⊆ ( 𝑋 [,] 𝑌 )
129 128 sseli ⊢ ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) → 𝑥 ∈ ( 𝑋 [,] 𝑌 ) )
130 129 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑥 ∈ ( 𝑋 [,] 𝑌 ) )
131 rsp ⊢ ( ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) 𝐴 ∈ ( 𝐾 [,] 𝐿 ) → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) → 𝐴 ∈ ( 𝐾 [,] 𝐿 ) ) )
132 127 130 131 sylc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐴 ∈ ( 𝐾 [,] 𝐿 ) )
133 132 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑢 = 𝐴 ) → 𝐴 ∈ ( 𝐾 [,] 𝐿 ) )
134 110 133 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑢 = 𝐴 ) → 𝑢 ∈ ( 𝐾 [,] 𝐿 ) )
135 134 iftrued ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑢 = 𝐴 ) → if ( 𝑢 ∈ ( 𝐾 [,] 𝐿 ) , ( 𝐹 ‘ 𝑢 ) , if ( 𝑢 < 𝐾 , ( 𝐹 ‘ 𝐾 ) , ( 𝐹 ‘ 𝐿 ) ) ) = ( 𝐹 ‘ 𝑢 ) )
136 simpll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑢 = 𝐴 ) → 𝜑 )
137 136 134 34 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑢 = 𝐴 ) → 𝐶 ∈ ℂ )
138 134 137 36 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑢 = 𝐴 ) → ( 𝐹 ‘ 𝑢 ) = 𝐶 )
139 13 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑢 = 𝐴 ) → 𝐶 = 𝐸 )
140 135 138 139 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑢 = 𝐴 ) → if ( 𝑢 ∈ ( 𝐾 [,] 𝐿 ) , ( 𝐹 ‘ 𝑢 ) , if ( 𝑢 < 𝐾 , ( 𝐹 ‘ 𝐾 ) , ( 𝐹 ‘ 𝐿 ) ) ) = 𝐸 )
141 23 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝐾 [,] 𝐿 ) ⊆ ℝ )
142 141 132 sseldd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐴 ∈ ℝ )
143 elex ⊢ ( 𝐴 ∈ ( 𝐾 [,] 𝐿 ) → 𝐴 ∈ V )
144 132 143 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐴 ∈ V )
145 isset ⊢ ( 𝐴 ∈ V ↔ ∃ 𝑢 𝑢 = 𝐴 )
146 144 145 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ∃ 𝑢 𝑢 = 𝐴 )
147 139 137 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑢 = 𝐴 ) → 𝐸 ∈ ℂ )
148 146 147 exlimddv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐸 ∈ ℂ )
149 109 140 142 148 fvmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝐺 ‘ 𝐴 ) = 𝐸 )
150 149 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( 𝐺 ‘ 𝐴 ) · 𝐵 ) = ( 𝐸 · 𝐵 ) )
151 5 150 ditgeq3d ⊢ ( 𝜑 → ⨜ [ 𝑋 → 𝑌 ] ( ( 𝐺 ‘ 𝐴 ) · 𝐵 ) d 𝑥 = ⨜ [ 𝑋 → 𝑌 ] ( 𝐸 · 𝐵 ) d 𝑥 )
152 108 151 eqtrd ⊢ ( 𝜑 → ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 = ⨜ [ 𝑋 → 𝑌 ] ( 𝐸 · 𝐵 ) d 𝑥 )