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 24631

Description: Lemma for itgsubst 24632. (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 24439	. 2 ⊢ (𝜑 → ⨜[𝑋 → 𝑌](𝐸 · 𝐵) d𝑥 = ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥)
3		itgsubst.x	. . . 4 ⊢ (𝜑 → 𝑋 ∈ ℝ)
4		itgsubst.y	. . . 4 ⊢ (𝜑 → 𝑌 ∈ ℝ)
5		ax-resscn 10580	. . . . . . . 8 ⊢ ℝ ⊆ ℂ
6	5	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℝ ⊆ ℂ)
7		iccssre 12805	. . . . . . . 8 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑋[,]𝑌) ⊆ ℝ)
8	3, 4, 7	syl2anc 586	. . . . . . 7 ⊢ (𝜑 → (𝑋[,]𝑌) ⊆ ℝ)
9		itgsubst.cl2	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑀(,)𝑁))
10		eqidd 2822	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) = (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴))
11		eqidd 2822	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) = (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢))
12		oveq2 7150	. . . . . . . . . . . 12 ⊢ (𝑣 = 𝐴 → (𝑀(,)𝑣) = (𝑀(,)𝐴))
13		itgeq1 24356	. . . . . . . . . . . 12 ⊢ ((𝑀(,)𝑣) = (𝑀(,)𝐴) → ∫(𝑀(,)𝑣)𝐶 d𝑢 = ∫(𝑀(,)𝐴)𝐶 d𝑢)
14	12, 13	syl 17	. . . . . . . . . . 11 ⊢ (𝑣 = 𝐴 → ∫(𝑀(,)𝑣)𝐶 d𝑢 = ∫(𝑀(,)𝐴)𝐶 d𝑢)
15	9, 10, 11, 14	fmptco 6877	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))
16	9	fmpttd 6865	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁))
17		ioossicc 12809	. . . . . . . . . . . . . . 15 ⊢ (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁)
18		itgsubst.z	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑍 ∈ ℝ^*)
19		itgsubst.w	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑊 ∈ ℝ^*)
20		itgsubst.m	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑀 ∈ (𝑍(,)𝑊))
21		eliooord 12783	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ∈ (𝑍(,)𝑊) → (𝑍 < 𝑀 ∧ 𝑀 < 𝑊))
22	20, 21	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑍 < 𝑀 ∧ 𝑀 < 𝑊))
23	22	simpld 497	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑍 < 𝑀)
24		itgsubst.n	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ (𝑍(,)𝑊))
25		eliooord 12783	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ (𝑍(,)𝑊) → (𝑍 < 𝑁 ∧ 𝑁 < 𝑊))
26	24, 25	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑍 < 𝑁 ∧ 𝑁 < 𝑊))
27	26	simprd 498	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 < 𝑊)
28		iccssioo 12792	. . . . . . . . . . . . . . . 16 ⊢ (((𝑍 ∈ ℝ^* ∧ 𝑊 ∈ ℝ^*) ∧ (𝑍 < 𝑀 ∧ 𝑁 < 𝑊)) → (𝑀[,]𝑁) ⊆ (𝑍(,)𝑊))
29	18, 19, 23, 27, 28	syl22anc 836	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀[,]𝑁) ⊆ (𝑍(,)𝑊))
30	17, 29	sstrid 3966	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀(,)𝑁) ⊆ (𝑍(,)𝑊))
31		ioossre 12785	. . . . . . . . . . . . . . . 16 ⊢ (𝑍(,)𝑊) ⊆ ℝ
32	31	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑍(,)𝑊) ⊆ ℝ)
33	32, 5	sstrdi 3967	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑍(,)𝑊) ⊆ ℂ)
34	30, 33	sstrd 3965	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑀(,)𝑁) ⊆ ℂ)
35		itgsubst.a	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊)))
36		cncffvrn 23489	. . . . . . . . . . . . 13 ⊢ (((𝑀(,)𝑁) ⊆ ℂ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊))) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑀(,)𝑁)) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁)))
37	34, 35, 36	syl2anc 586	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑀(,)𝑁)) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁)))
38	16, 37	mpbird 259	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑀(,)𝑁)))
39	17	sseli 3951	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ (𝑀(,)𝑁) → 𝑣 ∈ (𝑀[,]𝑁))
40	31, 24	sseldi 3953	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑁 ∈ ℝ)
41	40	rexrd 10677	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 ∈ ℝ^*)
42	41	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → 𝑁 ∈ ℝ^*)
43	31, 20	sseldi 3953	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑀 ∈ ℝ)
44		elicc2 12788	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑣 ∈ (𝑀[,]𝑁) ↔ (𝑣 ∈ ℝ ∧ 𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁)))
45	43, 40, 44	syl2anc 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑣 ∈ (𝑀[,]𝑁) ↔ (𝑣 ∈ ℝ ∧ 𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁)))
46	45	biimpa 479	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑣 ∈ ℝ ∧ 𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁))
47	46	simp3d 1140	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → 𝑣 ≤ 𝑁)
48		iooss2 12761	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℝ^* ∧ 𝑣 ≤ 𝑁) → (𝑀(,)𝑣) ⊆ (𝑀(,)𝑁))
49	42, 47, 48	syl2anc 586	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑀(,)𝑣) ⊆ (𝑀(,)𝑁))
50	49	sselda 3955	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑣)) → 𝑢 ∈ (𝑀(,)𝑁))
51	30	sselda 3955	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀(,)𝑁)) → 𝑢 ∈ (𝑍(,)𝑊))
52		itgsubst.c	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ))
53		cncff 23484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ) → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶):(𝑍(,)𝑊)⟶ℂ)
54	52, 53	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶):(𝑍(,)𝑊)⟶ℂ)
55	54	fvmptelrn 6863	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝑍(,)𝑊)) → 𝐶 ∈ ℂ)
56	51, 55	syldan 593	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀(,)𝑁)) → 𝐶 ∈ ℂ)
57	56	adantlr 713	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑁)) → 𝐶 ∈ ℂ)
58	50, 57	syldan 593	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑣)) → 𝐶 ∈ ℂ)
59		ioombl 24149	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀(,)𝑣) ∈ dom vol
60	59	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑀(,)𝑣) ∈ dom vol)
61	17	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁))
62		ioombl 24149	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀(,)𝑁) ∈ dom vol
63	62	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑀(,)𝑁) ∈ dom vol)
64	29	sselda 3955	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀[,]𝑁)) → 𝑢 ∈ (𝑍(,)𝑊))
65	64, 55	syldan 593	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀[,]𝑁)) → 𝐶 ∈ ℂ)
66	29	resmptd 5894	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ↾ (𝑀[,]𝑁)) = (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶))
67		rescncf 23488	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀[,]𝑁) ⊆ (𝑍(,)𝑊) → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ) → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℂ)))
68	29, 52, 67	sylc 65	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℂ))
69	66, 68	eqeltrrd 2914	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℂ))
70		cniccibl 24424	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℂ)) → (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ 𝐿¹)
71	43, 40, 69, 70	syl3anc 1367	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ 𝐿¹)
72	61, 63, 65, 71	iblss 24388	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) ∈ 𝐿¹)
73	72	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) ∈ 𝐿¹)
74	49, 60, 57, 73	iblss 24388	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑢 ∈ (𝑀(,)𝑣) ↦ 𝐶) ∈ 𝐿¹)
75	58, 74	itgcl 24367	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → ∫(𝑀(,)𝑣)𝐶 d𝑢 ∈ ℂ)
76	39, 75	sylan2 594	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀(,)𝑁)) → ∫(𝑀(,)𝑣)𝐶 d𝑢 ∈ ℂ)
77	76	fmpttd 6865	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢):(𝑀(,)𝑁)⟶ℂ)
78	30, 31	sstrdi 3967	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀(,)𝑁) ⊆ ℝ)
79		fveq2 6656	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑢 → ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) = ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢))
80		nffvmpt1 6667	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑢((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡)
81		nfcv 2977	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢)
82	79, 80, 81	cbvitg 24359	. . . . . . . . . . . . . . . . . 18 ⊢ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡 = ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) d𝑢
83		eqid 2821	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)
84	83	fvmpt2 6765	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑢 ∈ (𝑀(,)𝑁) ∧ 𝐶 ∈ ℂ) → ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) = 𝐶)
85	50, 58, 84	syl2anc 586	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑣)) → ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) = 𝐶)
86	85	itgeq2dv 24365	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) d𝑢 = ∫(𝑀(,)𝑣)𝐶 d𝑢)
87	82, 86	syl5eq 2868	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡 = ∫(𝑀(,)𝑣)𝐶 d𝑢)
88	87	mpteq2dva 5147	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡) = (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢))
89	88	oveq2d 7158	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡)) = (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)))
90		eqid 2821	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡) = (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡)
91	3	rexrd 10677	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑋 ∈ ℝ^*)
92	4	rexrd 10677	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑌 ∈ ℝ^*)
93		lbicc2 12839	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑋 ∈ ℝ^* ∧ 𝑌 ∈ ℝ^* ∧ 𝑋 ≤ 𝑌) → 𝑋 ∈ (𝑋[,]𝑌))
94	91, 92, 1, 93	syl3anc 1367	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑋 ∈ (𝑋[,]𝑌))
95		n0i 4285	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑋 ∈ (𝑋[,]𝑌) → ¬ (𝑋[,]𝑌) = ∅)
96	94, 95	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ¬ (𝑋[,]𝑌) = ∅)
97		feq3 6483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀(,)𝑁) = ∅ → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅))
98	16, 97	syl5ibcom 247	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑀(,)𝑁) = ∅ → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅))
99		f00 6547	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅ ↔ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) = ∅ ∧ (𝑋[,]𝑌) = ∅))
100	99	simprbi 499	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅ → (𝑋[,]𝑌) = ∅)
101	98, 100	syl6 35	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑀(,)𝑁) = ∅ → (𝑋[,]𝑌) = ∅))
102	96, 101	mtod 200	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ¬ (𝑀(,)𝑁) = ∅)
103	43	rexrd 10677	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ ℝ^*)
104		ioo0 12750	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ ℝ^* ∧ 𝑁 ∈ ℝ^*) → ((𝑀(,)𝑁) = ∅ ↔ 𝑁 ≤ 𝑀))
105	103, 41, 104	syl2anc 586	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑀(,)𝑁) = ∅ ↔ 𝑁 ≤ 𝑀))
106	102, 105	mtbid 326	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ¬ 𝑁 ≤ 𝑀)
107	40, 43	letrid 10778	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑁 ≤ 𝑀 ∨ 𝑀 ≤ 𝑁))
108	107	ord 860	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (¬ 𝑁 ≤ 𝑀 → 𝑀 ≤ 𝑁))
109	106, 108	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ≤ 𝑁)
110		resmpt 5891	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶))
111	17, 110	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)
112		rescncf 23488	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℂ) → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) ∈ ((𝑀(,)𝑁)–cn→ℂ)))
113	17, 69, 112	mpsyl 68	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) ∈ ((𝑀(,)𝑁)–cn→ℂ))
114	111, 113	eqeltrrid 2918	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) ∈ ((𝑀(,)𝑁)–cn→ℂ))
115	90, 43, 40, 109, 114, 72	ftc1cn 24625	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶))
116	29, 31	sstrdi 3967	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑀[,]𝑁) ⊆ ℝ)
117		eqid 2821	. . . . . . . . . . . . . . . . 17 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
118	117	tgioo2 23394	. . . . . . . . . . . . . . . 16 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
119		iccntr 23412	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝑀[,]𝑁)) = (𝑀(,)𝑁))
120	43, 40, 119	syl2anc 586	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘(𝑀[,]𝑁)) = (𝑀(,)𝑁))
121	6, 116, 75, 118, 117, 120	dvmptntr 24553	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)))
122	89, 115, 121	3eqtr3rd 2865	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶))
123	122	dmeqd 5760	. . . . . . . . . . . . 13 ⊢ (𝜑 → dom (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = dom (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶))
124	83, 56	dmmptd 6479	. . . . . . . . . . . . 13 ⊢ (𝜑 → dom (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) = (𝑀(,)𝑁))
125	123, 124	eqtrd 2856	. . . . . . . . . . . 12 ⊢ (𝜑 → dom (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑀(,)𝑁))
126		dvcn 24503	. . . . . . . . . . . 12 ⊢ (((ℝ ⊆ ℂ ∧ (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢):(𝑀(,)𝑁)⟶ℂ ∧ (𝑀(,)𝑁) ⊆ ℝ) ∧ dom (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑀(,)𝑁)) → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∈ ((𝑀(,)𝑁)–cn→ℂ))
127	6, 77, 78, 125, 126	syl31anc 1369	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∈ ((𝑀(,)𝑁)–cn→ℂ))
128	38, 127	cncfco 23498	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) ∈ ((𝑋[,]𝑌)–cn→ℂ))
129	15, 128	eqeltrrd 2914	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢) ∈ ((𝑋[,]𝑌)–cn→ℂ))
130		cncff 23484	. . . . . . . . 9 ⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢) ∈ ((𝑋[,]𝑌)–cn→ℂ) → (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢):(𝑋[,]𝑌)⟶ℂ)
131	129, 130	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢):(𝑋[,]𝑌)⟶ℂ)
132	131	fvmptelrn 6863	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → ∫(𝑀(,)𝐴)𝐶 d𝑢 ∈ ℂ)
133		iccntr 23412	. . . . . . . 8 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝑋[,]𝑌)) = (𝑋(,)𝑌))
134	3, 4, 133	syl2anc 586	. . . . . . 7 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘(𝑋[,]𝑌)) = (𝑋(,)𝑌))
135	6, 8, 132, 118, 117, 134	dvmptntr 24553	. . . . . 6 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)))
136		reelprrecn 10615	. . . . . . . 8 ⊢ ℝ ∈ {ℝ, ℂ}
137	136	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
138		ioossicc 12809	. . . . . . . . 9 ⊢ (𝑋(,)𝑌) ⊆ (𝑋[,]𝑌)
139	138	sseli 3951	. . . . . . . 8 ⊢ (𝑥 ∈ (𝑋(,)𝑌) → 𝑥 ∈ (𝑋[,]𝑌))
140	139, 9	sylan2 594	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐴 ∈ (𝑀(,)𝑁))
141		itgsubst.b	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ (((𝑋(,)𝑌)–cn→ℂ) ∩ 𝐿¹))
142		elin 4157	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ (((𝑋(,)𝑌)–cn→ℂ) ∩ 𝐿¹) ↔ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ) ∧ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿¹))
143	141, 142	sylib 220	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ) ∧ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿¹))
144	143	simpld 497	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ))
145		cncff 23484	. . . . . . . . 9 ⊢ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ) → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵):(𝑋(,)𝑌)⟶ℂ)
146	144, 145	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵):(𝑋(,)𝑌)⟶ℂ)
147	146	fvmptelrn 6863	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐵 ∈ ℂ)
148	56	fmpttd 6865	. . . . . . . . 9 ⊢ (𝜑 → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶):(𝑀(,)𝑁)⟶ℂ)
149		nfcv 2977	. . . . . . . . . . 11 ⊢ Ⅎ𝑣𝐶
150		nfcsb1v 3895	. . . . . . . . . . 11 ⊢ Ⅎ𝑢⦋𝑣 / 𝑢⦌𝐶
151		csbeq1a 3885	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑣 → 𝐶 = ⦋𝑣 / 𝑢⦌𝐶)
152	149, 150, 151	cbvmpt 5153	. . . . . . . . . 10 ⊢ (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) = (𝑣 ∈ (𝑀(,)𝑁) ↦ ⦋𝑣 / 𝑢⦌𝐶)
153	152	fmpt 6860	. . . . . . . . 9 ⊢ (∀𝑣 ∈ (𝑀(,)𝑁)⦋𝑣 / 𝑢⦌𝐶 ∈ ℂ ↔ (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶):(𝑀(,)𝑁)⟶ℂ)
154	148, 153	sylibr 236	. . . . . . . 8 ⊢ (𝜑 → ∀𝑣 ∈ (𝑀(,)𝑁)⦋𝑣 / 𝑢⦌𝐶 ∈ ℂ)
155	154	r19.21bi 3208	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀(,)𝑁)) → ⦋𝑣 / 𝑢⦌𝐶 ∈ ℂ)
156	31, 5	sstri 3964	. . . . . . . . . 10 ⊢ (𝑍(,)𝑊) ⊆ ℂ
157		cncff 23484	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊)) → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑍(,)𝑊))
158	35, 157	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑍(,)𝑊))
159	158	fvmptelrn 6863	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑍(,)𝑊))
160	156, 159	sseldi 3953	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ ℂ)
161	6, 8, 160, 118, 117, 134	dvmptntr 24553	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐴)))
162		itgsubst.da	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵))
163	161, 162	eqtr3d 2858	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵))
164	122, 152	syl6eq 2872	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑣 ∈ (𝑀(,)𝑁) ↦ ⦋𝑣 / 𝑢⦌𝐶))
165		csbeq1 3874	. . . . . . 7 ⊢ (𝑣 = 𝐴 → ⦋𝑣 / 𝑢⦌𝐶 = ⦋𝐴 / 𝑢⦌𝐶)
166	137, 137, 140, 147, 76, 155, 163, 164, 14, 165	dvmptco 24554	. . . . . 6 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (⦋𝐴 / 𝑢⦌𝐶 · 𝐵)))
167		nfcvd 2978	. . . . . . . . . 10 ⊢ (𝐴 ∈ (𝑀(,)𝑁) → Ⅎ𝑢𝐸)
168		itgsubst.e	. . . . . . . . . 10 ⊢ (𝑢 = 𝐴 → 𝐶 = 𝐸)
169	167, 168	csbiegf 3904	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝑀(,)𝑁) → ⦋𝐴 / 𝑢⦌𝐶 = 𝐸)
170	140, 169	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ⦋𝐴 / 𝑢⦌𝐶 = 𝐸)
171	170	oveq1d 7157	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (⦋𝐴 / 𝑢⦌𝐶 · 𝐵) = (𝐸 · 𝐵))
172	171	mpteq2dva 5147	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ (⦋𝐴 / 𝑢⦌𝐶 · 𝐵)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)))
173	135, 166, 172	3eqtrd 2860	. . . . 5 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)))
174		resmpt 5891	. . . . . . . 8 ⊢ ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸))
175	138, 174	ax-mp 5	. . . . . . 7 ⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)
176		eqidd 2822	. . . . . . . . . 10 ⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) = (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶))
177	159, 10, 176, 168	fmptco 6877	. . . . . . . . 9 ⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸))
178	35, 52	cncfco 23498	. . . . . . . . 9 ⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) ∈ ((𝑋[,]𝑌)–cn→ℂ))
179	177, 178	eqeltrrd 2914	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ))
180		rescncf 23488	. . . . . . . 8 ⊢ ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ)))
181	138, 179, 180	mpsyl 68	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
182	175, 181	eqeltrrid 2918	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ ((𝑋(,)𝑌)–cn→ℂ))
183	182, 144	mulcncf 24030	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
184	173, 183	eqeltrd 2913	. . . 4 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
185		ioombl 24149	. . . . . . . 8 ⊢ (𝑋(,)𝑌) ∈ dom vol
186	185	a1i 11	. . . . . . 7 ⊢ (𝜑 → (𝑋(,)𝑌) ∈ dom vol)
187		fco 6517	. . . . . . . . . . 11 ⊢ (((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶):(𝑍(,)𝑊)⟶ℂ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑍(,)𝑊)) → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)):(𝑋[,]𝑌)⟶ℂ)
188	54, 158, 187	syl2anc 586	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)):(𝑋[,]𝑌)⟶ℂ)
189	177	feq1d 6485	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)):(𝑋[,]𝑌)⟶ℂ ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸):(𝑋[,]𝑌)⟶ℂ))
190	188, 189	mpbid 234	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸):(𝑋[,]𝑌)⟶ℂ)
191	190	fvmptelrn 6863	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐸 ∈ ℂ)
192	139, 191	sylan2 594	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐸 ∈ ℂ)
193		eqidd 2822	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸))
194		eqidd 2822	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵))
195	186, 192, 147, 193, 194	offval2 7412	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘_f · (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)))
196	173, 195	eqtr4d 2859	. . . . 5 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘_f · (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)))
197	138	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (𝑋(,)𝑌) ⊆ (𝑋[,]𝑌))
198		cniccibl 24424	. . . . . . . . 9 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ)) → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ 𝐿¹)
199	3, 4, 179, 198	syl3anc 1367	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ 𝐿¹)
200	197, 186, 191, 199	iblss 24388	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ 𝐿¹)
201		iblmbf 24351	. . . . . . 7 ⊢ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ 𝐿¹ → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ MblFn)
202	200, 201	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ MblFn)
203	143	simprd 498	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿¹)
204		cniccbdd 24045	. . . . . . . 8 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ)) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)
205	3, 4, 179, 204	syl3anc 1367	. . . . . . 7 ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)
206		ssralv 4021	. . . . . . . . . 10 ⊢ ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → (∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
207	138, 206	ax-mp 5	. . . . . . . . 9 ⊢ (∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)
208		eqid 2821	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)
209	208, 192	dmmptd 6479	. . . . . . . . . . 11 ⊢ (𝜑 → dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) = (𝑋(,)𝑌))
210	209	raleqdv 3411	. . . . . . . . . 10 ⊢ (𝜑 → (∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
211	175	fveq1i 6657	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌))‘𝑧) = ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)
212		fvres 6675	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (𝑋(,)𝑌) → (((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌))‘𝑧) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧))
213	211, 212	syl5eqr 2870	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝑋(,)𝑌) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧))
214	213	fveq2d 6660	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (𝑋(,)𝑌) → (abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) = (abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)))
215	214	breq1d 5062	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (𝑋(,)𝑌) → ((abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ (abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
216	215	ralbiia 3164	. . . . . . . . . 10 ⊢ (∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)
217	210, 216	syl6rbb 290	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
218	207, 217	syl5ib 246	. . . . . . . 8 ⊢ (𝜑 → (∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
219	218	reximdv 3273	. . . . . . 7 ⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
220	205, 219	mpd 15	. . . . . 6 ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)
221		bddmulibl 24422	. . . . . 6 ⊢ (((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ MblFn ∧ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿¹ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘_f · (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) ∈ 𝐿¹)
222	202, 203, 220, 221	syl3anc 1367	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘_f · (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) ∈ 𝐿¹)
223	196, 222	eqeltrd 2913	. . . 4 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) ∈ 𝐿¹)
224	3, 4, 1, 184, 223, 129	ftc2 24626	. . 3 ⊢ (𝜑 → ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) d𝑡 = (((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) − ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋)))
225		fveq2 6656	. . . . 5 ⊢ (𝑡 = 𝑥 → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) = ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥))
226		nfcv 2977	. . . . . . 7 ⊢ Ⅎ𝑥ℝ
227		nfcv 2977	. . . . . . 7 ⊢ Ⅎ𝑥 D
228		nfmpt1 5150	. . . . . . 7 ⊢ Ⅎ𝑥(𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)
229	226, 227, 228	nfov 7172	. . . . . 6 ⊢ Ⅎ𝑥(ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))
230		nfcv 2977	. . . . . 6 ⊢ Ⅎ𝑥𝑡
231	229, 230	nffv 6666	. . . . 5 ⊢ Ⅎ𝑥((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡)
232		nfcv 2977	. . . . 5 ⊢ Ⅎ𝑡((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥)
233	225, 231, 232	cbvitg 24359	. . . 4 ⊢ ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) d𝑡 = ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) d𝑥
234	173	fveq1d 6658	. . . . . 6 ⊢ (𝜑 → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) = ((𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))‘𝑥))
235		ovex 7175	. . . . . . 7 ⊢ (𝐸 · 𝐵) ∈ V
236		eqid 2821	. . . . . . . 8 ⊢ (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))
237	236	fvmpt2 6765	. . . . . . 7 ⊢ ((𝑥 ∈ (𝑋(,)𝑌) ∧ (𝐸 · 𝐵) ∈ V) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))‘𝑥) = (𝐸 · 𝐵))
238	235, 237	mpan2 689	. . . . . 6 ⊢ (𝑥 ∈ (𝑋(,)𝑌) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))‘𝑥) = (𝐸 · 𝐵))
239	234, 238	sylan9eq 2876	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) = (𝐸 · 𝐵))
240	239	itgeq2dv 24365	. . . 4 ⊢ (𝜑 → ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) d𝑥 = ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥)
241	233, 240	syl5eq 2868	. . 3 ⊢ (𝜑 → ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) d𝑡 = ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥)
242	17, 9	sseldi 3953	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑀[,]𝑁))
243		elicc2 12788	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝐴 ∈ (𝑀[,]𝑁) ↔ (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁)))
244	43, 40, 243	syl2anc 586	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 ∈ (𝑀[,]𝑁) ↔ (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁)))
245	244	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → (𝐴 ∈ (𝑀[,]𝑁) ↔ (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁)))
246	242, 245	mpbid 234	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁))
247	246	simp2d 1139	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝑀 ≤ 𝐴)
248	247	ditgpos 24439	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ∫(𝑀(,)𝐴)𝐶 d𝑢)
249	248	mpteq2dva 5147	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢) = (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))
250	249	fveq1d 6658	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑌) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌))
251		ubicc2 12840	. . . . . . . 8 ⊢ ((𝑋 ∈ ℝ^* ∧ 𝑌 ∈ ℝ^* ∧ 𝑋 ≤ 𝑌) → 𝑌 ∈ (𝑋[,]𝑌))
252	91, 92, 1, 251	syl3anc 1367	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ (𝑋[,]𝑌))
253		itgsubst.l	. . . . . . . . 9 ⊢ (𝑥 = 𝑌 → 𝐴 = 𝐿)
254		ditgeq2 24432	. . . . . . . . 9 ⊢ (𝐴 = 𝐿 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐿]𝐶 d𝑢)
255	253, 254	syl 17	. . . . . . . 8 ⊢ (𝑥 = 𝑌 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐿]𝐶 d𝑢)
256		eqid 2821	. . . . . . . 8 ⊢ (𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢) = (𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)
257		ditgex 24435	. . . . . . . 8 ⊢ ⨜[𝑀 → 𝐿]𝐶 d𝑢 ∈ V
258	255, 256, 257	fvmpt 6754	. . . . . . 7 ⊢ (𝑌 ∈ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑌) = ⨜[𝑀 → 𝐿]𝐶 d𝑢)
259	252, 258	syl 17	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑌) = ⨜[𝑀 → 𝐿]𝐶 d𝑢)
260	250, 259	eqtr3d 2858	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) = ⨜[𝑀 → 𝐿]𝐶 d𝑢)
261	249	fveq1d 6658	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑋) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋))
262		itgsubst.k	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → 𝐴 = 𝐾)
263		ditgeq2 24432	. . . . . . . . 9 ⊢ (𝐴 = 𝐾 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐾]𝐶 d𝑢)
264	262, 263	syl 17	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐾]𝐶 d𝑢)
265		ditgex 24435	. . . . . . . 8 ⊢ ⨜[𝑀 → 𝐾]𝐶 d𝑢 ∈ V
266	264, 256, 265	fvmpt 6754	. . . . . . 7 ⊢ (𝑋 ∈ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑋) = ⨜[𝑀 → 𝐾]𝐶 d𝑢)
267	94, 266	syl 17	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑋) = ⨜[𝑀 → 𝐾]𝐶 d𝑢)
268	261, 267	eqtr3d 2858	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋) = ⨜[𝑀 → 𝐾]𝐶 d𝑢)
269	260, 268	oveq12d 7160	. . . 4 ⊢ (𝜑 → (((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) − ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋)) = (⨜[𝑀 → 𝐿]𝐶 d𝑢 − ⨜[𝑀 → 𝐾]𝐶 d𝑢))
270		lbicc2 12839	. . . . . . 7 ⊢ ((𝑀 ∈ ℝ^* ∧ 𝑁 ∈ ℝ^* ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ (𝑀[,]𝑁))
271	103, 41, 109, 270	syl3anc 1367	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ (𝑀[,]𝑁))
272	262	eleq1d 2897	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (𝐴 ∈ (𝑀[,]𝑁) ↔ 𝐾 ∈ (𝑀[,]𝑁)))
273	242	ralrimiva 3182	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ (𝑋[,]𝑌)𝐴 ∈ (𝑀[,]𝑁))
274	272, 273, 94	rspcdva 3617	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ (𝑀[,]𝑁))
275	253	eleq1d 2897	. . . . . . 7 ⊢ (𝑥 = 𝑌 → (𝐴 ∈ (𝑀[,]𝑁) ↔ 𝐿 ∈ (𝑀[,]𝑁)))
276	275, 273, 252	rspcdva 3617	. . . . . 6 ⊢ (𝜑 → 𝐿 ∈ (𝑀[,]𝑁))
277	43, 40, 271, 274, 276, 56, 72	ditgsplit 24444	. . . . 5 ⊢ (𝜑 → ⨜[𝑀 → 𝐿]𝐶 d𝑢 = (⨜[𝑀 → 𝐾]𝐶 d𝑢 + ⨜[𝐾 → 𝐿]𝐶 d𝑢))
278	277	oveq1d 7157	. . . 4 ⊢ (𝜑 → (⨜[𝑀 → 𝐿]𝐶 d𝑢 − ⨜[𝑀 → 𝐾]𝐶 d𝑢) = ((⨜[𝑀 → 𝐾]𝐶 d𝑢 + ⨜[𝐾 → 𝐿]𝐶 d𝑢) − ⨜[𝑀 → 𝐾]𝐶 d𝑢))
279	43, 40, 271, 274, 56, 72	ditgcl 24441	. . . . 5 ⊢ (𝜑 → ⨜[𝑀 → 𝐾]𝐶 d𝑢 ∈ ℂ)
280	43, 40, 274, 276, 56, 72	ditgcl 24441	. . . . 5 ⊢ (𝜑 → ⨜[𝐾 → 𝐿]𝐶 d𝑢 ∈ ℂ)
281	279, 280	pncan2d 10985	. . . 4 ⊢ (𝜑 → ((⨜[𝑀 → 𝐾]𝐶 d𝑢 + ⨜[𝐾 → 𝐿]𝐶 d𝑢) − ⨜[𝑀 → 𝐾]𝐶 d𝑢) = ⨜[𝐾 → 𝐿]𝐶 d𝑢)
282	269, 278, 281	3eqtrd 2860	. . 3 ⊢ (𝜑 → (((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) − ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋)) = ⨜[𝐾 → 𝐿]𝐶 d𝑢)
283	224, 241, 282	3eqtr3d 2864	. 2 ⊢ (𝜑 → ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥 = ⨜[𝐾 → 𝐿]𝐶 d𝑢)
284	2, 283	eqtr2d 2857	1 ⊢ (𝜑 → ⨜[𝐾 → 𝐿]𝐶 d𝑢 = ⨜[𝑋 → 𝑌](𝐸 · 𝐵) d𝑥)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1537 ∈ wcel 2114 ∀wral 3138 ∃wrex 3139 Vcvv 3486 ⦋csb 3871 ∩ cin 3923 ⊆ wss 3924 ∅c0 4279 {cpr 4555 class class class wbr 5052 ↦ cmpt 5132 dom cdm 5541 ran crn 5542 ↾ cres 5543 ∘ ccom 5545 ⟶wf 6337 ‘cfv 6341 (class class class)co 7142 ∘_f cof 7393 ℂcc 10521 ℝcr 10522 + caddc 10526 · cmul 10528 ℝ^*cxr 10660 < clt 10661 ≤ cle 10662 − cmin 10856 (,)cioo 12725 [,]cicc 12728 abscabs 14578 TopOpenctopn 16678 topGenctg 16694 ℂ_fldccnfld 20528 intcnt 21608 –cn→ccncf 23467 volcvol 24047 MblFncmbf 24198 𝐿¹cibl 24201 ∫citg 24202 ⨜cdit 24429 D cdv 24446

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 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-rep 5176 ax-sep 5189 ax-nul 5196 ax-pow 5252 ax-pr 5316 ax-un 7447 ax-inf2 9090 ax-cc 9843 ax-cnex 10579 ax-resscn 10580 ax-1cn 10581 ax-icn 10582 ax-addcl 10583 ax-addrcl 10584 ax-mulcl 10585 ax-mulrcl 10586 ax-mulcom 10587 ax-addass 10588 ax-mulass 10589 ax-distr 10590 ax-i2m1 10591 ax-1ne0 10592 ax-1rid 10593 ax-rnegex 10594 ax-rrecex 10595 ax-cnre 10596 ax-pre-lttri 10597 ax-pre-lttrn 10598 ax-pre-ltadd 10599 ax-pre-mulgt0 10600 ax-pre-sup 10601 ax-addf 10602 ax-mulf 10603

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-fal 1550 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3488 df-sbc 3764 df-csb 3872 df-dif 3927 df-un 3929 df-in 3931 df-ss 3940 df-pss 3942 df-symdif 4207 df-nul 4280 df-if 4454 df-pw 4527 df-sn 4554 df-pr 4556 df-tp 4558 df-op 4560 df-uni 4825 df-int 4863 df-iun 4907 df-iin 4908 df-disj 5018 df-br 5053 df-opab 5115 df-mpt 5133 df-tr 5159 df-id 5446 df-eprel 5451 df-po 5460 df-so 5461 df-fr 5500 df-se 5501 df-we 5502 df-xp 5547 df-rel 5548 df-cnv 5549 df-co 5550 df-dm 5551 df-rn 5552 df-res 5553 df-ima 5554 df-pred 6134 df-ord 6180 df-on 6181 df-lim 6182 df-suc 6183 df-iota 6300 df-fun 6343 df-fn 6344 df-f 6345 df-f1 6346 df-fo 6347 df-f1o 6348 df-fv 6349 df-isom 6350 df-riota 7100 df-ov 7145 df-oprab 7146 df-mpo 7147 df-of 7395 df-ofr 7396 df-om 7567 df-1st 7675 df-2nd 7676 df-supp 7817 df-wrecs 7933 df-recs 7994 df-rdg 8032 df-1o 8088 df-2o 8089 df-oadd 8092 df-omul 8093 df-er 8275 df-map 8394 df-pm 8395 df-ixp 8448 df-en 8496 df-dom 8497 df-sdom 8498 df-fin 8499 df-fsupp 8820 df-fi 8861 df-sup 8892 df-inf 8893 df-oi 8960 df-dju 9316 df-card 9354 df-acn 9357 df-pnf 10663 df-mnf 10664 df-xr 10665 df-ltxr 10666 df-le 10667 df-sub 10858 df-neg 10859 df-div 11284 df-nn 11625 df-2 11687 df-3 11688 df-4 11689 df-5 11690 df-6 11691 df-7 11692 df-8 11693 df-9 11694 df-n0 11885 df-z 11969 df-dec 12086 df-uz 12231 df-q 12336 df-rp 12377 df-xneg 12494 df-xadd 12495 df-xmul 12496 df-ioo 12729 df-ioc 12730 df-ico 12731 df-icc 12732 df-fz 12883 df-fzo 13024 df-fl 13152 df-mod 13228 df-seq 13360 df-exp 13420 df-hash 13681 df-cj 14443 df-re 14444 df-im 14445 df-sqrt 14579 df-abs 14580 df-limsup 14813 df-clim 14830 df-rlim 14831 df-sum 15028 df-struct 16468 df-ndx 16469 df-slot 16470 df-base 16472 df-sets 16473 df-ress 16474 df-plusg 16561 df-mulr 16562 df-starv 16563 df-sca 16564 df-vsca 16565 df-ip 16566 df-tset 16567 df-ple 16568 df-ds 16570 df-unif 16571 df-hom 16572 df-cco 16573 df-rest 16679 df-topn 16680 df-0g 16698 df-gsum 16699 df-topgen 16700 df-pt 16701 df-prds 16704 df-xrs 16758 df-qtop 16763 df-imas 16764 df-xps 16766 df-mre 16840 df-mrc 16841 df-acs 16843 df-mgm 17835 df-sgrp 17884 df-mnd 17895 df-submnd 17940 df-mulg 18208 df-cntz 18430 df-cmn 18891 df-psmet 20520 df-xmet 20521 df-met 20522 df-bl 20523 df-mopn 20524 df-fbas 20525 df-fg 20526 df-cnfld 20529 df-top 21485 df-topon 21502 df-topsp 21524 df-bases 21537 df-cld 21610 df-ntr 21611 df-cls 21612 df-nei 21689 df-lp 21727 df-perf 21728 df-cn 21818 df-cnp 21819 df-haus 21906 df-cmp 21978 df-tx 22153 df-hmeo 22346 df-fil 22437 df-fm 22529 df-flim 22530 df-flf 22531 df-xms 22913 df-ms 22914 df-tms 22915 df-cncf 23469 df-ovol 24048 df-vol 24049 df-mbf 24203 df-itg1 24204 df-itg2 24205 df-ibl 24206 df-itg 24207 df-0p 24254 df-ditg 24430 df-limc 24449 df-dv 24450

This theorem is referenced by: itgsubst 24632

W3C validator