itgsubstlem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > itgsubstlem		Structured version Visualization version GIF version

Theorem itgsubstlem 26218

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

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

**Assertion**
Ref	Expression
itgsubstlem	⊢ (𝜑 → ⨜[𝐾 → 𝐿]𝐶 d𝑢 = ⨜[𝑋 → 𝑌](𝐸 · 𝐵) d𝑥)

Distinct variable groups: 𝑢,𝐸 𝑥,𝑢,𝐾 𝑢,𝑀,𝑥 𝜑,𝑢,𝑥 𝑢,𝑋,𝑥 𝑢,𝑌,𝑥 𝑢,𝐴 𝑥,𝐶 𝑢,𝑊,𝑥 𝑢,𝐿,𝑥 𝑢,𝑁,𝑥 𝑢,𝑍,𝑥 Allowed substitution hints: 𝐴(𝑥) 𝐵(𝑥, 𝑢) 𝐶(𝑢) 𝐸(𝑥)

Proof of Theorem itgsubstlem Dummy variables 𝑦 𝑧 𝑡 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		itgsubst.le	. . 3 ⊢ (𝜑 → 𝑋 ≤ 𝑌)
2	1	ditgpos 26026	. 2 ⊢ (𝜑 → ⨜[𝑋 → 𝑌](𝐸 · 𝐵) d𝑥 = ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥)
3		itgsubst.x	. . . 4 ⊢ (𝜑 → 𝑋 ∈ ℝ)
4		itgsubst.y	. . . 4 ⊢ (𝜑 → 𝑌 ∈ ℝ)
5		ax-resscn 11163	. . . . . . . 8 ⊢ ℝ ⊆ ℂ
6	5	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℝ ⊆ ℂ)
7		iccssre 13462	. . . . . . . 8 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑋[,]𝑌) ⊆ ℝ)
8	3, 4, 7	syl2anc 595	. . . . . . 7 ⊢ (𝜑 → (𝑋[,]𝑌) ⊆ ℝ)
9		itgsubst.cl2	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑀(,)𝑁))
10		eqidd 2763	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) = (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴))
11		eqidd 2763	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) = (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢))
12		oveq2 7420	. . . . . . . . . . . 12 ⊢ (𝑣 = 𝐴 → (𝑀(,)𝑣) = (𝑀(,)𝐴))
13		itgeq1 25943	. . . . . . . . . . . 12 ⊢ ((𝑀(,)𝑣) = (𝑀(,)𝐴) → ∫(𝑀(,)𝑣)𝐶 d𝑢 = ∫(𝑀(,)𝐴)𝐶 d𝑢)
14	12, 13	syl 18	. . . . . . . . . . 11 ⊢ (𝑣 = 𝐴 → ∫(𝑀(,)𝑣)𝐶 d𝑢 = ∫(𝑀(,)𝐴)𝐶 d𝑢)
15	9, 10, 11, 14	fmptco 7125	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))
16	9	fmpttd 7110	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁))
17		ioossicc 13466	. . . . . . . . . . . . . . 15 ⊢ (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁)
18		itgsubst.z	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑍 ∈ ℝ^*)
19		itgsubst.w	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑊 ∈ ℝ^*)
20		itgsubst.m	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑀 ∈ (𝑍(,)𝑊))
21		eliooord 13438	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ∈ (𝑍(,)𝑊) → (𝑍 < 𝑀 ∧ 𝑀 < 𝑊))
22	20, 21	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑍 < 𝑀 ∧ 𝑀 < 𝑊))
23	22	simpld 499	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑍 < 𝑀)
24		itgsubst.n	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ (𝑍(,)𝑊))
25		eliooord 13438	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ (𝑍(,)𝑊) → (𝑍 < 𝑁 ∧ 𝑁 < 𝑊))
26	24, 25	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑍 < 𝑁 ∧ 𝑁 < 𝑊))
27	26	simprd 500	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 < 𝑊)
28		iccssioo 13448	. . . . . . . . . . . . . . . 16 ⊢ (((𝑍 ∈ ℝ^* ∧ 𝑊 ∈ ℝ^*) ∧ (𝑍 < 𝑀 ∧ 𝑁 < 𝑊)) → (𝑀[,]𝑁) ⊆ (𝑍(,)𝑊))
29	18, 19, 23, 27, 28	syl22anc 851	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀[,]𝑁) ⊆ (𝑍(,)𝑊))
30	17, 29	sstrid 3947	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀(,)𝑁) ⊆ (𝑍(,)𝑊))
31		ioossre 13440	. . . . . . . . . . . . . . . 16 ⊢ (𝑍(,)𝑊) ⊆ ℝ
32	31	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑍(,)𝑊) ⊆ ℝ)
33	32, 5	sstrdi 3948	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑍(,)𝑊) ⊆ ℂ)
34	30, 33	sstrd 3946	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑀(,)𝑁) ⊆ ℂ)
35		itgsubst.a	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊)))
36		cncfcdm 25068	. . . . . . . . . . . . 13 ⊢ (((𝑀(,)𝑁) ⊆ ℂ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊))) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑀(,)𝑁)) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁)))
37	34, 35, 36	syl2anc 595	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑀(,)𝑁)) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁)))
38	16, 37	mpbird 260	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑀(,)𝑁)))
39	17	sseli 3932	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ (𝑀(,)𝑁) → 𝑣 ∈ (𝑀[,]𝑁))
40	31, 24	sselid 3934	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑁 ∈ ℝ)
41	40	rexrd 11265	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 ∈ ℝ^*)
42	41	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → 𝑁 ∈ ℝ^*)
43	31, 20	sselid 3934	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑀 ∈ ℝ)
44		elicc2 13444	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑣 ∈ (𝑀[,]𝑁) ↔ (𝑣 ∈ ℝ ∧ 𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁)))
45	43, 40, 44	syl2anc 595	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑣 ∈ (𝑀[,]𝑁) ↔ (𝑣 ∈ ℝ ∧ 𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁)))
46	45	biimpa 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑣 ∈ ℝ ∧ 𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁))
47	46	simp3d 1161	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → 𝑣 ≤ 𝑁)
48		iooss2 13414	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℝ^* ∧ 𝑣 ≤ 𝑁) → (𝑀(,)𝑣) ⊆ (𝑀(,)𝑁))
49	42, 47, 48	syl2anc 595	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑀(,)𝑣) ⊆ (𝑀(,)𝑁))
50	49	sselda 3936	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑣)) → 𝑢 ∈ (𝑀(,)𝑁))
51	30	sselda 3936	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀(,)𝑁)) → 𝑢 ∈ (𝑍(,)𝑊))
52		itgsubst.c	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ))
53		cncff 25063	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ) → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶):(𝑍(,)𝑊)⟶ℂ)
54	52, 53	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶):(𝑍(,)𝑊)⟶ℂ)
55	54	fvmptelcdm 7108	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝑍(,)𝑊)) → 𝐶 ∈ ℂ)
56	51, 55	syldan 602	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀(,)𝑁)) → 𝐶 ∈ ℂ)
57	56	adantlr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑁)) → 𝐶 ∈ ℂ)
58	50, 57	syldan 602	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑣)) → 𝐶 ∈ ℂ)
59		ioombl 25735	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀(,)𝑣) ∈ dom vol
60	59	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑀(,)𝑣) ∈ dom vol)
61	17	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁))
62		ioombl 25735	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀(,)𝑁) ∈ dom vol
63	62	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑀(,)𝑁) ∈ dom vol)
64	29	sselda 3936	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀[,]𝑁)) → 𝑢 ∈ (𝑍(,)𝑊))
65	64, 55	syldan 602	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀[,]𝑁)) → 𝐶 ∈ ℂ)
66	29	resmptd 6041	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ↾ (𝑀[,]𝑁)) = (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶))
67		rescncf 25067	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀[,]𝑁) ⊆ (𝑍(,)𝑊) → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ) → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℂ)))
68	29, 52, 67	sylc 66	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℂ))
69	66, 68	eqeltrrd 2863	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℂ))
70		cniccibl 26011	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℂ)) → (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ 𝐿¹)
71	43, 40, 69, 70	syl3anc 1397	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ 𝐿¹)
72	61, 63, 65, 71	iblss 25975	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) ∈ 𝐿¹)
73	72	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) ∈ 𝐿¹)
74	49, 60, 57, 73	iblss 25975	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑢 ∈ (𝑀(,)𝑣) ↦ 𝐶) ∈ 𝐿¹)
75	58, 74	itgcl 25954	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → ∫(𝑀(,)𝑣)𝐶 d𝑢 ∈ ℂ)
76	39, 75	sylan2 604	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀(,)𝑁)) → ∫(𝑀(,)𝑣)𝐶 d𝑢 ∈ ℂ)
77	76	fmpttd 7110	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢):(𝑀(,)𝑁)⟶ℂ)
78	30, 31	sstrdi 3948	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀(,)𝑁) ⊆ ℝ)
79		fveq2 6881	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑢 → ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) = ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢))
80		nffvmpt1 6892	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑢((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡)
81		nfcv 2924	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢)
82	79, 80, 81	cbvitg 25946	. . . . . . . . . . . . . . . . . 18 ⊢ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡 = ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) d𝑢
83		eqid 2762	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)
84	83	fvmpt2 7001	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑢 ∈ (𝑀(,)𝑁) ∧ 𝐶 ∈ ℂ) → ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) = 𝐶)
85	50, 58, 84	syl2anc 595	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑣)) → ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) = 𝐶)
86	85	itgeq2dv 25952	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) d𝑢 = ∫(𝑀(,)𝑣)𝐶 d𝑢)
87	82, 86	eqtrid 2809	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡 = ∫(𝑀(,)𝑣)𝐶 d𝑢)
88	87	mpteq2dva 5203	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡) = (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢))
89	88	oveq2d 7428	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡)) = (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)))
90		eqid 2762	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡) = (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡)
91	3	rexrd 11265	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑋 ∈ ℝ^*)
92	4	rexrd 11265	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑌 ∈ ℝ^*)
93		lbicc2 13497	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑋 ∈ ℝ^* ∧ 𝑌 ∈ ℝ^* ∧ 𝑋 ≤ 𝑌) → 𝑋 ∈ (𝑋[,]𝑌))
94	91, 92, 1, 93	syl3anc 1397	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑋 ∈ (𝑋[,]𝑌))
95		n0i 4292	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑋 ∈ (𝑋[,]𝑌) → ¬ (𝑋[,]𝑌) = ∅)
96	94, 95	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ¬ (𝑋[,]𝑌) = ∅)
97		feq3 6685	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀(,)𝑁) = ∅ → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅))
98	16, 97	syl5ibcom 248	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑀(,)𝑁) = ∅ → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅))
99		f00 6760	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅ ↔ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) = ∅ ∧ (𝑋[,]𝑌) = ∅))
100	99	simprbi 502	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅ → (𝑋[,]𝑌) = ∅)
101	98, 100	syl6 36	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑀(,)𝑁) = ∅ → (𝑋[,]𝑌) = ∅))
102	96, 101	mtod 201	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ¬ (𝑀(,)𝑁) = ∅)
103	43	rexrd 11265	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ ℝ^*)
104		ioo0 13403	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ ℝ^* ∧ 𝑁 ∈ ℝ^*) → ((𝑀(,)𝑁) = ∅ ↔ 𝑁 ≤ 𝑀))
105	103, 41, 104	syl2anc 595	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑀(,)𝑁) = ∅ ↔ 𝑁 ≤ 𝑀))
106	102, 105	mtbid 327	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ¬ 𝑁 ≤ 𝑀)
107	40, 43	letrid 11368	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑁 ≤ 𝑀 ∨ 𝑀 ≤ 𝑁))
108	107	ord 877	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (¬ 𝑁 ≤ 𝑀 → 𝑀 ≤ 𝑁))
109	106, 108	mpd 16	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ≤ 𝑁)
110		resmpt 6038	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶))
111	17, 110	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)
112		rescncf 25067	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℂ) → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) ∈ ((𝑀(,)𝑁)–cn→ℂ)))
113	17, 69, 112	mpsyl 69	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) ∈ ((𝑀(,)𝑁)–cn→ℂ))
114	111, 113	eqeltrrid 2867	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) ∈ ((𝑀(,)𝑁)–cn→ℂ))
115	90, 43, 40, 109, 114, 72	ftc1cn 26213	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶))
116	29, 31	sstrdi 3948	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑀[,]𝑁) ⊆ ℝ)
117		tgioo4 24973	. . . . . . . . . . . . . . . 16 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
118		eqid 2762	. . . . . . . . . . . . . . . 16 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
119		iccntr 24990	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝑀[,]𝑁)) = (𝑀(,)𝑁))
120	43, 40, 119	syl2anc 595	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘(𝑀[,]𝑁)) = (𝑀(,)𝑁))
121	6, 116, 75, 117, 118, 120	dvmptntr 26141	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)))
122	89, 115, 121	3eqtr3rd 2806	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶))
123	122	dmeqd 5894	. . . . . . . . . . . . 13 ⊢ (𝜑 → dom (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = dom (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶))
124	83, 56	dmmptd 6680	. . . . . . . . . . . . 13 ⊢ (𝜑 → dom (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) = (𝑀(,)𝑁))
125	123, 124	eqtrd 2797	. . . . . . . . . . . 12 ⊢ (𝜑 → dom (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑀(,)𝑁))
126		dvcn 26091	. . . . . . . . . . . 12 ⊢ (((ℝ ⊆ ℂ ∧ (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢):(𝑀(,)𝑁)⟶ℂ ∧ (𝑀(,)𝑁) ⊆ ℝ) ∧ dom (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑀(,)𝑁)) → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∈ ((𝑀(,)𝑁)–cn→ℂ))
127	6, 77, 78, 125, 126	syl31anc 1399	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∈ ((𝑀(,)𝑁)–cn→ℂ))
128	38, 127	cncfco 25077	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) ∈ ((𝑋[,]𝑌)–cn→ℂ))
129	15, 128	eqeltrrd 2863	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢) ∈ ((𝑋[,]𝑌)–cn→ℂ))
130		cncff 25063	. . . . . . . . 9 ⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢) ∈ ((𝑋[,]𝑌)–cn→ℂ) → (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢):(𝑋[,]𝑌)⟶ℂ)
131	129, 130	syl 18	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢):(𝑋[,]𝑌)⟶ℂ)
132	131	fvmptelcdm 7108	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → ∫(𝑀(,)𝐴)𝐶 d𝑢 ∈ ℂ)
133		iccntr 24990	. . . . . . . 8 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝑋[,]𝑌)) = (𝑋(,)𝑌))
134	3, 4, 133	syl2anc 595	. . . . . . 7 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘(𝑋[,]𝑌)) = (𝑋(,)𝑌))
135	6, 8, 132, 117, 118, 134	dvmptntr 26141	. . . . . 6 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)))
136		reelprrecn 11198	. . . . . . . 8 ⊢ ℝ ∈ {ℝ, ℂ}
137	136	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
138		ioossicc 13466	. . . . . . . . 9 ⊢ (𝑋(,)𝑌) ⊆ (𝑋[,]𝑌)
139	138	sseli 3932	. . . . . . . 8 ⊢ (𝑥 ∈ (𝑋(,)𝑌) → 𝑥 ∈ (𝑋[,]𝑌))
140	139, 9	sylan2 604	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐴 ∈ (𝑀(,)𝑁))
141		itgsubst.b	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ (((𝑋(,)𝑌)–cn→ℂ) ∩ 𝐿¹))
142		elin 3920	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ (((𝑋(,)𝑌)–cn→ℂ) ∩ 𝐿¹) ↔ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ) ∧ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿¹))
143	141, 142	sylib 221	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ) ∧ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿¹))
144	143	simpld 499	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ))
145		cncff 25063	. . . . . . . . 9 ⊢ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ) → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵):(𝑋(,)𝑌)⟶ℂ)
146	144, 145	syl 18	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵):(𝑋(,)𝑌)⟶ℂ)
147	146	fvmptelcdm 7108	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐵 ∈ ℂ)
148	56	fmpttd 7110	. . . . . . . . 9 ⊢ (𝜑 → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶):(𝑀(,)𝑁)⟶ℂ)
149		nfcv 2924	. . . . . . . . . . 11 ⊢ Ⅎ𝑣𝐶
150		nfcsb1v 3876	. . . . . . . . . . 11 ⊢ Ⅎ𝑢⦋𝑣 / 𝑢⦌𝐶
151		csbeq1a 3866	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑣 → 𝐶 = ⦋𝑣 / 𝑢⦌𝐶)
152	149, 150, 151	cbvmpt 5212	. . . . . . . . . 10 ⊢ (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) = (𝑣 ∈ (𝑀(,)𝑁) ↦ ⦋𝑣 / 𝑢⦌𝐶)
153	152	fmpt 7105	. . . . . . . . 9 ⊢ (∀𝑣 ∈ (𝑀(,)𝑁)⦋𝑣 / 𝑢⦌𝐶 ∈ ℂ ↔ (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶):(𝑀(,)𝑁)⟶ℂ)
154	148, 153	sylibr 237	. . . . . . . 8 ⊢ (𝜑 → ∀𝑣 ∈ (𝑀(,)𝑁)⦋𝑣 / 𝑢⦌𝐶 ∈ ℂ)
155	154	r19.21bi 3256	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀(,)𝑁)) → ⦋𝑣 / 𝑢⦌𝐶 ∈ ℂ)
156	31, 5	sstri 3945	. . . . . . . . . 10 ⊢ (𝑍(,)𝑊) ⊆ ℂ
157		cncff 25063	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊)) → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑍(,)𝑊))
158	35, 157	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑍(,)𝑊))
159	158	fvmptelcdm 7108	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑍(,)𝑊))
160	156, 159	sselid 3934	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ ℂ)
161	6, 8, 160, 117, 118, 134	dvmptntr 26141	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐴)))
162		itgsubst.da	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵))
163	161, 162	eqtr3d 2799	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵))
164	122, 152	eqtrdi 2813	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑣 ∈ (𝑀(,)𝑁) ↦ ⦋𝑣 / 𝑢⦌𝐶))
165		csbeq1 3855	. . . . . . 7 ⊢ (𝑣 = 𝐴 → ⦋𝑣 / 𝑢⦌𝐶 = ⦋𝐴 / 𝑢⦌𝐶)
166	137, 137, 140, 147, 76, 155, 163, 164, 14, 165	dvmptco 26142	. . . . . 6 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (⦋𝐴 / 𝑢⦌𝐶 · 𝐵)))
167		nfcvd 2925	. . . . . . . . . 10 ⊢ (𝐴 ∈ (𝑀(,)𝑁) → Ⅎ𝑢𝐸)
168		itgsubst.e	. . . . . . . . . 10 ⊢ (𝑢 = 𝐴 → 𝐶 = 𝐸)
169	167, 168	csbiegf 3885	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝑀(,)𝑁) → ⦋𝐴 / 𝑢⦌𝐶 = 𝐸)
170	140, 169	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ⦋𝐴 / 𝑢⦌𝐶 = 𝐸)
171	170	oveq1d 7427	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (⦋𝐴 / 𝑢⦌𝐶 · 𝐵) = (𝐸 · 𝐵))
172	171	mpteq2dva 5203	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ (⦋𝐴 / 𝑢⦌𝐶 · 𝐵)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)))
173	135, 166, 172	3eqtrd 2801	. . . . 5 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)))
174		resmpt 6038	. . . . . . . 8 ⊢ ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸))
175	138, 174	ax-mp 5	. . . . . . 7 ⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)
176		eqidd 2763	. . . . . . . . . 10 ⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) = (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶))
177	159, 10, 176, 168	fmptco 7125	. . . . . . . . 9 ⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸))
178	35, 52	cncfco 25077	. . . . . . . . 9 ⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) ∈ ((𝑋[,]𝑌)–cn→ℂ))
179	177, 178	eqeltrrd 2863	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ))
180		rescncf 25067	. . . . . . . 8 ⊢ ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ)))
181	138, 179, 180	mpsyl 69	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
182	175, 181	eqeltrrid 2867	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ ((𝑋(,)𝑌)–cn→ℂ))
183	182, 144	mulcncf 25616	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
184	173, 183	eqeltrd 2862	. . . 4 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
185		ioombl 25735	. . . . . . . 8 ⊢ (𝑋(,)𝑌) ∈ dom vol
186	185	a1i 11	. . . . . . 7 ⊢ (𝜑 → (𝑋(,)𝑌) ∈ dom vol)
187		fco 6730	. . . . . . . . . . 11 ⊢ (((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶):(𝑍(,)𝑊)⟶ℂ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑍(,)𝑊)) → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)):(𝑋[,]𝑌)⟶ℂ)
188	54, 158, 187	syl2anc 595	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)):(𝑋[,]𝑌)⟶ℂ)
189	177	feq1d 6687	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)):(𝑋[,]𝑌)⟶ℂ ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸):(𝑋[,]𝑌)⟶ℂ))
190	188, 189	mpbid 235	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸):(𝑋[,]𝑌)⟶ℂ)
191	190	fvmptelcdm 7108	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐸 ∈ ℂ)
192	139, 191	sylan2 604	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐸 ∈ ℂ)
193		eqidd 2763	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸))
194		eqidd 2763	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵))
195	186, 192, 147, 193, 194	offval2 7696	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘_f · (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)))
196	173, 195	eqtr4d 2800	. . . . 5 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘_f · (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)))
197	138	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (𝑋(,)𝑌) ⊆ (𝑋[,]𝑌))
198		cniccibl 26011	. . . . . . . . 9 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ)) → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ 𝐿¹)
199	3, 4, 179, 198	syl3anc 1397	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ 𝐿¹)
200	197, 186, 191, 199	iblss 25975	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ 𝐿¹)
201		iblmbf 25937	. . . . . . 7 ⊢ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ 𝐿¹ → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ MblFn)
202	200, 201	syl 18	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ MblFn)
203	143	simprd 500	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿¹)
204		cniccbdd 25631	. . . . . . . 8 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ)) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)
205	3, 4, 179, 204	syl3anc 1397	. . . . . . 7 ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)
206		ssralv 4005	. . . . . . . . . 10 ⊢ ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → (∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
207	138, 206	ax-mp 5	. . . . . . . . 9 ⊢ (∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)
208		eqid 2762	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)
209	208, 192	dmmptd 6680	. . . . . . . . . . 11 ⊢ (𝜑 → dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) = (𝑋(,)𝑌))
210	209	raleqdv 3322	. . . . . . . . . 10 ⊢ (𝜑 → (∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
211	175	fveq1i 6882	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌))‘𝑧) = ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)
212		fvres 6900	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (𝑋(,)𝑌) → (((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌))‘𝑧) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧))
213	211, 212	eqtr3id 2811	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝑋(,)𝑌) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧))
214	213	fveq2d 6885	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (𝑋(,)𝑌) → (abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) = (abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)))
215	214	breq1d 5118	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (𝑋(,)𝑌) → ((abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ (abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
216	215	ralbiia 3108	. . . . . . . . . 10 ⊢ (∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)
217	210, 216	bitr2di 291	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
218	207, 217	imbitrid 247	. . . . . . . 8 ⊢ (𝜑 → (∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
219	218	reximdv 3179	. . . . . . 7 ⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
220	205, 219	mpd 16	. . . . . 6 ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)
221		bddmulibl 26009	. . . . . 6 ⊢ (((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ MblFn ∧ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿¹ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘_f · (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) ∈ 𝐿¹)
222	202, 203, 220, 221	syl3anc 1397	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘_f · (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) ∈ 𝐿¹)
223	196, 222	eqeltrd 2862	. . . 4 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) ∈ 𝐿¹)
224	3, 4, 1, 184, 223, 129	ftc2 26214	. . 3 ⊢ (𝜑 → ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) d𝑡 = (((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) − ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋)))
225		fveq2 6881	. . . . 5 ⊢ (𝑡 = 𝑥 → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) = ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥))
226		nfcv 2924	. . . . . . 7 ⊢ Ⅎ𝑥ℝ
227		nfcv 2924	. . . . . . 7 ⊢ Ⅎ𝑥 D
228		nfmpt1 5209	. . . . . . 7 ⊢ Ⅎ𝑥(𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)
229	226, 227, 228	nfov 7442	. . . . . 6 ⊢ Ⅎ𝑥(ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))
230		nfcv 2924	. . . . . 6 ⊢ Ⅎ𝑥𝑡
231	229, 230	nffv 6891	. . . . 5 ⊢ Ⅎ𝑥((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡)
232		nfcv 2924	. . . . 5 ⊢ Ⅎ𝑡((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥)
233	225, 231, 232	cbvitg 25946	. . . 4 ⊢ ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) d𝑡 = ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) d𝑥
234	173	fveq1d 6883	. . . . . 6 ⊢ (𝜑 → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) = ((𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))‘𝑥))
235		ovex 7445	. . . . . . 7 ⊢ (𝐸 · 𝐵) ∈ V
236		eqid 2762	. . . . . . . 8 ⊢ (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))
237	236	fvmpt2 7001	. . . . . . 7 ⊢ ((𝑥 ∈ (𝑋(,)𝑌) ∧ (𝐸 · 𝐵) ∈ V) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))‘𝑥) = (𝐸 · 𝐵))
238	235, 237	mpan2 703	. . . . . 6 ⊢ (𝑥 ∈ (𝑋(,)𝑌) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))‘𝑥) = (𝐸 · 𝐵))
239	234, 238	sylan9eq 2817	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) = (𝐸 · 𝐵))
240	239	itgeq2dv 25952	. . . 4 ⊢ (𝜑 → ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) d𝑥 = ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥)
241	233, 240	eqtrid 2809	. . 3 ⊢ (𝜑 → ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) d𝑡 = ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥)
242	17, 9	sselid 3934	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑀[,]𝑁))
243		elicc2 13444	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝐴 ∈ (𝑀[,]𝑁) ↔ (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁)))
244	43, 40, 243	syl2anc 595	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 ∈ (𝑀[,]𝑁) ↔ (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁)))
245	244	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → (𝐴 ∈ (𝑀[,]𝑁) ↔ (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁)))
246	242, 245	mpbid 235	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁))
247	246	simp2d 1160	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝑀 ≤ 𝐴)
248	247	ditgpos 26026	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ∫(𝑀(,)𝐴)𝐶 d𝑢)
249	248	mpteq2dva 5203	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢) = (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))
250	249	fveq1d 6883	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑌) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌))
251		ubicc2 13498	. . . . . . . 8 ⊢ ((𝑋 ∈ ℝ^* ∧ 𝑌 ∈ ℝ^* ∧ 𝑋 ≤ 𝑌) → 𝑌 ∈ (𝑋[,]𝑌))
252	91, 92, 1, 251	syl3anc 1397	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ (𝑋[,]𝑌))
253		itgsubst.l	. . . . . . . . 9 ⊢ (𝑥 = 𝑌 → 𝐴 = 𝐿)
254		ditgeq2 26019	. . . . . . . . 9 ⊢ (𝐴 = 𝐿 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐿]𝐶 d𝑢)
255	253, 254	syl 18	. . . . . . . 8 ⊢ (𝑥 = 𝑌 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐿]𝐶 d𝑢)
256		eqid 2762	. . . . . . . 8 ⊢ (𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢) = (𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)
257		ditgex 26022	. . . . . . . 8 ⊢ ⨜[𝑀 → 𝐿]𝐶 d𝑢 ∈ V
258	255, 256, 257	fvmpt 6989	. . . . . . 7 ⊢ (𝑌 ∈ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑌) = ⨜[𝑀 → 𝐿]𝐶 d𝑢)
259	252, 258	syl 18	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑌) = ⨜[𝑀 → 𝐿]𝐶 d𝑢)
260	250, 259	eqtr3d 2799	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) = ⨜[𝑀 → 𝐿]𝐶 d𝑢)
261	249	fveq1d 6883	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑋) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋))
262		itgsubst.k	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → 𝐴 = 𝐾)
263		ditgeq2 26019	. . . . . . . . 9 ⊢ (𝐴 = 𝐾 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐾]𝐶 d𝑢)
264	262, 263	syl 18	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐾]𝐶 d𝑢)
265		ditgex 26022	. . . . . . . 8 ⊢ ⨜[𝑀 → 𝐾]𝐶 d𝑢 ∈ V
266	264, 256, 265	fvmpt 6989	. . . . . . 7 ⊢ (𝑋 ∈ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑋) = ⨜[𝑀 → 𝐾]𝐶 d𝑢)
267	94, 266	syl 18	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑋) = ⨜[𝑀 → 𝐾]𝐶 d𝑢)
268	261, 267	eqtr3d 2799	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋) = ⨜[𝑀 → 𝐾]𝐶 d𝑢)
269	260, 268	oveq12d 7430	. . . 4 ⊢ (𝜑 → (((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) − ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋)) = (⨜[𝑀 → 𝐿]𝐶 d𝑢 − ⨜[𝑀 → 𝐾]𝐶 d𝑢))
270		lbicc2 13497	. . . . . . 7 ⊢ ((𝑀 ∈ ℝ^* ∧ 𝑁 ∈ ℝ^* ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ (𝑀[,]𝑁))
271	103, 41, 109, 270	syl3anc 1397	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ (𝑀[,]𝑁))
272	262	eleq1d 2847	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (𝐴 ∈ (𝑀[,]𝑁) ↔ 𝐾 ∈ (𝑀[,]𝑁)))
273	242	ralrimiva 3156	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ (𝑋[,]𝑌)𝐴 ∈ (𝑀[,]𝑁))
274	272, 273, 94	rspcdva 3581	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ (𝑀[,]𝑁))
275	253	eleq1d 2847	. . . . . . 7 ⊢ (𝑥 = 𝑌 → (𝐴 ∈ (𝑀[,]𝑁) ↔ 𝐿 ∈ (𝑀[,]𝑁)))
276	275, 273, 252	rspcdva 3581	. . . . . 6 ⊢ (𝜑 → 𝐿 ∈ (𝑀[,]𝑁))
277	43, 40, 271, 274, 276, 56, 72	ditgsplit 26031	. . . . 5 ⊢ (𝜑 → ⨜[𝑀 → 𝐿]𝐶 d𝑢 = (⨜[𝑀 → 𝐾]𝐶 d𝑢 + ⨜[𝐾 → 𝐿]𝐶 d𝑢))
278	277	oveq1d 7427	. . . 4 ⊢ (𝜑 → (⨜[𝑀 → 𝐿]𝐶 d𝑢 − ⨜[𝑀 → 𝐾]𝐶 d𝑢) = ((⨜[𝑀 → 𝐾]𝐶 d𝑢 + ⨜[𝐾 → 𝐿]𝐶 d𝑢) − ⨜[𝑀 → 𝐾]𝐶 d𝑢))
279	43, 40, 271, 274, 56, 72	ditgcl 26028	. . . . 5 ⊢ (𝜑 → ⨜[𝑀 → 𝐾]𝐶 d𝑢 ∈ ℂ)
280	43, 40, 274, 276, 56, 72	ditgcl 26028	. . . . 5 ⊢ (𝜑 → ⨜[𝐾 → 𝐿]𝐶 d𝑢 ∈ ℂ)
281	279, 280	pncan2d 11577	. . . 4 ⊢ (𝜑 → ((⨜[𝑀 → 𝐾]𝐶 d𝑢 + ⨜[𝐾 → 𝐿]𝐶 d𝑢) − ⨜[𝑀 → 𝐾]𝐶 d𝑢) = ⨜[𝐾 → 𝐿]𝐶 d𝑢)
282	269, 278, 281	3eqtrd 2801	. . 3 ⊢ (𝜑 → (((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) − ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋)) = ⨜[𝐾 → 𝐿]𝐶 d𝑢)
283	224, 241, 282	3eqtr3d 2805	. 2 ⊢ (𝜑 → ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥 = ⨜[𝐾 → 𝐿]𝐶 d𝑢)
284	2, 283	eqtr2d 2798	1 ⊢ (𝜑 → ⨜[𝐾 → 𝐿]𝐶 d𝑢 = ⨜[𝑋 → 𝑌](𝐸 · 𝐵) d𝑥)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1102 = wceq 1569 ∈ wcel 2142 ∀wral 3078 ∃wrex 3088 Vcvv 3454 ⦋csb 3852 ∩ cin 3903 ⊆ wss 3904 ∅c0 4285 {cpr 4590 class class class wbr 5108 ↦ cmpt 5191 dom cdm 5660 ran crn 5661 ↾ cres 5662 ∘ ccom 5664 ⟶wf 6532 ‘cfv 6536 (class class class)co 7412 ∘_f cof 7674 ℂcc 11104 ℝcr 11105 + caddc 11109 · cmul 11111 ℝ^*cxr 11248 < clt 11249 ≤ cle 11250 − cmin 11447 (,)cioo 13378 [,]cicc 13381 abscabs 15292 TopOpenctopn 17480 topGenctg 17496 ℂ_fldccnfld 21533 intcnt 23185 –cn→ccncf 25046 volcvol 25633 MblFncmbf 25784 𝐿¹cibl 25787 ∫citg 25788 ⨜cdit 26016 D cdv 26033

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1824 ax-4 1838 ax-5 1939 ax-6 1996 ax-7 2037 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5335 ax-pr 5403 ax-un 7734 ax-inf2 9608 ax-cc 10425 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183 ax-pre-sup 11184 ax-addf 11185

This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1103 df-3an 1104 df-tru 1572 df-fal 1582 df-ex 1809 df-nf 1813 df-sb 2096 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3368 df-reu 3369 df-rab 3416 df-v 3456 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-symdif 4205 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4595 df-uni 4872 df-int 4912 df-iun 4957 df-iin 4958 df-disj 5076 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5555 df-eprel 5560 df-po 5568 df-so 5569 df-fr 5613 df-se 5614 df-we 5615 df-xp 5666 df-rel 5667 df-cnv 5668 df-co 5669 df-dm 5670 df-rn 5671 df-res 5672 df-ima 5673 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-of 7676 df-ofr 7677 df-om 7861 df-1st 7984 df-2nd 7985 df-supp 8155 df-frecs 8276 df-wrecs 8307 df-recs 8356 df-rdg 8395 df-1o 8451 df-2o 8452 df-oadd 8455 df-omul 8456 df-er 8692 df-map 8824 df-pm 8825 df-ixp 8894 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-fsupp 9320 df-fi 9369 df-sup 9400 df-inf 9401 df-oi 9470 df-dju 9894 df-card 9932 df-acn 9935 df-pnf 11251 df-mnf 11252 df-xr 11253 df-ltxr 11254 df-le 11255 df-sub 11449 df-neg 11450 df-div 11878 df-nn 12240 df-2 12309 df-3 12310 df-4 12311 df-5 12312 df-6 12313 df-7 12314 df-8 12315 df-9 12316 df-n0 12511 df-z 12598 df-dec 12718 df-uz 12869 df-q 12979 df-rp 13023 df-xneg 13143 df-xadd 13144 df-xmul 13145 df-ioo 13382 df-ioc 13383 df-ico 13384 df-icc 13385 df-fz 13542 df-fzo 13690 df-fl 13832 df-mod 13910 df-seq 14045 df-exp 14105 df-hash 14374 df-cj 15157 df-re 15158 df-im 15159 df-sqrt 15293 df-abs 15294 df-limsup 15529 df-clim 15546 df-rlim 15547 df-sum 15745 df-struct 17213 df-sets 17230 df-slot 17248 df-ndx 17260 df-base 17276 df-ress 17297 df-plusg 17329 df-mulr 17330 df-starv 17331 df-sca 17332 df-vsca 17333 df-ip 17334 df-tset 17335 df-ple 17336 df-ds 17338 df-unif 17339 df-hom 17340 df-cco 17341 df-rest 17481 df-topn 17482 df-0g 17500 df-gsum 17501 df-topgen 17502 df-pt 17503 df-prds 17506 df-xrs 17562 df-qtop 17567 df-imas 17568 df-xps 17570 df-mre 17644 df-mrc 17645 df-acs 17647 df-mgm 18704 df-sgrp 18783 df-mnd 18799 df-submnd 18848 df-mulg 19140 df-cntz 19393 df-cmn 19858 df-psmet 21525 df-xmet 21526 df-met 21527 df-bl 21528 df-mopn 21529 df-fbas 21530 df-fg 21531 df-cnfld 21534 df-top 23062 df-topon 23079 df-topsp 23101 df-bases 23114 df-cld 23187 df-ntr 23188 df-cls 23189 df-nei 23266 df-lp 23304 df-perf 23305 df-cn 23395 df-cnp 23396 df-haus 23483 df-cmp 23555 df-tx 23730 df-hmeo 23923 df-fil 24014 df-fm 24106 df-flim 24107 df-flf 24108 df-xms 24488 df-ms 24489 df-tms 24490 df-cncf 25048 df-ovol 25634 df-vol 25635 df-mbf 25789 df-itg1 25790 df-itg2 25791 df-ibl 25792 df-itg 25793 df-0p 25840 df-ditg 26017 df-limc 26036 df-dv 26037

This theorem is used by: itgsubst 26219

W3C validator