Theorem itgsubstlem

Description: Lemma for itgsubst . (Contributed by Mario Carneiro, 12-Sep-2014)

	Ref	Expression
Hypotheses	itgsubst.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
	itgsubst.y	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
	itgsubst.le	⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
	itgsubst.z	⊢ ( 𝜑 → 𝑍 ∈ ℝ* )
	itgsubst.w	⊢ ( 𝜑 → 𝑊 ∈ ℝ* )
	itgsubst.a	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ( 𝑍 (,) 𝑊 ) ) )
	itgsubst.b	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ ( ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) ∩ 𝐿1 ) )
	itgsubst.c	⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) ∈ ( ( 𝑍 (,) 𝑊 ) –cn→ ℂ ) )
	itgsubst.da	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) )
	itgsubst.e	⊢ ( 𝑢 = 𝐴 → 𝐶 = 𝐸 )
	itgsubst.k	⊢ ( 𝑥 = 𝑋 → 𝐴 = 𝐾 )
	itgsubst.l	⊢ ( 𝑥 = 𝑌 → 𝐴 = 𝐿 )
	itgsubst.m	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑍 (,) 𝑊 ) )
	itgsubst.n	⊢ ( 𝜑 → 𝑁 ∈ ( 𝑍 (,) 𝑊 ) )
	itgsubst.cl2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝐴 ∈ ( 𝑀 (,) 𝑁 ) )
