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 26089

Description: Lemma for itgsubst 26090. (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 25891	. 2 ⊢ (𝜑 → ⨜[𝑋 → 𝑌](𝐸 · 𝐵) d𝑥 = ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥)
3		itgsubst.x	. . . 4 ⊢ (𝜑 → 𝑋 ∈ ℝ)
4		itgsubst.y	. . . 4 ⊢ (𝜑 → 𝑌 ∈ ℝ)
5		ax-resscn 11212	. . . . . . . 8 ⊢ ℝ ⊆ ℂ
6	5	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℝ ⊆ ℂ)
7		iccssre 13469	. . . . . . . 8 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑋[,]𝑌) ⊆ ℝ)
8	3, 4, 7	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (𝑋[,]𝑌) ⊆ ℝ)
9		itgsubst.cl2	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑀(,)𝑁))
10		eqidd 2738	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) = (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴))
11		eqidd 2738	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) = (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢))
12		oveq2 7439	. . . . . . . . . . . 12 ⊢ (𝑣 = 𝐴 → (𝑀(,)𝑣) = (𝑀(,)𝐴))
13		itgeq1 25808	. . . . . . . . . . . 12 ⊢ ((𝑀(,)𝑣) = (𝑀(,)𝐴) → ∫(𝑀(,)𝑣)𝐶 d𝑢 = ∫(𝑀(,)𝐴)𝐶 d𝑢)
14	12, 13	syl 17	. . . . . . . . . . 11 ⊢ (𝑣 = 𝐴 → ∫(𝑀(,)𝑣)𝐶 d𝑢 = ∫(𝑀(,)𝐴)𝐶 d𝑢)
15	9, 10, 11, 14	fmptco 7149	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))
16	9	fmpttd 7135	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁))
17		ioossicc 13473	. . . . . . . . . . . . . . 15 ⊢ (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁)
18		itgsubst.z	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑍 ∈ ℝ^*)
19		itgsubst.w	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑊 ∈ ℝ^*)
20		itgsubst.m	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑀 ∈ (𝑍(,)𝑊))
21		eliooord 13446	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ∈ (𝑍(,)𝑊) → (𝑍 < 𝑀 ∧ 𝑀 < 𝑊))
22	20, 21	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑍 < 𝑀 ∧ 𝑀 < 𝑊))
23	22	simpld 494	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑍 < 𝑀)
24		itgsubst.n	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ (𝑍(,)𝑊))
25		eliooord 13446	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ (𝑍(,)𝑊) → (𝑍 < 𝑁 ∧ 𝑁 < 𝑊))
26	24, 25	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑍 < 𝑁 ∧ 𝑁 < 𝑊))
27	26	simprd 495	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 < 𝑊)
28		iccssioo 13456	. . . . . . . . . . . . . . . 16 ⊢ (((𝑍 ∈ ℝ^* ∧ 𝑊 ∈ ℝ^*) ∧ (𝑍 < 𝑀 ∧ 𝑁 < 𝑊)) → (𝑀[,]𝑁) ⊆ (𝑍(,)𝑊))
29	18, 19, 23, 27, 28	syl22anc 839	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀[,]𝑁) ⊆ (𝑍(,)𝑊))
30	17, 29	sstrid 3995	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀(,)𝑁) ⊆ (𝑍(,)𝑊))
31		ioossre 13448	. . . . . . . . . . . . . . . 16 ⊢ (𝑍(,)𝑊) ⊆ ℝ
32	31	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑍(,)𝑊) ⊆ ℝ)
33	32, 5	sstrdi 3996	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑍(,)𝑊) ⊆ ℂ)
34	30, 33	sstrd 3994	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑀(,)𝑁) ⊆ ℂ)
35		itgsubst.a	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊)))
36		cncfcdm 24924	. . . . . . . . . . . . 13 ⊢ (((𝑀(,)𝑁) ⊆ ℂ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊))) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑀(,)𝑁)) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁)))
37	34, 35, 36	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑀(,)𝑁)) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁)))
38	16, 37	mpbird 257	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑀(,)𝑁)))
39	17	sseli 3979	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ (𝑀(,)𝑁) → 𝑣 ∈ (𝑀[,]𝑁))
40	31, 24	sselid 3981	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑁 ∈ ℝ)
41	40	rexrd 11311	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 ∈ ℝ^*)
42	41	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → 𝑁 ∈ ℝ^*)
43	31, 20	sselid 3981	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑀 ∈ ℝ)
44		elicc2 13452	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑣 ∈ (𝑀[,]𝑁) ↔ (𝑣 ∈ ℝ ∧ 𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁)))
45	43, 40, 44	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑣 ∈ (𝑀[,]𝑁) ↔ (𝑣 ∈ ℝ ∧ 𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁)))
46	45	biimpa 476	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑣 ∈ ℝ ∧ 𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁))
47	46	simp3d 1145	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → 𝑣 ≤ 𝑁)
48		iooss2 13423	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℝ^* ∧ 𝑣 ≤ 𝑁) → (𝑀(,)𝑣) ⊆ (𝑀(,)𝑁))
49	42, 47, 48	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑀(,)𝑣) ⊆ (𝑀(,)𝑁))
50	49	sselda 3983	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑣)) → 𝑢 ∈ (𝑀(,)𝑁))
51	30	sselda 3983	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀(,)𝑁)) → 𝑢 ∈ (𝑍(,)𝑊))
52		itgsubst.c	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ))
53		cncff 24919	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ) → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶):(𝑍(,)𝑊)⟶ℂ)
54	52, 53	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶):(𝑍(,)𝑊)⟶ℂ)
55	54	fvmptelcdm 7133	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝑍(,)𝑊)) → 𝐶 ∈ ℂ)
56	51, 55	syldan 591	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀(,)𝑁)) → 𝐶 ∈ ℂ)
57	56	adantlr 715	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑁)) → 𝐶 ∈ ℂ)
58	50, 57	syldan 591	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑣)) → 𝐶 ∈ ℂ)
59		ioombl 25600	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀(,)𝑣) ∈ dom vol
60	59	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑀(,)𝑣) ∈ dom vol)
61	17	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁))
62		ioombl 25600	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀(,)𝑁) ∈ dom vol
63	62	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑀(,)𝑁) ∈ dom vol)
64	29	sselda 3983	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀[,]𝑁)) → 𝑢 ∈ (𝑍(,)𝑊))
65	64, 55	syldan 591	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀[,]𝑁)) → 𝐶 ∈ ℂ)
66	29	resmptd 6058	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ↾ (𝑀[,]𝑁)) = (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶))
67		rescncf 24923	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀[,]𝑁) ⊆ (𝑍(,)𝑊) → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ) → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℂ)))
68	29, 52, 67	sylc 65	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℂ))
69	66, 68	eqeltrrd 2842	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℂ))
70		cniccibl 25876	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℂ)) → (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ 𝐿¹)
71	43, 40, 69, 70	syl3anc 1373	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ 𝐿¹)
72	61, 63, 65, 71	iblss 25840	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) ∈ 𝐿¹)
73	72	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) ∈ 𝐿¹)
74	49, 60, 57, 73	iblss 25840	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑢 ∈ (𝑀(,)𝑣) ↦ 𝐶) ∈ 𝐿¹)
75	58, 74	itgcl 25819	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → ∫(𝑀(,)𝑣)𝐶 d𝑢 ∈ ℂ)
76	39, 75	sylan2 593	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀(,)𝑁)) → ∫(𝑀(,)𝑣)𝐶 d𝑢 ∈ ℂ)
77	76	fmpttd 7135	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢):(𝑀(,)𝑁)⟶ℂ)
78	30, 31	sstrdi 3996	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀(,)𝑁) ⊆ ℝ)
79		fveq2 6906	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑢 → ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) = ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢))
80		nffvmpt1 6917	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑢((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡)
81		nfcv 2905	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢)
82	79, 80, 81	cbvitg 25811	. . . . . . . . . . . . . . . . . 18 ⊢ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡 = ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) d𝑢
83		eqid 2737	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)
84	83	fvmpt2 7027	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑢 ∈ (𝑀(,)𝑁) ∧ 𝐶 ∈ ℂ) → ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) = 𝐶)
85	50, 58, 84	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑣)) → ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) = 𝐶)
86	85	itgeq2dv 25817	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) d𝑢 = ∫(𝑀(,)𝑣)𝐶 d𝑢)
87	82, 86	eqtrid 2789	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡 = ∫(𝑀(,)𝑣)𝐶 d𝑢)
88	87	mpteq2dva 5242	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡) = (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢))
89	88	oveq2d 7447	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡)) = (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)))
90		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡) = (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡)
91	3	rexrd 11311	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑋 ∈ ℝ^*)
92	4	rexrd 11311	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑌 ∈ ℝ^*)
93		lbicc2 13504	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑋 ∈ ℝ^* ∧ 𝑌 ∈ ℝ^* ∧ 𝑋 ≤ 𝑌) → 𝑋 ∈ (𝑋[,]𝑌))
94	91, 92, 1, 93	syl3anc 1373	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑋 ∈ (𝑋[,]𝑌))
95		n0i 4340	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑋 ∈ (𝑋[,]𝑌) → ¬ (𝑋[,]𝑌) = ∅)
96	94, 95	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ¬ (𝑋[,]𝑌) = ∅)
97		feq3 6718	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀(,)𝑁) = ∅ → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅))
98	16, 97	syl5ibcom 245	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑀(,)𝑁) = ∅ → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅))
99		f00 6790	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅ ↔ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) = ∅ ∧ (𝑋[,]𝑌) = ∅))
100	99	simprbi 496	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅ → (𝑋[,]𝑌) = ∅)
101	98, 100	syl6 35	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑀(,)𝑁) = ∅ → (𝑋[,]𝑌) = ∅))
102	96, 101	mtod 198	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ¬ (𝑀(,)𝑁) = ∅)
103	43	rexrd 11311	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ ℝ^*)
104		ioo0 13412	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ ℝ^* ∧ 𝑁 ∈ ℝ^*) → ((𝑀(,)𝑁) = ∅ ↔ 𝑁 ≤ 𝑀))
105	103, 41, 104	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑀(,)𝑁) = ∅ ↔ 𝑁 ≤ 𝑀))
106	102, 105	mtbid 324	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ¬ 𝑁 ≤ 𝑀)
107	40, 43	letrid 11413	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑁 ≤ 𝑀 ∨ 𝑀 ≤ 𝑁))
108	107	ord 865	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (¬ 𝑁 ≤ 𝑀 → 𝑀 ≤ 𝑁))
109	106, 108	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ≤ 𝑁)
110		resmpt 6055	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶))
111	17, 110	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)
112		rescncf 24923	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℂ) → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) ∈ ((𝑀(,)𝑁)–cn→ℂ)))
113	17, 69, 112	mpsyl 68	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) ∈ ((𝑀(,)𝑁)–cn→ℂ))
114	111, 113	eqeltrrid 2846	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) ∈ ((𝑀(,)𝑁)–cn→ℂ))
115	90, 43, 40, 109, 114, 72	ftc1cn 26084	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶))
116	29, 31	sstrdi 3996	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑀[,]𝑁) ⊆ ℝ)
117		tgioo4 24826	. . . . . . . . . . . . . . . 16 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
118		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
119		iccntr 24843	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝑀[,]𝑁)) = (𝑀(,)𝑁))
120	43, 40, 119	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘(𝑀[,]𝑁)) = (𝑀(,)𝑁))
121	6, 116, 75, 117, 118, 120	dvmptntr 26009	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)))
122	89, 115, 121	3eqtr3rd 2786	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶))
123	122	dmeqd 5916	. . . . . . . . . . . . 13 ⊢ (𝜑 → dom (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = dom (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶))
124	83, 56	dmmptd 6713	. . . . . . . . . . . . 13 ⊢ (𝜑 → dom (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) = (𝑀(,)𝑁))
125	123, 124	eqtrd 2777	. . . . . . . . . . . 12 ⊢ (𝜑 → dom (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑀(,)𝑁))
126		dvcn 25957	. . . . . . . . . . . 12 ⊢ (((ℝ ⊆ ℂ ∧ (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢):(𝑀(,)𝑁)⟶ℂ ∧ (𝑀(,)𝑁) ⊆ ℝ) ∧ dom (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑀(,)𝑁)) → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∈ ((𝑀(,)𝑁)–cn→ℂ))
127	6, 77, 78, 125, 126	syl31anc 1375	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∈ ((𝑀(,)𝑁)–cn→ℂ))
128	38, 127	cncfco 24933	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) ∈ ((𝑋[,]𝑌)–cn→ℂ))
129	15, 128	eqeltrrd 2842	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢) ∈ ((𝑋[,]𝑌)–cn→ℂ))
130		cncff 24919	. . . . . . . . 9 ⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢) ∈ ((𝑋[,]𝑌)–cn→ℂ) → (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢):(𝑋[,]𝑌)⟶ℂ)
131	129, 130	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢):(𝑋[,]𝑌)⟶ℂ)
132	131	fvmptelcdm 7133	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → ∫(𝑀(,)𝐴)𝐶 d𝑢 ∈ ℂ)
133		iccntr 24843	. . . . . . . 8 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝑋[,]𝑌)) = (𝑋(,)𝑌))
134	3, 4, 133	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘(𝑋[,]𝑌)) = (𝑋(,)𝑌))
135	6, 8, 132, 117, 118, 134	dvmptntr 26009	. . . . . 6 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)))
136		reelprrecn 11247	. . . . . . . 8 ⊢ ℝ ∈ {ℝ, ℂ}
137	136	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
138		ioossicc 13473	. . . . . . . . 9 ⊢ (𝑋(,)𝑌) ⊆ (𝑋[,]𝑌)
139	138	sseli 3979	. . . . . . . 8 ⊢ (𝑥 ∈ (𝑋(,)𝑌) → 𝑥 ∈ (𝑋[,]𝑌))
140	139, 9	sylan2 593	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐴 ∈ (𝑀(,)𝑁))
141		itgsubst.b	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ (((𝑋(,)𝑌)–cn→ℂ) ∩ 𝐿¹))
142		elin 3967	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ (((𝑋(,)𝑌)–cn→ℂ) ∩ 𝐿¹) ↔ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ) ∧ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿¹))
143	141, 142	sylib 218	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ) ∧ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿¹))
144	143	simpld 494	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ))
145		cncff 24919	. . . . . . . . 9 ⊢ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ) → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵):(𝑋(,)𝑌)⟶ℂ)
146	144, 145	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵):(𝑋(,)𝑌)⟶ℂ)
147	146	fvmptelcdm 7133	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐵 ∈ ℂ)
148	56	fmpttd 7135	. . . . . . . . 9 ⊢ (𝜑 → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶):(𝑀(,)𝑁)⟶ℂ)
149		nfcv 2905	. . . . . . . . . . 11 ⊢ Ⅎ𝑣𝐶
150		nfcsb1v 3923	. . . . . . . . . . 11 ⊢ Ⅎ𝑢⦋𝑣 / 𝑢⦌𝐶
151		csbeq1a 3913	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑣 → 𝐶 = ⦋𝑣 / 𝑢⦌𝐶)
152	149, 150, 151	cbvmpt 5253	. . . . . . . . . 10 ⊢ (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) = (𝑣 ∈ (𝑀(,)𝑁) ↦ ⦋𝑣 / 𝑢⦌𝐶)
153	152	fmpt 7130	. . . . . . . . 9 ⊢ (∀𝑣 ∈ (𝑀(,)𝑁)⦋𝑣 / 𝑢⦌𝐶 ∈ ℂ ↔ (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶):(𝑀(,)𝑁)⟶ℂ)
154	148, 153	sylibr 234	. . . . . . . 8 ⊢ (𝜑 → ∀𝑣 ∈ (𝑀(,)𝑁)⦋𝑣 / 𝑢⦌𝐶 ∈ ℂ)
155	154	r19.21bi 3251	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀(,)𝑁)) → ⦋𝑣 / 𝑢⦌𝐶 ∈ ℂ)
156	31, 5	sstri 3993	. . . . . . . . . 10 ⊢ (𝑍(,)𝑊) ⊆ ℂ
157		cncff 24919	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊)) → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑍(,)𝑊))
158	35, 157	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑍(,)𝑊))
159	158	fvmptelcdm 7133	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑍(,)𝑊))
160	156, 159	sselid 3981	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ ℂ)
161	6, 8, 160, 117, 118, 134	dvmptntr 26009	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐴)))
162		itgsubst.da	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵))
163	161, 162	eqtr3d 2779	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵))
164	122, 152	eqtrdi 2793	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑣 ∈ (𝑀(,)𝑁) ↦ ⦋𝑣 / 𝑢⦌𝐶))
165		csbeq1 3902	. . . . . . 7 ⊢ (𝑣 = 𝐴 → ⦋𝑣 / 𝑢⦌𝐶 = ⦋𝐴 / 𝑢⦌𝐶)
166	137, 137, 140, 147, 76, 155, 163, 164, 14, 165	dvmptco 26010	. . . . . 6 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (⦋𝐴 / 𝑢⦌𝐶 · 𝐵)))
167		nfcvd 2906	. . . . . . . . . 10 ⊢ (𝐴 ∈ (𝑀(,)𝑁) → Ⅎ𝑢𝐸)
168		itgsubst.e	. . . . . . . . . 10 ⊢ (𝑢 = 𝐴 → 𝐶 = 𝐸)
169	167, 168	csbiegf 3932	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝑀(,)𝑁) → ⦋𝐴 / 𝑢⦌𝐶 = 𝐸)
170	140, 169	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ⦋𝐴 / 𝑢⦌𝐶 = 𝐸)
171	170	oveq1d 7446	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (⦋𝐴 / 𝑢⦌𝐶 · 𝐵) = (𝐸 · 𝐵))
172	171	mpteq2dva 5242	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ (⦋𝐴 / 𝑢⦌𝐶 · 𝐵)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)))
173	135, 166, 172	3eqtrd 2781	. . . . 5 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)))
174		resmpt 6055	. . . . . . . 8 ⊢ ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸))
175	138, 174	ax-mp 5	. . . . . . 7 ⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)
176		eqidd 2738	. . . . . . . . . 10 ⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) = (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶))
177	159, 10, 176, 168	fmptco 7149	. . . . . . . . 9 ⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸))
178	35, 52	cncfco 24933	. . . . . . . . 9 ⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) ∈ ((𝑋[,]𝑌)–cn→ℂ))
179	177, 178	eqeltrrd 2842	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ))
180		rescncf 24923	. . . . . . . 8 ⊢ ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ)))
181	138, 179, 180	mpsyl 68	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
182	175, 181	eqeltrrid 2846	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ ((𝑋(,)𝑌)–cn→ℂ))
183	182, 144	mulcncf 25480	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
184	173, 183	eqeltrd 2841	. . . 4 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
185		ioombl 25600	. . . . . . . 8 ⊢ (𝑋(,)𝑌) ∈ dom vol
186	185	a1i 11	. . . . . . 7 ⊢ (𝜑 → (𝑋(,)𝑌) ∈ dom vol)
187		fco 6760	. . . . . . . . . . 11 ⊢ (((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶):(𝑍(,)𝑊)⟶ℂ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑍(,)𝑊)) → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)):(𝑋[,]𝑌)⟶ℂ)
188	54, 158, 187	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)):(𝑋[,]𝑌)⟶ℂ)
189	177	feq1d 6720	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)):(𝑋[,]𝑌)⟶ℂ ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸):(𝑋[,]𝑌)⟶ℂ))
190	188, 189	mpbid 232	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸):(𝑋[,]𝑌)⟶ℂ)
191	190	fvmptelcdm 7133	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐸 ∈ ℂ)
192	139, 191	sylan2 593	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐸 ∈ ℂ)
193		eqidd 2738	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸))
194		eqidd 2738	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵))
195	186, 192, 147, 193, 194	offval2 7717	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘_f · (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)))
196	173, 195	eqtr4d 2780	. . . . 5 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘_f · (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)))
197	138	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (𝑋(,)𝑌) ⊆ (𝑋[,]𝑌))
198		cniccibl 25876	. . . . . . . . 9 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ)) → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ 𝐿¹)
199	3, 4, 179, 198	syl3anc 1373	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ 𝐿¹)
200	197, 186, 191, 199	iblss 25840	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ 𝐿¹)
201		iblmbf 25802	. . . . . . 7 ⊢ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ 𝐿¹ → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ MblFn)
202	200, 201	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ MblFn)
203	143	simprd 495	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿¹)
204		cniccbdd 25496	. . . . . . . 8 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ)) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)
205	3, 4, 179, 204	syl3anc 1373	. . . . . . 7 ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)
206		ssralv 4052	. . . . . . . . . 10 ⊢ ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → (∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
207	138, 206	ax-mp 5	. . . . . . . . 9 ⊢ (∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)
208		eqid 2737	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)
209	208, 192	dmmptd 6713	. . . . . . . . . . 11 ⊢ (𝜑 → dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) = (𝑋(,)𝑌))
210	209	raleqdv 3326	. . . . . . . . . 10 ⊢ (𝜑 → (∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
211	175	fveq1i 6907	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌))‘𝑧) = ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)
212		fvres 6925	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (𝑋(,)𝑌) → (((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌))‘𝑧) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧))
213	211, 212	eqtr3id 2791	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝑋(,)𝑌) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧))
214	213	fveq2d 6910	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (𝑋(,)𝑌) → (abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) = (abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)))
215	214	breq1d 5153	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (𝑋(,)𝑌) → ((abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ (abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
216	215	ralbiia 3091	. . . . . . . . . 10 ⊢ (∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)
217	210, 216	bitr2di 288	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
218	207, 217	imbitrid 244	. . . . . . . 8 ⊢ (𝜑 → (∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
219	218	reximdv 3170	. . . . . . 7 ⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
220	205, 219	mpd 15	. . . . . 6 ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)
221		bddmulibl 25874	. . . . . 6 ⊢ (((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ MblFn ∧ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿¹ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘_f · (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) ∈ 𝐿¹)
222	202, 203, 220, 221	syl3anc 1373	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘_f · (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) ∈ 𝐿¹)
223	196, 222	eqeltrd 2841	. . . 4 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) ∈ 𝐿¹)
224	3, 4, 1, 184, 223, 129	ftc2 26085	. . 3 ⊢ (𝜑 → ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) d𝑡 = (((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) − ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋)))
225		fveq2 6906	. . . . 5 ⊢ (𝑡 = 𝑥 → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) = ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥))
226		nfcv 2905	. . . . . . 7 ⊢ Ⅎ𝑥ℝ
227		nfcv 2905	. . . . . . 7 ⊢ Ⅎ𝑥 D
228		nfmpt1 5250	. . . . . . 7 ⊢ Ⅎ𝑥(𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)
229	226, 227, 228	nfov 7461	. . . . . 6 ⊢ Ⅎ𝑥(ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))
230		nfcv 2905	. . . . . 6 ⊢ Ⅎ𝑥𝑡
231	229, 230	nffv 6916	. . . . 5 ⊢ Ⅎ𝑥((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡)
232		nfcv 2905	. . . . 5 ⊢ Ⅎ𝑡((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥)
233	225, 231, 232	cbvitg 25811	. . . 4 ⊢ ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) d𝑡 = ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) d𝑥
234	173	fveq1d 6908	. . . . . 6 ⊢ (𝜑 → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) = ((𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))‘𝑥))
235		ovex 7464	. . . . . . 7 ⊢ (𝐸 · 𝐵) ∈ V
236		eqid 2737	. . . . . . . 8 ⊢ (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))
237	236	fvmpt2 7027	. . . . . . 7 ⊢ ((𝑥 ∈ (𝑋(,)𝑌) ∧ (𝐸 · 𝐵) ∈ V) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))‘𝑥) = (𝐸 · 𝐵))
238	235, 237	mpan2 691	. . . . . 6 ⊢ (𝑥 ∈ (𝑋(,)𝑌) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))‘𝑥) = (𝐸 · 𝐵))
239	234, 238	sylan9eq 2797	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) = (𝐸 · 𝐵))
240	239	itgeq2dv 25817	. . . 4 ⊢ (𝜑 → ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) d𝑥 = ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥)
241	233, 240	eqtrid 2789	. . 3 ⊢ (𝜑 → ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) d𝑡 = ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥)
242	17, 9	sselid 3981	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑀[,]𝑁))
243		elicc2 13452	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝐴 ∈ (𝑀[,]𝑁) ↔ (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁)))
244	43, 40, 243	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 ∈ (𝑀[,]𝑁) ↔ (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁)))
245	244	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → (𝐴 ∈ (𝑀[,]𝑁) ↔ (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁)))
246	242, 245	mpbid 232	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁))
247	246	simp2d 1144	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝑀 ≤ 𝐴)
248	247	ditgpos 25891	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ∫(𝑀(,)𝐴)𝐶 d𝑢)
249	248	mpteq2dva 5242	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢) = (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))
250	249	fveq1d 6908	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑌) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌))
251		ubicc2 13505	. . . . . . . 8 ⊢ ((𝑋 ∈ ℝ^* ∧ 𝑌 ∈ ℝ^* ∧ 𝑋 ≤ 𝑌) → 𝑌 ∈ (𝑋[,]𝑌))
252	91, 92, 1, 251	syl3anc 1373	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ (𝑋[,]𝑌))
253		itgsubst.l	. . . . . . . . 9 ⊢ (𝑥 = 𝑌 → 𝐴 = 𝐿)
254		ditgeq2 25884	. . . . . . . . 9 ⊢ (𝐴 = 𝐿 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐿]𝐶 d𝑢)
255	253, 254	syl 17	. . . . . . . 8 ⊢ (𝑥 = 𝑌 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐿]𝐶 d𝑢)
256		eqid 2737	. . . . . . . 8 ⊢ (𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢) = (𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)
257		ditgex 25887	. . . . . . . 8 ⊢ ⨜[𝑀 → 𝐿]𝐶 d𝑢 ∈ V
258	255, 256, 257	fvmpt 7016	. . . . . . 7 ⊢ (𝑌 ∈ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑌) = ⨜[𝑀 → 𝐿]𝐶 d𝑢)
259	252, 258	syl 17	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑌) = ⨜[𝑀 → 𝐿]𝐶 d𝑢)
260	250, 259	eqtr3d 2779	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) = ⨜[𝑀 → 𝐿]𝐶 d𝑢)
261	249	fveq1d 6908	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑋) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋))
262		itgsubst.k	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → 𝐴 = 𝐾)
263		ditgeq2 25884	. . . . . . . . 9 ⊢ (𝐴 = 𝐾 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐾]𝐶 d𝑢)
264	262, 263	syl 17	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐾]𝐶 d𝑢)
265		ditgex 25887	. . . . . . . 8 ⊢ ⨜[𝑀 → 𝐾]𝐶 d𝑢 ∈ V
266	264, 256, 265	fvmpt 7016	. . . . . . 7 ⊢ (𝑋 ∈ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑋) = ⨜[𝑀 → 𝐾]𝐶 d𝑢)
267	94, 266	syl 17	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑋) = ⨜[𝑀 → 𝐾]𝐶 d𝑢)
268	261, 267	eqtr3d 2779	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋) = ⨜[𝑀 → 𝐾]𝐶 d𝑢)
269	260, 268	oveq12d 7449	. . . 4 ⊢ (𝜑 → (((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) − ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋)) = (⨜[𝑀 → 𝐿]𝐶 d𝑢 − ⨜[𝑀 → 𝐾]𝐶 d𝑢))
270		lbicc2 13504	. . . . . . 7 ⊢ ((𝑀 ∈ ℝ^* ∧ 𝑁 ∈ ℝ^* ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ (𝑀[,]𝑁))
271	103, 41, 109, 270	syl3anc 1373	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ (𝑀[,]𝑁))
272	262	eleq1d 2826	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (𝐴 ∈ (𝑀[,]𝑁) ↔ 𝐾 ∈ (𝑀[,]𝑁)))
273	242	ralrimiva 3146	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ (𝑋[,]𝑌)𝐴 ∈ (𝑀[,]𝑁))
274	272, 273, 94	rspcdva 3623	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ (𝑀[,]𝑁))
275	253	eleq1d 2826	. . . . . . 7 ⊢ (𝑥 = 𝑌 → (𝐴 ∈ (𝑀[,]𝑁) ↔ 𝐿 ∈ (𝑀[,]𝑁)))
276	275, 273, 252	rspcdva 3623	. . . . . 6 ⊢ (𝜑 → 𝐿 ∈ (𝑀[,]𝑁))
277	43, 40, 271, 274, 276, 56, 72	ditgsplit 25896	. . . . 5 ⊢ (𝜑 → ⨜[𝑀 → 𝐿]𝐶 d𝑢 = (⨜[𝑀 → 𝐾]𝐶 d𝑢 + ⨜[𝐾 → 𝐿]𝐶 d𝑢))
278	277	oveq1d 7446	. . . 4 ⊢ (𝜑 → (⨜[𝑀 → 𝐿]𝐶 d𝑢 − ⨜[𝑀 → 𝐾]𝐶 d𝑢) = ((⨜[𝑀 → 𝐾]𝐶 d𝑢 + ⨜[𝐾 → 𝐿]𝐶 d𝑢) − ⨜[𝑀 → 𝐾]𝐶 d𝑢))
279	43, 40, 271, 274, 56, 72	ditgcl 25893	. . . . 5 ⊢ (𝜑 → ⨜[𝑀 → 𝐾]𝐶 d𝑢 ∈ ℂ)
280	43, 40, 274, 276, 56, 72	ditgcl 25893	. . . . 5 ⊢ (𝜑 → ⨜[𝐾 → 𝐿]𝐶 d𝑢 ∈ ℂ)
281	279, 280	pncan2d 11622	. . . 4 ⊢ (𝜑 → ((⨜[𝑀 → 𝐾]𝐶 d𝑢 + ⨜[𝐾 → 𝐿]𝐶 d𝑢) − ⨜[𝑀 → 𝐾]𝐶 d𝑢) = ⨜[𝐾 → 𝐿]𝐶 d𝑢)
282	269, 278, 281	3eqtrd 2781	. . 3 ⊢ (𝜑 → (((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) − ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋)) = ⨜[𝐾 → 𝐿]𝐶 d𝑢)
283	224, 241, 282	3eqtr3d 2785	. 2 ⊢ (𝜑 → ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥 = ⨜[𝐾 → 𝐿]𝐶 d𝑢)
284	2, 283	eqtr2d 2778	1 ⊢ (𝜑 → ⨜[𝐾 → 𝐿]𝐶 d𝑢 = ⨜[𝑋 → 𝑌](𝐸 · 𝐵) d𝑥)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 ∀wral 3061 ∃wrex 3070 Vcvv 3480 ⦋csb 3899 ∩ cin 3950 ⊆ wss 3951 ∅c0 4333 {cpr 4628 class class class wbr 5143 ↦ cmpt 5225 dom cdm 5685 ran crn 5686 ↾ cres 5687 ∘ ccom 5689 ⟶wf 6557 ‘cfv 6561 (class class class)co 7431 ∘_f cof 7695 ℂcc 11153 ℝcr 11154 + caddc 11158 · cmul 11160 ℝ^*cxr 11294 < clt 11295 ≤ cle 11296 − cmin 11492 (,)cioo 13387 [,]cicc 13390 abscabs 15273 TopOpenctopn 17466 topGenctg 17482 ℂ_fldccnfld 21364 intcnt 23025 –cn→ccncf 24902 volcvol 25498 MblFncmbf 25649 𝐿¹cibl 25652 ∫citg 25653 ⨜cdit 25881 D cdv 25898

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-inf2 9681 ax-cc 10475 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232 ax-pre-sup 11233 ax-addf 11234

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-symdif 4253 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-tp 4631 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-iin 4994 df-disj 5111 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-se 5638 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-isom 6570 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-of 7697 df-ofr 7698 df-om 7888 df-1st 8014 df-2nd 8015 df-supp 8186 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-1o 8506 df-2o 8507 df-oadd 8510 df-omul 8511 df-er 8745 df-map 8868 df-pm 8869 df-ixp 8938 df-en 8986 df-dom 8987 df-sdom 8988 df-fin 8989 df-fsupp 9402 df-fi 9451 df-sup 9482 df-inf 9483 df-oi 9550 df-dju 9941 df-card 9979 df-acn 9982 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-div 11921 df-nn 12267 df-2 12329 df-3 12330 df-4 12331 df-5 12332 df-6 12333 df-7 12334 df-8 12335 df-9 12336 df-n0 12527 df-z 12614 df-dec 12734 df-uz 12879 df-q 12991 df-rp 13035 df-xneg 13154 df-xadd 13155 df-xmul 13156 df-ioo 13391 df-ioc 13392 df-ico 13393 df-icc 13394 df-fz 13548 df-fzo 13695 df-fl 13832 df-mod 13910 df-seq 14043 df-exp 14103 df-hash 14370 df-cj 15138 df-re 15139 df-im 15140 df-sqrt 15274 df-abs 15275 df-limsup 15507 df-clim 15524 df-rlim 15525 df-sum 15723 df-struct 17184 df-sets 17201 df-slot 17219 df-ndx 17231 df-base 17248 df-ress 17275 df-plusg 17310 df-mulr 17311 df-starv 17312 df-sca 17313 df-vsca 17314 df-ip 17315 df-tset 17316 df-ple 17317 df-ds 17319 df-unif 17320 df-hom 17321 df-cco 17322 df-rest 17467 df-topn 17468 df-0g 17486 df-gsum 17487 df-topgen 17488 df-pt 17489 df-prds 17492 df-xrs 17547 df-qtop 17552 df-imas 17553 df-xps 17555 df-mre 17629 df-mrc 17630 df-acs 17632 df-mgm 18653 df-sgrp 18732 df-mnd 18748 df-submnd 18797 df-mulg 19086 df-cntz 19335 df-cmn 19800 df-psmet 21356 df-xmet 21357 df-met 21358 df-bl 21359 df-mopn 21360 df-fbas 21361 df-fg 21362 df-cnfld 21365 df-top 22900 df-topon 22917 df-topsp 22939 df-bases 22953 df-cld 23027 df-ntr 23028 df-cls 23029 df-nei 23106 df-lp 23144 df-perf 23145 df-cn 23235 df-cnp 23236 df-haus 23323 df-cmp 23395 df-tx 23570 df-hmeo 23763 df-fil 23854 df-fm 23946 df-flim 23947 df-flf 23948 df-xms 24330 df-ms 24331 df-tms 24332 df-cncf 24904 df-ovol 25499 df-vol 25500 df-mbf 25654 df-itg1 25655 df-itg2 25656 df-ibl 25657 df-itg 25658 df-0p 25705 df-ditg 25882 df-limc 25901 df-dv 25902

This theorem is referenced by: itgsubst 26090

W3C validator