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	fvmptelcdm	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐾 [,] 𝐿 ) ) → 𝐶 ∈ ℂ )
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 𝑥 )