Assertion	itgsubstlem	⊢ ( 𝜑 → ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 = ⨜ [ 𝑋 → 𝑌 ] ( 𝐸 · 𝐵 ) d 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		itgsubst.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
2		itgsubst.y	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
3		itgsubst.le	⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
4		itgsubst.z	⊢ ( 𝜑 → 𝑍 ∈ ℝ* )
5		itgsubst.w	⊢ ( 𝜑 → 𝑊 ∈ ℝ* )
6		itgsubst.a	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ( 𝑍 (,) 𝑊 ) ) )
7		itgsubst.b	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ ( ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) ∩ 𝐿1 ) )
8		itgsubst.c	⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) ∈ ( ( 𝑍 (,) 𝑊 ) –cn→ ℂ ) )
9		itgsubst.da	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) )
10		itgsubst.e	⊢ ( 𝑢 = 𝐴 → 𝐶 = 𝐸 )
11		itgsubst.k	⊢ ( 𝑥 = 𝑋 → 𝐴 = 𝐾 )
12		itgsubst.l	⊢ ( 𝑥 = 𝑌 → 𝐴 = 𝐿 )
13		itgsubst.m	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑍 (,) 𝑊 ) )
14		itgsubst.n	⊢ ( 𝜑 → 𝑁 ∈ ( 𝑍 (,) 𝑊 ) )
15		itgsubst.cl2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝐴 ∈ ( 𝑀 (,) 𝑁 ) )
16	3	ditgpos	⊢ ( 𝜑 → ⨜ [ 𝑋 → 𝑌 ] ( 𝐸 · 𝐵 ) d 𝑥 = ∫ ( 𝑋 (,) 𝑌 ) ( 𝐸 · 𝐵 ) d 𝑥 )
17		ax-resscn	⊢ ℝ ⊆ ℂ
18	17	a1i	⊢ ( 𝜑 → ℝ ⊆ ℂ )
19		iccssre	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( 𝑋 [,] 𝑌 ) ⊆ ℝ )
20	1 2 19	syl2anc	⊢ ( 𝜑 → ( 𝑋 [,] 𝑌 ) ⊆ ℝ )
21		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) = ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) )
22		eqidd	⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) = ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) )
23		oveq2	⊢ ( 𝑣 = 𝐴 → ( 𝑀 (,) 𝑣 ) = ( 𝑀 (,) 𝐴 ) )
24		itgeq1	⊢ ( ( 𝑀 (,) 𝑣 ) = ( 𝑀 (,) 𝐴 ) → ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 = ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 )
25	23 24	syl	⊢ ( 𝑣 = 𝐴 → ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 = ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 )
26	15 21 22 25	fmptco	⊢ ( 𝜑 → ( ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) ∘ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) )
27	15	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ( 𝑀 (,) 𝑁 ) )
28		ioossicc	⊢ ( 𝑀 (,) 𝑁 ) ⊆ ( 𝑀 [,] 𝑁 )
29		eliooord	⊢ ( 𝑀 ∈ ( 𝑍 (,) 𝑊 ) → ( 𝑍 < 𝑀 ∧ 𝑀 < 𝑊 ) )
30	13 29	syl	⊢ ( 𝜑 → ( 𝑍 < 𝑀 ∧ 𝑀 < 𝑊 ) )
31	30	simpld	⊢ ( 𝜑 → 𝑍 < 𝑀 )
32		eliooord	⊢ ( 𝑁 ∈ ( 𝑍 (,) 𝑊 ) → ( 𝑍 < 𝑁 ∧ 𝑁 < 𝑊 ) )
33	14 32	syl	⊢ ( 𝜑 → ( 𝑍 < 𝑁 ∧ 𝑁 < 𝑊 ) )
34	33	simprd	⊢ ( 𝜑 → 𝑁 < 𝑊 )
35		iccssioo	⊢ ( ( ( 𝑍 ∈ ℝ* ∧ 𝑊 ∈ ℝ* ) ∧ ( 𝑍 < 𝑀 ∧ 𝑁 < 𝑊 ) ) → ( 𝑀 [,] 𝑁 ) ⊆ ( 𝑍 (,) 𝑊 ) )
36	4 5 31 34 35	syl22anc	⊢ ( 𝜑 → ( 𝑀 [,] 𝑁 ) ⊆ ( 𝑍 (,) 𝑊 ) )
37	28 36	sstrid	⊢ ( 𝜑 → ( 𝑀 (,) 𝑁 ) ⊆ ( 𝑍 (,) 𝑊 ) )
38		ioossre	⊢ ( 𝑍 (,) 𝑊 ) ⊆ ℝ
39	38	a1i	⊢ ( 𝜑 → ( 𝑍 (,) 𝑊 ) ⊆ ℝ )
40	39 17	sstrdi	⊢ ( 𝜑 → ( 𝑍 (,) 𝑊 ) ⊆ ℂ )
41	37 40	sstrd	⊢ ( 𝜑 → ( 𝑀 (,) 𝑁 ) ⊆ ℂ )
42		cncfcdm	⊢ ( ( ( 𝑀 (,) 𝑁 ) ⊆ ℂ ∧ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ( 𝑍 (,) 𝑊 ) ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ( 𝑀 (,) 𝑁 ) ) ↔ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ( 𝑀 (,) 𝑁 ) ) )
43	41 6 42	syl2anc	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ( 𝑀 (,) 𝑁 ) ) ↔ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ( 𝑀 (,) 𝑁 ) ) )
44	27 43	mpbird	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ( 𝑀 (,) 𝑁 ) ) )
45	28	sseli	⊢ ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) → 𝑣 ∈ ( 𝑀 [,] 𝑁 ) )
46	38 14	sselid	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
47	46	rexrd	⊢ ( 𝜑 → 𝑁 ∈ ℝ* )
48	47	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ) → 𝑁 ∈ ℝ* )
49	38 13	sselid	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
50		elicc2	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ↔ ( 𝑣 ∈ ℝ ∧ 𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁 ) ) )
51	49 46 50	syl2anc	⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ↔ ( 𝑣 ∈ ℝ ∧ 𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁 ) ) )
52	51	biimpa	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ) → ( 𝑣 ∈ ℝ ∧ 𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁 ) )
53	52	simp3d	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ) → 𝑣 ≤ 𝑁 )
54		iooss2	⊢ ( ( 𝑁 ∈ ℝ* ∧ 𝑣 ≤ 𝑁 ) → ( 𝑀 (,) 𝑣 ) ⊆ ( 𝑀 (,) 𝑁 ) )
55	48 53 54	syl2anc	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ) → ( 𝑀 (,) 𝑣 ) ⊆ ( 𝑀 (,) 𝑁 ) )
56	55	sselda	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ 𝑢 ∈ ( 𝑀 (,) 𝑣 ) ) → 𝑢 ∈ ( 𝑀 (,) 𝑁 ) )
57	37	sselda	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝑢 ∈ ( 𝑍 (,) 𝑊 ) )
58		cncff	⊢ ( ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) ∈ ( ( 𝑍 (,) 𝑊 ) –cn→ ℂ ) → ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) : ( 𝑍 (,) 𝑊 ) ⟶ ℂ )
59	8 58	syl	⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) : ( 𝑍 (,) 𝑊 ) ⟶ ℂ )
60	59	fvmptelcdm	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ) → 𝐶 ∈ ℂ )
61	57 60	syldan	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝐶 ∈ ℂ )
62	61	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝐶 ∈ ℂ )
63	56 62	syldan	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ 𝑢 ∈ ( 𝑀 (,) 𝑣 ) ) → 𝐶 ∈ ℂ )
64		ioombl	⊢ ( 𝑀 (,) 𝑣 ) ∈ dom vol
65	64	a1i	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ) → ( 𝑀 (,) 𝑣 ) ∈ dom vol )
66	28	a1i	⊢ ( 𝜑 → ( 𝑀 (,) 𝑁 ) ⊆ ( 𝑀 [,] 𝑁 ) )
67		ioombl	⊢ ( 𝑀 (,) 𝑁 ) ∈ dom vol
68	67	a1i	⊢ ( 𝜑 → ( 𝑀 (,) 𝑁 ) ∈ dom vol )
69	36	sselda	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑀 [,] 𝑁 ) ) → 𝑢 ∈ ( 𝑍 (,) 𝑊 ) )
70	69 60	syldan	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑀 [,] 𝑁 ) ) → 𝐶 ∈ ℂ )
71	36	resmptd	⊢ ( 𝜑 → ( ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) ↾ ( 𝑀 [,] 𝑁 ) ) = ( 𝑢 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐶 ) )
72		rescncf	⊢ ( ( 𝑀 [,] 𝑁 ) ⊆ ( 𝑍 (,) 𝑊 ) → ( ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) ∈ ( ( 𝑍 (,) 𝑊 ) –cn→ ℂ ) → ( ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) ↾ ( 𝑀 [,] 𝑁 ) ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℂ ) ) )
73	36 8 72	sylc	⊢ ( 𝜑 → ( ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) ↾ ( 𝑀 [,] 𝑁 ) ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℂ ) )
74	71 73	eqeltrrd	⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐶 ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℂ ) )
75		cniccibl	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 𝑢 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐶 ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℂ ) ) → ( 𝑢 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐶 ) ∈ 𝐿1 )
76	49 46 74 75	syl3anc	⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐶 ) ∈ 𝐿1 )
77	66 68 70 76	iblss	⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ∈ 𝐿1 )
78	77	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ) → ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ∈ 𝐿1 )
79	55 65 62 78	iblss	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ) → ( 𝑢 ∈ ( 𝑀 (,) 𝑣 ) ↦ 𝐶 ) ∈ 𝐿1 )
80	63 79	itgcl	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ) → ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ∈ ℂ )
81	45 80	sylan2	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ) → ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ∈ ℂ )
82	81	fmpttd	⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) : ( 𝑀 (,) 𝑁 ) ⟶ ℂ )
83	37 38	sstrdi	⊢ ( 𝜑 → ( 𝑀 (,) 𝑁 ) ⊆ ℝ )
84		fveq2	⊢ ( 𝑡 = 𝑢 → ( ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ‘ 𝑡 ) = ( ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ‘ 𝑢 ) )
85		nffvmpt1	⊢ Ⅎ 𝑢 ( ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ‘ 𝑡 )
86		nfcv	⊢ Ⅎ 𝑡 ( ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ‘ 𝑢 )
87	84 85 86	cbvitg	⊢ ∫ ( 𝑀 (,) 𝑣 ) ( ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ‘ 𝑡 ) d 𝑡 = ∫ ( 𝑀 (,) 𝑣 ) ( ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ‘ 𝑢 ) d 𝑢
88		eqid	⊢ ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) = ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 )
89	88	fvmpt2	⊢ ( ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ∧ 𝐶 ∈ ℂ ) → ( ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ‘ 𝑢 ) = 𝐶 )
90	56 63 89	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ 𝑢 ∈ ( 𝑀 (,) 𝑣 ) ) → ( ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ‘ 𝑢 ) = 𝐶 )
91	90	itgeq2dv	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ) → ∫ ( 𝑀 (,) 𝑣 ) ( ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ‘ 𝑢 ) d 𝑢 = ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 )
92	87 91	eqtrid	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ) → ∫ ( 𝑀 (,) 𝑣 ) ( ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ‘ 𝑡 ) d 𝑡 = ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 )
93	92	mpteq2dva	⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) ( ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ‘ 𝑡 ) d 𝑡 ) = ( 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) )
94	93	oveq2d	⊢ ( 𝜑 → ( ℝ D ( 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) ( ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ‘ 𝑡 ) d 𝑡 ) ) = ( ℝ D ( 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) ) )
95		eqid	⊢ ( 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) ( ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ‘ 𝑡 ) d 𝑡 ) = ( 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) ( ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ‘ 𝑡 ) d 𝑡 )
96	1	rexrd	⊢ ( 𝜑 → 𝑋 ∈ ℝ* )
97	2	rexrd	⊢ ( 𝜑 → 𝑌 ∈ ℝ* )
98		lbicc2	⊢ ( ( 𝑋 ∈ ℝ* ∧ 𝑌 ∈ ℝ* ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ∈ ( 𝑋 [,] 𝑌 ) )
99	96 97 3 98	syl3anc	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑋 [,] 𝑌 ) )
100		n0i	⊢ ( 𝑋 ∈ ( 𝑋 [,] 𝑌 ) → ¬ ( 𝑋 [,] 𝑌 ) = ∅ )
101	99 100	syl	⊢ ( 𝜑 → ¬ ( 𝑋 [,] 𝑌 ) = ∅ )
102		feq3	⊢ ( ( 𝑀 (,) 𝑁 ) = ∅ → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ( 𝑀 (,) 𝑁 ) ↔ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ∅ ) )
103	27 102	syl5ibcom	⊢ ( 𝜑 → ( ( 𝑀 (,) 𝑁 ) = ∅ → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ∅ ) )
104		f00	⊢ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ∅ ↔ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) = ∅ ∧ ( 𝑋 [,] 𝑌 ) = ∅ ) )
105	104	simprbi	⊢ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ∅ → ( 𝑋 [,] 𝑌 ) = ∅ )
106	103 105	syl6	⊢ ( 𝜑 → ( ( 𝑀 (,) 𝑁 ) = ∅ → ( 𝑋 [,] 𝑌 ) = ∅ ) )
107	101 106	mtod	⊢ ( 𝜑 → ¬ ( 𝑀 (,) 𝑁 ) = ∅ )
108	49	rexrd	⊢ ( 𝜑 → 𝑀 ∈ ℝ* )
109		ioo0	⊢ ( ( 𝑀 ∈ ℝ* ∧ 𝑁 ∈ ℝ* ) → ( ( 𝑀 (,) 𝑁 ) = ∅ ↔ 𝑁 ≤ 𝑀 ) )
110	108 47 109	syl2anc	⊢ ( 𝜑 → ( ( 𝑀 (,) 𝑁 ) = ∅ ↔ 𝑁 ≤ 𝑀 ) )
111	107 110	mtbid	⊢ ( 𝜑 → ¬ 𝑁 ≤ 𝑀 )
112	46 49	letrid	⊢ ( 𝜑 → ( 𝑁 ≤ 𝑀 ∨ 𝑀 ≤ 𝑁 ) )
113	112	ord	⊢ ( 𝜑 → ( ¬ 𝑁 ≤ 𝑀 → 𝑀 ≤ 𝑁 ) )
114	111 113	mpd	⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
115		resmpt	⊢ ( ( 𝑀 (,) 𝑁 ) ⊆ ( 𝑀 [,] 𝑁 ) → ( ( 𝑢 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐶 ) ↾ ( 𝑀 (,) 𝑁 ) ) = ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) )
116	28 115	ax-mp	⊢ ( ( 𝑢 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐶 ) ↾ ( 𝑀 (,) 𝑁 ) ) = ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 )
117		rescncf	⊢ ( ( 𝑀 (,) 𝑁 ) ⊆ ( 𝑀 [,] 𝑁 ) → ( ( 𝑢 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐶 ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℂ ) → ( ( 𝑢 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐶 ) ↾ ( 𝑀 (,) 𝑁 ) ) ∈ ( ( 𝑀 (,) 𝑁 ) –cn→ ℂ ) ) )
118	28 74 117	mpsyl	⊢ ( 𝜑 → ( ( 𝑢 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐶 ) ↾ ( 𝑀 (,) 𝑁 ) ) ∈ ( ( 𝑀 (,) 𝑁 ) –cn→ ℂ ) )
119	116 118	eqeltrrid	⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ∈ ( ( 𝑀 (,) 𝑁 ) –cn→ ℂ ) )
120	95 49 46 114 119 77	ftc1cn	⊢ ( 𝜑 → ( ℝ D ( 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) ( ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ‘ 𝑡 ) d 𝑡 ) ) = ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) )
121	36 38	sstrdi	⊢ ( 𝜑 → ( 𝑀 [,] 𝑁 ) ⊆ ℝ )
122		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
123	122	tgioo2	⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
124		iccntr	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑀 [,] 𝑁 ) ) = ( 𝑀 (,) 𝑁 ) )
125	49 46 124	syl2anc	⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑀 [,] 𝑁 ) ) = ( 𝑀 (,) 𝑁 ) )
126	18 121 80 123 122 125	dvmptntr	⊢ ( 𝜑 → ( ℝ D ( 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) ) = ( ℝ D ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) ) )
127	94 120 126	3eqtr3rd	⊢ ( 𝜑 → ( ℝ D ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) ) = ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) )
128	127	dmeqd	⊢ ( 𝜑 → dom ( ℝ D ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) ) = dom ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) )
129	88 61	dmmptd	⊢ ( 𝜑 → dom ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) = ( 𝑀 (,) 𝑁 ) )
130	128 129	eqtrd	⊢ ( 𝜑 → dom ( ℝ D ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) ) = ( 𝑀 (,) 𝑁 ) )
131		dvcn	⊢ ( ( ( ℝ ⊆ ℂ ∧ ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) : ( 𝑀 (,) 𝑁 ) ⟶ ℂ ∧ ( 𝑀 (,) 𝑁 ) ⊆ ℝ ) ∧ dom ( ℝ D ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) ) = ( 𝑀 (,) 𝑁 ) ) → ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) ∈ ( ( 𝑀 (,) 𝑁 ) –cn→ ℂ ) )
132	18 82 83 130 131	syl31anc	⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) ∈ ( ( 𝑀 (,) 𝑁 ) –cn→ ℂ ) )
133	44 132	cncfco	⊢ ( 𝜑 → ( ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) ∘ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℂ ) )
134	26 133	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℂ ) )
135		cncff	⊢ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℂ ) → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) : ( 𝑋 [,] 𝑌 ) ⟶ ℂ )
136	134 135	syl	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) : ( 𝑋 [,] 𝑌 ) ⟶ ℂ )
137	136	fvmptelcdm	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) → ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ∈ ℂ )
138		iccntr	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑋 [,] 𝑌 ) ) = ( 𝑋 (,) 𝑌 ) )
139	1 2 138	syl2anc	⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑋 [,] 𝑌 ) ) = ( 𝑋 (,) 𝑌 ) )
140	18 20 137 123 122 139	dvmptntr	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) = ( ℝ D ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) )
141		reelprrecn	⊢ ℝ ∈ { ℝ , ℂ }
142	141	a1i	⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
143		ioossicc	⊢ ( 𝑋 (,) 𝑌 ) ⊆ ( 𝑋 [,] 𝑌 )
144	143	sseli	⊢ ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) → 𝑥 ∈ ( 𝑋 [,] 𝑌 ) )
145	144 15	sylan2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐴 ∈ ( 𝑀 (,) 𝑁 ) )
146		elin	⊢ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ ( ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) ∩ 𝐿1 ) ↔ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) ∧ ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ 𝐿1 ) )
147	7 146	sylib	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) ∧ ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ 𝐿1 ) )
148	147	simpld	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
149		cncff	⊢ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) : ( 𝑋 (,) 𝑌 ) ⟶ ℂ )
150	148 149	syl	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) : ( 𝑋 (,) 𝑌 ) ⟶ ℂ )
151	150	fvmptelcdm	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐵 ∈ ℂ )
152	61	fmpttd	⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) : ( 𝑀 (,) 𝑁 ) ⟶ ℂ )
153		nfcv	⊢ Ⅎ 𝑣 𝐶
154		nfcsb1v	⊢ Ⅎ 𝑢 ⦋ 𝑣 / 𝑢 ⦌ 𝐶
155		csbeq1a	⊢ ( 𝑢 = 𝑣 → 𝐶 = ⦋ 𝑣 / 𝑢 ⦌ 𝐶 )
156	153 154 155	cbvmpt	⊢ ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) = ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ↦ ⦋ 𝑣 / 𝑢 ⦌ 𝐶 )
157	156	fmpt	⊢ ( ∀ 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ⦋ 𝑣 / 𝑢 ⦌ 𝐶 ∈ ℂ ↔ ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) : ( 𝑀 (,) 𝑁 ) ⟶ ℂ )
158	152 157	sylibr	⊢ ( 𝜑 → ∀ 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ⦋ 𝑣 / 𝑢 ⦌ 𝐶 ∈ ℂ )
159	158	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ) → ⦋ 𝑣 / 𝑢 ⦌ 𝐶 ∈ ℂ )
160	38 17	sstri	⊢ ( 𝑍 (,) 𝑊 ) ⊆ ℂ
161		cncff	⊢ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ( 𝑍 (,) 𝑊 ) ) → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ( 𝑍 (,) 𝑊 ) )
162	6 161	syl	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ( 𝑍 (,) 𝑊 ) )
163	162	fvmptelcdm	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝐴 ∈ ( 𝑍 (,) 𝑊 ) )
164	160 163	sselid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝐴 ∈ ℂ )
165	18 20 164 123 122 139	dvmptntr	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ) = ( ℝ D ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐴 ) ) )
166	165 9	eqtr3d	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) )
167	127 156	eqtrdi	⊢ ( 𝜑 → ( ℝ D ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) ) = ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ↦ ⦋ 𝑣 / 𝑢 ⦌ 𝐶 ) )
168		csbeq1	⊢ ( 𝑣 = 𝐴 → ⦋ 𝑣 / 𝑢 ⦌ 𝐶 = ⦋ 𝐴 / 𝑢 ⦌ 𝐶 )
169	142 142 145 151 81 159 166 167 25 168	dvmptco	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ⦋ 𝐴 / 𝑢 ⦌ 𝐶 · 𝐵 ) ) )
170		nfcvd	⊢ ( 𝐴 ∈ ( 𝑀 (,) 𝑁 ) → Ⅎ 𝑢 𝐸 )
171	170 10	csbiegf	⊢ ( 𝐴 ∈ ( 𝑀 (,) 𝑁 ) → ⦋ 𝐴 / 𝑢 ⦌ 𝐶 = 𝐸 )
172	145 171	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ⦋ 𝐴 / 𝑢 ⦌ 𝐶 = 𝐸 )
173	172	oveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ⦋ 𝐴 / 𝑢 ⦌ 𝐶 · 𝐵 ) = ( 𝐸 · 𝐵 ) )
174	173	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ⦋ 𝐴 / 𝑢 ⦌ 𝐶 · 𝐵 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 · 𝐵 ) ) )
175	140 169 174	3eqtrd	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 · 𝐵 ) ) )
176		resmpt	⊢ ( ( 𝑋 (,) 𝑌 ) ⊆ ( 𝑋 [,] 𝑌 ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ↾ ( 𝑋 (,) 𝑌 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) )
177	143 176	ax-mp	⊢ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ↾ ( 𝑋 (,) 𝑌 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 )
178		eqidd	⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) = ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) )
179	163 21 178 10	fmptco	⊢ ( 𝜑 → ( ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) ∘ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) )
180	6 8	cncfco	⊢ ( 𝜑 → ( ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) ∘ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℂ ) )
181	179 180	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℂ ) )
182		rescncf	⊢ ( ( 𝑋 (,) 𝑌 ) ⊆ ( 𝑋 [,] 𝑌 ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℂ ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ↾ ( 𝑋 (,) 𝑌 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) ) )
183	143 181 182	mpsyl	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ↾ ( 𝑋 (,) 𝑌 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
184	177 183	eqeltrrid	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
185	184 148	mulcncf	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 · 𝐵 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
186	175 185	eqeltrd	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
187		ioombl	⊢ ( 𝑋 (,) 𝑌 ) ∈ dom vol
188	187	a1i	⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ∈ dom vol )
189		fco	⊢ ( ( ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) : ( 𝑍 (,) 𝑊 ) ⟶ ℂ ∧ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ( 𝑍 (,) 𝑊 ) ) → ( ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) ∘ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ) : ( 𝑋 [,] 𝑌 ) ⟶ ℂ )
190	59 162 189	syl2anc	⊢ ( 𝜑 → ( ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) ∘ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ) : ( 𝑋 [,] 𝑌 ) ⟶ ℂ )
191	179	feq1d	⊢ ( 𝜑 → ( ( ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) ∘ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ) : ( 𝑋 [,] 𝑌 ) ⟶ ℂ ↔ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) : ( 𝑋 [,] 𝑌 ) ⟶ ℂ ) )
192	190 191	mpbid	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) : ( 𝑋 [,] 𝑌 ) ⟶ ℂ )
193	192	fvmptelcdm	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝐸 ∈ ℂ )
194	144 193	sylan2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐸 ∈ ℂ )
195		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) )
196		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) )
197	188 194 151 195 196	offval2	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ∘f · ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 · 𝐵 ) ) )
198	175 197	eqtr4d	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) = ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ∘f · ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ) )
199	143	a1i	⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ⊆ ( 𝑋 [,] 𝑌 ) )
200		cniccibl	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℂ ) ) → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ∈ 𝐿1 )
201	1 2 181 200	syl3anc	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ∈ 𝐿1 )
202	199 188 193 201	iblss	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ∈ 𝐿1 )
203		iblmbf	⊢ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ∈ 𝐿1 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ∈ MblFn )
204	202 203	syl	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ∈ MblFn )
205	147	simprd	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ 𝐿1 )
206		cniccbdd	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℂ ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 )
207	1 2 181 206	syl3anc	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 )
208		ssralv	⊢ ( ( 𝑋 (,) 𝑌 ) ⊆ ( 𝑋 [,] 𝑌 ) → ( ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 → ∀ 𝑧 ∈ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 ) )
209	143 208	ax-mp	⊢ ( ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 → ∀ 𝑧 ∈ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 )
210		eqid	⊢ ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 )
211	210 194	dmmptd	⊢ ( 𝜑 → dom ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) = ( 𝑋 (,) 𝑌 ) )
212	211	raleqdv	⊢ ( 𝜑 → ( ∀ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 ↔ ∀ 𝑧 ∈ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 ) )
213	177	fveq1i	⊢ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑧 ) = ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 )
214		fvres	⊢ ( 𝑧 ∈ ( 𝑋 (,) 𝑌 ) → ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑧 ) = ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) )
215	213 214	eqtr3id	⊢ ( 𝑧 ∈ ( 𝑋 (,) 𝑌 ) → ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) = ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) )
216	215	fveq2d	⊢ ( 𝑧 ∈ ( 𝑋 (,) 𝑌 ) → ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) = ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) )
217	216	breq1d	⊢ ( 𝑧 ∈ ( 𝑋 (,) 𝑌 ) → ( ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 ↔ ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 ) )
218	217	ralbiia	⊢ ( ∀ 𝑧 ∈ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 ↔ ∀ 𝑧 ∈ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 )
219	212 218	bitr2di	⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 ↔ ∀ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 ) )
220	209 219	imbitrid	⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 → ∀ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 ) )
221	220	reximdv	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 ) )
222	207 221	mpd	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 )
223		bddmulibl	⊢ ( ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ∈ MblFn ∧ ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ 𝐿1 ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 ) → ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ∘f · ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ) ∈ 𝐿1 )
224	204 205 222 223	syl3anc	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ∘f · ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ) ∈ 𝐿1 )
225	198 224	eqeltrd	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) ∈ 𝐿1 )
226	1 2 3 186 225 134	ftc2	⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) ‘ 𝑡 ) d 𝑡 = ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ‘ 𝑌 ) − ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ‘ 𝑋 ) ) )
227		fveq2	⊢ ( 𝑡 = 𝑥 → ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) ‘ 𝑡 ) = ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) ‘ 𝑥 ) )
228		nfcv	⊢ Ⅎ 𝑥 ℝ
229		nfcv	⊢ Ⅎ 𝑥 D
230		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 )
231	228 229 230	nfov	⊢ Ⅎ 𝑥 ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) )
232		nfcv	⊢ Ⅎ 𝑥 𝑡
233	231 232	nffv	⊢ Ⅎ 𝑥 ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) ‘ 𝑡 )
234		nfcv	⊢ Ⅎ 𝑡 ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) ‘ 𝑥 )
235	227 233 234	cbvitg	⊢ ∫ ( 𝑋 (,) 𝑌 ) ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) ‘ 𝑡 ) d 𝑡 = ∫ ( 𝑋 (,) 𝑌 ) ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) ‘ 𝑥 ) d 𝑥
236	175	fveq1d	⊢ ( 𝜑 → ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) ‘ 𝑥 ) = ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 · 𝐵 ) ) ‘ 𝑥 ) )
237		ovex	⊢ ( 𝐸 · 𝐵 ) ∈ V
238		eqid	⊢ ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 · 𝐵 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 · 𝐵 ) )
239	238	fvmpt2	⊢ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ∧ ( 𝐸 · 𝐵 ) ∈ V ) → ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 · 𝐵 ) ) ‘ 𝑥 ) = ( 𝐸 · 𝐵 ) )
240	237 239	mpan2	⊢ ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) → ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 · 𝐵 ) ) ‘ 𝑥 ) = ( 𝐸 · 𝐵 ) )
241	236 240	sylan9eq	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) ‘ 𝑥 ) = ( 𝐸 · 𝐵 ) )
242	241	itgeq2dv	⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) ‘ 𝑥 ) d 𝑥 = ∫ ( 𝑋 (,) 𝑌 ) ( 𝐸 · 𝐵 ) d 𝑥 )
243	235 242	eqtrid	⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) ‘ 𝑡 ) d 𝑡 = ∫ ( 𝑋 (,) 𝑌 ) ( 𝐸 · 𝐵 ) d 𝑥 )
244	28 15	sselid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝐴 ∈ ( 𝑀 [,] 𝑁 ) )
245		elicc2	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝐴 ∈ ( 𝑀 [,] 𝑁 ) ↔ ( 𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁 ) ) )
246	49 46 245	syl2anc	⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝑀 [,] 𝑁 ) ↔ ( 𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁 ) ) )
247	246	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) → ( 𝐴 ∈ ( 𝑀 [,] 𝑁 ) ↔ ( 𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁 ) ) )
248	244 247	mpbid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) → ( 𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁 ) )
249	248	simp2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑀 ≤ 𝐴 )
250	249	ditgpos	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) → ⨜ [ 𝑀 → 𝐴 ] 𝐶 d 𝑢 = ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 )
251	250	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⨜ [ 𝑀 → 𝐴 ] 𝐶 d 𝑢 ) = ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) )
252	251	fveq1d	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⨜ [ 𝑀 → 𝐴 ] 𝐶 d 𝑢 ) ‘ 𝑌 ) = ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ‘ 𝑌 ) )
253		ubicc2	⊢ ( ( 𝑋 ∈ ℝ* ∧ 𝑌 ∈ ℝ* ∧ 𝑋 ≤ 𝑌 ) → 𝑌 ∈ ( 𝑋 [,] 𝑌 ) )
254	96 97 3 253	syl3anc	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑋 [,] 𝑌 ) )
255		ditgeq2	⊢ ( 𝐴 = 𝐿 → ⨜ [ 𝑀 → 𝐴 ] 𝐶 d 𝑢 = ⨜ [ 𝑀 → 𝐿 ] 𝐶 d 𝑢 )
256	12 255	syl	⊢ ( 𝑥 = 𝑌 → ⨜ [ 𝑀 → 𝐴 ] 𝐶 d 𝑢 = ⨜ [ 𝑀 → 𝐿 ] 𝐶 d 𝑢 )
257		eqid	⊢ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⨜ [ 𝑀 → 𝐴 ] 𝐶 d 𝑢 ) = ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⨜ [ 𝑀 → 𝐴 ] 𝐶 d 𝑢 )
258		ditgex	⊢ ⨜ [ 𝑀 → 𝐿 ] 𝐶 d 𝑢 ∈ V
259	256 257 258	fvmpt	⊢ ( 𝑌 ∈ ( 𝑋 [,] 𝑌 ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⨜ [ 𝑀 → 𝐴 ] 𝐶 d 𝑢 ) ‘ 𝑌 ) = ⨜ [ 𝑀 → 𝐿 ] 𝐶 d 𝑢 )
260	254 259	syl	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⨜ [ 𝑀 → 𝐴 ] 𝐶 d 𝑢 ) ‘ 𝑌 ) = ⨜ [ 𝑀 → 𝐿 ] 𝐶 d 𝑢 )
261	252 260	eqtr3d	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ‘ 𝑌 ) = ⨜ [ 𝑀 → 𝐿 ] 𝐶 d 𝑢 )
262	251	fveq1d	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⨜ [ 𝑀 → 𝐴 ] 𝐶 d 𝑢 ) ‘ 𝑋 ) = ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ‘ 𝑋 ) )
263		ditgeq2	⊢ ( 𝐴 = 𝐾 → ⨜ [ 𝑀 → 𝐴 ] 𝐶 d 𝑢 = ⨜ [ 𝑀 → 𝐾 ] 𝐶 d 𝑢 )
264	11 263	syl	⊢ ( 𝑥 = 𝑋 → ⨜ [ 𝑀 → 𝐴 ] 𝐶 d 𝑢 = ⨜ [ 𝑀 → 𝐾 ] 𝐶 d 𝑢 )
265		ditgex	⊢ ⨜ [ 𝑀 → 𝐾 ] 𝐶 d 𝑢 ∈ V
266	264 257 265	fvmpt	⊢ ( 𝑋 ∈ ( 𝑋 [,] 𝑌 ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⨜ [ 𝑀 → 𝐴 ] 𝐶 d 𝑢 ) ‘ 𝑋 ) = ⨜ [ 𝑀 → 𝐾 ] 𝐶 d 𝑢 )
267	99 266	syl	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⨜ [ 𝑀 → 𝐴 ] 𝐶 d 𝑢 ) ‘ 𝑋 ) = ⨜ [ 𝑀 → 𝐾 ] 𝐶 d 𝑢 )
268	262 267	eqtr3d	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ‘ 𝑋 ) = ⨜ [ 𝑀 → 𝐾 ] 𝐶 d 𝑢 )
269	261 268	oveq12d	⊢ ( 𝜑 → ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ‘ 𝑌 ) − ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ‘ 𝑋 ) ) = ( ⨜ [ 𝑀 → 𝐿 ] 𝐶 d 𝑢 − ⨜ [ 𝑀 → 𝐾 ] 𝐶 d 𝑢 ) )
270		lbicc2	⊢ ( ( 𝑀 ∈ ℝ* ∧ 𝑁 ∈ ℝ* ∧ 𝑀 ≤ 𝑁 ) → 𝑀 ∈ ( 𝑀 [,] 𝑁 ) )
271	108 47 114 270	syl3anc	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑀 [,] 𝑁 ) )
272	11	eleq1d	⊢ ( 𝑥 = 𝑋 → ( 𝐴 ∈ ( 𝑀 [,] 𝑁 ) ↔ 𝐾 ∈ ( 𝑀 [,] 𝑁 ) ) )
273	244	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) 𝐴 ∈ ( 𝑀 [,] 𝑁 ) )
274	272 273 99	rspcdva	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑀 [,] 𝑁 ) )
275	12	eleq1d	⊢ ( 𝑥 = 𝑌 → ( 𝐴 ∈ ( 𝑀 [,] 𝑁 ) ↔ 𝐿 ∈ ( 𝑀 [,] 𝑁 ) ) )
276	275 273 254	rspcdva	⊢ ( 𝜑 → 𝐿 ∈ ( 𝑀 [,] 𝑁 ) )
277	49 46 271 274 276 61 77	ditgsplit	⊢ ( 𝜑 → ⨜ [ 𝑀 → 𝐿 ] 𝐶 d 𝑢 = ( ⨜ [ 𝑀 → 𝐾 ] 𝐶 d 𝑢 + ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 ) )
278	277	oveq1d	⊢ ( 𝜑 → ( ⨜ [ 𝑀 → 𝐿 ] 𝐶 d 𝑢 − ⨜ [ 𝑀 → 𝐾 ] 𝐶 d 𝑢 ) = ( ( ⨜ [ 𝑀 → 𝐾 ] 𝐶 d 𝑢 + ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 ) − ⨜ [ 𝑀 → 𝐾 ] 𝐶 d 𝑢 ) )
279	49 46 271 274 61 77	ditgcl	⊢ ( 𝜑 → ⨜ [ 𝑀 → 𝐾 ] 𝐶 d 𝑢 ∈ ℂ )
280	49 46 274 276 61 77	ditgcl	⊢ ( 𝜑 → ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 ∈ ℂ )
281	279 280	pncan2d	⊢ ( 𝜑 → ( ( ⨜ [ 𝑀 → 𝐾 ] 𝐶 d 𝑢 + ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 ) − ⨜ [ 𝑀 → 𝐾 ] 𝐶 d 𝑢 ) = ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 )
282	269 278 281	3eqtrd	⊢ ( 𝜑 → ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ‘ 𝑌 ) − ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ‘ 𝑋 ) ) = ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 )
283	226 243 282	3eqtr3d	⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐸 · 𝐵 ) d 𝑥 = ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 )
284	16 283	eqtr2d	⊢ ( 𝜑 → ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 = ⨜ [ 𝑋 → 𝑌 ] ( 𝐸 · 𝐵 ) d 𝑥 )