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 25572

Description: Lemma for itgsubst 25573. (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 25380	. 2 ⊢ (𝜑 → ⨜[𝑋 → 𝑌](𝐸 · 𝐵) d𝑥 = ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥)
3		itgsubst.x	. . . 4 ⊢ (𝜑 → 𝑋 ∈ ℝ)
4		itgsubst.y	. . . 4 ⊢ (𝜑 → 𝑌 ∈ ℝ)
5		ax-resscn 11169	. . . . . . . 8 ⊢ ℝ ⊆ ℂ
6	5	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℝ ⊆ ℂ)
7		iccssre 13408	. . . . . . . 8 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑋[,]𝑌) ⊆ ℝ)
8	3, 4, 7	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (𝑋[,]𝑌) ⊆ ℝ)
9		itgsubst.cl2	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑀(,)𝑁))
10		eqidd 2733	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) = (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴))
11		eqidd 2733	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) = (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢))
12		oveq2 7419	. . . . . . . . . . . 12 ⊢ (𝑣 = 𝐴 → (𝑀(,)𝑣) = (𝑀(,)𝐴))
13		itgeq1 25297	. . . . . . . . . . . 12 ⊢ ((𝑀(,)𝑣) = (𝑀(,)𝐴) → ∫(𝑀(,)𝑣)𝐶 d𝑢 = ∫(𝑀(,)𝐴)𝐶 d𝑢)
14	12, 13	syl 17	. . . . . . . . . . 11 ⊢ (𝑣 = 𝐴 → ∫(𝑀(,)𝑣)𝐶 d𝑢 = ∫(𝑀(,)𝐴)𝐶 d𝑢)
15	9, 10, 11, 14	fmptco 7129	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))
16	9	fmpttd 7116	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁))
17		ioossicc 13412	. . . . . . . . . . . . . . 15 ⊢ (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁)
18		itgsubst.z	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑍 ∈ ℝ^*)
19		itgsubst.w	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑊 ∈ ℝ^*)
20		itgsubst.m	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑀 ∈ (𝑍(,)𝑊))
21		eliooord 13385	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ∈ (𝑍(,)𝑊) → (𝑍 < 𝑀 ∧ 𝑀 < 𝑊))
22	20, 21	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑍 < 𝑀 ∧ 𝑀 < 𝑊))
23	22	simpld 495	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑍 < 𝑀)
24		itgsubst.n	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ (𝑍(,)𝑊))
25		eliooord 13385	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ (𝑍(,)𝑊) → (𝑍 < 𝑁 ∧ 𝑁 < 𝑊))
26	24, 25	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑍 < 𝑁 ∧ 𝑁 < 𝑊))
27	26	simprd 496	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 < 𝑊)
28		iccssioo 13395	. . . . . . . . . . . . . . . 16 ⊢ (((𝑍 ∈ ℝ^* ∧ 𝑊 ∈ ℝ^*) ∧ (𝑍 < 𝑀 ∧ 𝑁 < 𝑊)) → (𝑀[,]𝑁) ⊆ (𝑍(,)𝑊))
29	18, 19, 23, 27, 28	syl22anc 837	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀[,]𝑁) ⊆ (𝑍(,)𝑊))
30	17, 29	sstrid 3993	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀(,)𝑁) ⊆ (𝑍(,)𝑊))
31		ioossre 13387	. . . . . . . . . . . . . . . 16 ⊢ (𝑍(,)𝑊) ⊆ ℝ
32	31	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑍(,)𝑊) ⊆ ℝ)
33	32, 5	sstrdi 3994	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑍(,)𝑊) ⊆ ℂ)
34	30, 33	sstrd 3992	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑀(,)𝑁) ⊆ ℂ)
35		itgsubst.a	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊)))
36		cncfcdm 24421	. . . . . . . . . . . . 13 ⊢ (((𝑀(,)𝑁) ⊆ ℂ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊))) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑀(,)𝑁)) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁)))
37	34, 35, 36	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑀(,)𝑁)) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁)))
38	16, 37	mpbird 256	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑀(,)𝑁)))
39	17	sseli 3978	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ (𝑀(,)𝑁) → 𝑣 ∈ (𝑀[,]𝑁))
40	31, 24	sselid 3980	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑁 ∈ ℝ)
41	40	rexrd 11266	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 ∈ ℝ^*)
42	41	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → 𝑁 ∈ ℝ^*)
43	31, 20	sselid 3980	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑀 ∈ ℝ)
44		elicc2 13391	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑣 ∈ (𝑀[,]𝑁) ↔ (𝑣 ∈ ℝ ∧ 𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁)))
45	43, 40, 44	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑣 ∈ (𝑀[,]𝑁) ↔ (𝑣 ∈ ℝ ∧ 𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁)))
46	45	biimpa 477	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑣 ∈ ℝ ∧ 𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁))
47	46	simp3d 1144	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → 𝑣 ≤ 𝑁)
48		iooss2 13362	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℝ^* ∧ 𝑣 ≤ 𝑁) → (𝑀(,)𝑣) ⊆ (𝑀(,)𝑁))
49	42, 47, 48	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑀(,)𝑣) ⊆ (𝑀(,)𝑁))
50	49	sselda 3982	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑣)) → 𝑢 ∈ (𝑀(,)𝑁))
51	30	sselda 3982	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀(,)𝑁)) → 𝑢 ∈ (𝑍(,)𝑊))
52		itgsubst.c	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ))
53		cncff 24416	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ) → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶):(𝑍(,)𝑊)⟶ℂ)
54	52, 53	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶):(𝑍(,)𝑊)⟶ℂ)
55	54	fvmptelcdm 7114	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝑍(,)𝑊)) → 𝐶 ∈ ℂ)
56	51, 55	syldan 591	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀(,)𝑁)) → 𝐶 ∈ ℂ)
57	56	adantlr 713	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑁)) → 𝐶 ∈ ℂ)
58	50, 57	syldan 591	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑣)) → 𝐶 ∈ ℂ)
59		ioombl 25089	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀(,)𝑣) ∈ dom vol
60	59	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑀(,)𝑣) ∈ dom vol)
61	17	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁))
62		ioombl 25089	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀(,)𝑁) ∈ dom vol
63	62	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑀(,)𝑁) ∈ dom vol)
64	29	sselda 3982	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀[,]𝑁)) → 𝑢 ∈ (𝑍(,)𝑊))
65	64, 55	syldan 591	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀[,]𝑁)) → 𝐶 ∈ ℂ)
66	29	resmptd 6040	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ↾ (𝑀[,]𝑁)) = (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶))
67		rescncf 24420	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀[,]𝑁) ⊆ (𝑍(,)𝑊) → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ) → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℂ)))
68	29, 52, 67	sylc 65	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℂ))
69	66, 68	eqeltrrd 2834	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℂ))
70		cniccibl 25365	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℂ)) → (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ 𝐿¹)
71	43, 40, 69, 70	syl3anc 1371	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ 𝐿¹)
72	61, 63, 65, 71	iblss 25329	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) ∈ 𝐿¹)
73	72	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) ∈ 𝐿¹)
74	49, 60, 57, 73	iblss 25329	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑢 ∈ (𝑀(,)𝑣) ↦ 𝐶) ∈ 𝐿¹)
75	58, 74	itgcl 25308	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → ∫(𝑀(,)𝑣)𝐶 d𝑢 ∈ ℂ)
76	39, 75	sylan2 593	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀(,)𝑁)) → ∫(𝑀(,)𝑣)𝐶 d𝑢 ∈ ℂ)
77	76	fmpttd 7116	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢):(𝑀(,)𝑁)⟶ℂ)
78	30, 31	sstrdi 3994	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀(,)𝑁) ⊆ ℝ)
79		fveq2 6891	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑢 → ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) = ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢))
80		nffvmpt1 6902	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑢((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡)
81		nfcv 2903	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢)
82	79, 80, 81	cbvitg 25300	. . . . . . . . . . . . . . . . . 18 ⊢ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡 = ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) d𝑢
83		eqid 2732	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)
84	83	fvmpt2 7009	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑢 ∈ (𝑀(,)𝑁) ∧ 𝐶 ∈ ℂ) → ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) = 𝐶)
85	50, 58, 84	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑣)) → ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) = 𝐶)
86	85	itgeq2dv 25306	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) d𝑢 = ∫(𝑀(,)𝑣)𝐶 d𝑢)
87	82, 86	eqtrid 2784	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡 = ∫(𝑀(,)𝑣)𝐶 d𝑢)
88	87	mpteq2dva 5248	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡) = (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢))
89	88	oveq2d 7427	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡)) = (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)))
90		eqid 2732	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡) = (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡)
91	3	rexrd 11266	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑋 ∈ ℝ^*)
92	4	rexrd 11266	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑌 ∈ ℝ^*)
93		lbicc2 13443	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑋 ∈ ℝ^* ∧ 𝑌 ∈ ℝ^* ∧ 𝑋 ≤ 𝑌) → 𝑋 ∈ (𝑋[,]𝑌))
94	91, 92, 1, 93	syl3anc 1371	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑋 ∈ (𝑋[,]𝑌))
95		n0i 4333	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑋 ∈ (𝑋[,]𝑌) → ¬ (𝑋[,]𝑌) = ∅)
96	94, 95	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ¬ (𝑋[,]𝑌) = ∅)
97		feq3 6700	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀(,)𝑁) = ∅ → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅))
98	16, 97	syl5ibcom 244	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑀(,)𝑁) = ∅ → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅))
99		f00 6773	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅ ↔ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) = ∅ ∧ (𝑋[,]𝑌) = ∅))
100	99	simprbi 497	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅ → (𝑋[,]𝑌) = ∅)
101	98, 100	syl6 35	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑀(,)𝑁) = ∅ → (𝑋[,]𝑌) = ∅))
102	96, 101	mtod 197	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ¬ (𝑀(,)𝑁) = ∅)
103	43	rexrd 11266	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ ℝ^*)
104		ioo0 13351	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ ℝ^* ∧ 𝑁 ∈ ℝ^*) → ((𝑀(,)𝑁) = ∅ ↔ 𝑁 ≤ 𝑀))
105	103, 41, 104	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑀(,)𝑁) = ∅ ↔ 𝑁 ≤ 𝑀))
106	102, 105	mtbid 323	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ¬ 𝑁 ≤ 𝑀)
107	40, 43	letrid 11368	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑁 ≤ 𝑀 ∨ 𝑀 ≤ 𝑁))
108	107	ord 862	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (¬ 𝑁 ≤ 𝑀 → 𝑀 ≤ 𝑁))
109	106, 108	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ≤ 𝑁)
110		resmpt 6037	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶))
111	17, 110	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)
112		rescncf 24420	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℂ) → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) ∈ ((𝑀(,)𝑁)–cn→ℂ)))
113	17, 69, 112	mpsyl 68	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) ∈ ((𝑀(,)𝑁)–cn→ℂ))
114	111, 113	eqeltrrid 2838	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) ∈ ((𝑀(,)𝑁)–cn→ℂ))
115	90, 43, 40, 109, 114, 72	ftc1cn 25567	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶))
116	29, 31	sstrdi 3994	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑀[,]𝑁) ⊆ ℝ)
117		eqid 2732	. . . . . . . . . . . . . . . . 17 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
118	117	tgioo2 24326	. . . . . . . . . . . . . . . 16 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
119		iccntr 24344	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝑀[,]𝑁)) = (𝑀(,)𝑁))
120	43, 40, 119	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘(𝑀[,]𝑁)) = (𝑀(,)𝑁))
121	6, 116, 75, 118, 117, 120	dvmptntr 25495	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)))
122	89, 115, 121	3eqtr3rd 2781	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶))
123	122	dmeqd 5905	. . . . . . . . . . . . 13 ⊢ (𝜑 → dom (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = dom (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶))
124	83, 56	dmmptd 6695	. . . . . . . . . . . . 13 ⊢ (𝜑 → dom (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) = (𝑀(,)𝑁))
125	123, 124	eqtrd 2772	. . . . . . . . . . . 12 ⊢ (𝜑 → dom (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑀(,)𝑁))
126		dvcn 25445	. . . . . . . . . . . 12 ⊢ (((ℝ ⊆ ℂ ∧ (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢):(𝑀(,)𝑁)⟶ℂ ∧ (𝑀(,)𝑁) ⊆ ℝ) ∧ dom (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑀(,)𝑁)) → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∈ ((𝑀(,)𝑁)–cn→ℂ))
127	6, 77, 78, 125, 126	syl31anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∈ ((𝑀(,)𝑁)–cn→ℂ))
128	38, 127	cncfco 24430	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) ∈ ((𝑋[,]𝑌)–cn→ℂ))
129	15, 128	eqeltrrd 2834	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢) ∈ ((𝑋[,]𝑌)–cn→ℂ))
130		cncff 24416	. . . . . . . . 9 ⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢) ∈ ((𝑋[,]𝑌)–cn→ℂ) → (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢):(𝑋[,]𝑌)⟶ℂ)
131	129, 130	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢):(𝑋[,]𝑌)⟶ℂ)
132	131	fvmptelcdm 7114	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → ∫(𝑀(,)𝐴)𝐶 d𝑢 ∈ ℂ)
133		iccntr 24344	. . . . . . . 8 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝑋[,]𝑌)) = (𝑋(,)𝑌))
134	3, 4, 133	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘(𝑋[,]𝑌)) = (𝑋(,)𝑌))
135	6, 8, 132, 118, 117, 134	dvmptntr 25495	. . . . . 6 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)))
136		reelprrecn 11204	. . . . . . . 8 ⊢ ℝ ∈ {ℝ, ℂ}
137	136	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
138		ioossicc 13412	. . . . . . . . 9 ⊢ (𝑋(,)𝑌) ⊆ (𝑋[,]𝑌)
139	138	sseli 3978	. . . . . . . 8 ⊢ (𝑥 ∈ (𝑋(,)𝑌) → 𝑥 ∈ (𝑋[,]𝑌))
140	139, 9	sylan2 593	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐴 ∈ (𝑀(,)𝑁))
141		itgsubst.b	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ (((𝑋(,)𝑌)–cn→ℂ) ∩ 𝐿¹))
142		elin 3964	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ (((𝑋(,)𝑌)–cn→ℂ) ∩ 𝐿¹) ↔ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ) ∧ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿¹))
143	141, 142	sylib 217	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ) ∧ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿¹))
144	143	simpld 495	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ))
145		cncff 24416	. . . . . . . . 9 ⊢ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ) → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵):(𝑋(,)𝑌)⟶ℂ)
146	144, 145	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵):(𝑋(,)𝑌)⟶ℂ)
147	146	fvmptelcdm 7114	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐵 ∈ ℂ)
148	56	fmpttd 7116	. . . . . . . . 9 ⊢ (𝜑 → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶):(𝑀(,)𝑁)⟶ℂ)
149		nfcv 2903	. . . . . . . . . . 11 ⊢ Ⅎ𝑣𝐶
150		nfcsb1v 3918	. . . . . . . . . . 11 ⊢ Ⅎ𝑢⦋𝑣 / 𝑢⦌𝐶
151		csbeq1a 3907	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑣 → 𝐶 = ⦋𝑣 / 𝑢⦌𝐶)
152	149, 150, 151	cbvmpt 5259	. . . . . . . . . 10 ⊢ (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) = (𝑣 ∈ (𝑀(,)𝑁) ↦ ⦋𝑣 / 𝑢⦌𝐶)
153	152	fmpt 7111	. . . . . . . . 9 ⊢ (∀𝑣 ∈ (𝑀(,)𝑁)⦋𝑣 / 𝑢⦌𝐶 ∈ ℂ ↔ (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶):(𝑀(,)𝑁)⟶ℂ)
154	148, 153	sylibr 233	. . . . . . . 8 ⊢ (𝜑 → ∀𝑣 ∈ (𝑀(,)𝑁)⦋𝑣 / 𝑢⦌𝐶 ∈ ℂ)
155	154	r19.21bi 3248	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀(,)𝑁)) → ⦋𝑣 / 𝑢⦌𝐶 ∈ ℂ)
156	31, 5	sstri 3991	. . . . . . . . . 10 ⊢ (𝑍(,)𝑊) ⊆ ℂ
157		cncff 24416	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊)) → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑍(,)𝑊))
158	35, 157	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑍(,)𝑊))
159	158	fvmptelcdm 7114	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑍(,)𝑊))
160	156, 159	sselid 3980	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ ℂ)
161	6, 8, 160, 118, 117, 134	dvmptntr 25495	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐴)))
162		itgsubst.da	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵))
163	161, 162	eqtr3d 2774	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵))
164	122, 152	eqtrdi 2788	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑣 ∈ (𝑀(,)𝑁) ↦ ⦋𝑣 / 𝑢⦌𝐶))
165		csbeq1 3896	. . . . . . 7 ⊢ (𝑣 = 𝐴 → ⦋𝑣 / 𝑢⦌𝐶 = ⦋𝐴 / 𝑢⦌𝐶)
166	137, 137, 140, 147, 76, 155, 163, 164, 14, 165	dvmptco 25496	. . . . . 6 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (⦋𝐴 / 𝑢⦌𝐶 · 𝐵)))
167		nfcvd 2904	. . . . . . . . . 10 ⊢ (𝐴 ∈ (𝑀(,)𝑁) → Ⅎ𝑢𝐸)
168		itgsubst.e	. . . . . . . . . 10 ⊢ (𝑢 = 𝐴 → 𝐶 = 𝐸)
169	167, 168	csbiegf 3927	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝑀(,)𝑁) → ⦋𝐴 / 𝑢⦌𝐶 = 𝐸)
170	140, 169	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ⦋𝐴 / 𝑢⦌𝐶 = 𝐸)
171	170	oveq1d 7426	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (⦋𝐴 / 𝑢⦌𝐶 · 𝐵) = (𝐸 · 𝐵))
172	171	mpteq2dva 5248	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ (⦋𝐴 / 𝑢⦌𝐶 · 𝐵)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)))
173	135, 166, 172	3eqtrd 2776	. . . . 5 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)))
174		resmpt 6037	. . . . . . . 8 ⊢ ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸))
175	138, 174	ax-mp 5	. . . . . . 7 ⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)
176		eqidd 2733	. . . . . . . . . 10 ⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) = (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶))
177	159, 10, 176, 168	fmptco 7129	. . . . . . . . 9 ⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸))
178	35, 52	cncfco 24430	. . . . . . . . 9 ⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) ∈ ((𝑋[,]𝑌)–cn→ℂ))
179	177, 178	eqeltrrd 2834	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ))
180		rescncf 24420	. . . . . . . 8 ⊢ ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ)))
181	138, 179, 180	mpsyl 68	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
182	175, 181	eqeltrrid 2838	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ ((𝑋(,)𝑌)–cn→ℂ))
183	182, 144	mulcncf 24970	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
184	173, 183	eqeltrd 2833	. . . 4 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
185		ioombl 25089	. . . . . . . 8 ⊢ (𝑋(,)𝑌) ∈ dom vol
186	185	a1i 11	. . . . . . 7 ⊢ (𝜑 → (𝑋(,)𝑌) ∈ dom vol)
187		fco 6741	. . . . . . . . . . 11 ⊢ (((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶):(𝑍(,)𝑊)⟶ℂ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑍(,)𝑊)) → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)):(𝑋[,]𝑌)⟶ℂ)
188	54, 158, 187	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)):(𝑋[,]𝑌)⟶ℂ)
189	177	feq1d 6702	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)):(𝑋[,]𝑌)⟶ℂ ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸):(𝑋[,]𝑌)⟶ℂ))
190	188, 189	mpbid 231	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸):(𝑋[,]𝑌)⟶ℂ)
191	190	fvmptelcdm 7114	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐸 ∈ ℂ)
192	139, 191	sylan2 593	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐸 ∈ ℂ)
193		eqidd 2733	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸))
194		eqidd 2733	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵))
195	186, 192, 147, 193, 194	offval2 7692	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘_f · (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)))
196	173, 195	eqtr4d 2775	. . . . 5 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘_f · (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)))
197	138	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (𝑋(,)𝑌) ⊆ (𝑋[,]𝑌))
198		cniccibl 25365	. . . . . . . . 9 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ)) → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ 𝐿¹)
199	3, 4, 179, 198	syl3anc 1371	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ 𝐿¹)
200	197, 186, 191, 199	iblss 25329	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ 𝐿¹)
201		iblmbf 25292	. . . . . . 7 ⊢ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ 𝐿¹ → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ MblFn)
202	200, 201	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ MblFn)
203	143	simprd 496	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿¹)
204		cniccbdd 24985	. . . . . . . 8 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ)) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)
205	3, 4, 179, 204	syl3anc 1371	. . . . . . 7 ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)
206		ssralv 4050	. . . . . . . . . 10 ⊢ ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → (∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
207	138, 206	ax-mp 5	. . . . . . . . 9 ⊢ (∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)
208		eqid 2732	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)
209	208, 192	dmmptd 6695	. . . . . . . . . . 11 ⊢ (𝜑 → dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) = (𝑋(,)𝑌))
210	209	raleqdv 3325	. . . . . . . . . 10 ⊢ (𝜑 → (∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
211	175	fveq1i 6892	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌))‘𝑧) = ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)
212		fvres 6910	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (𝑋(,)𝑌) → (((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌))‘𝑧) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧))
213	211, 212	eqtr3id 2786	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝑋(,)𝑌) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧))
214	213	fveq2d 6895	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (𝑋(,)𝑌) → (abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) = (abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)))
215	214	breq1d 5158	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (𝑋(,)𝑌) → ((abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ (abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
216	215	ralbiia 3091	. . . . . . . . . 10 ⊢ (∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)
217	210, 216	bitr2di 287	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
218	207, 217	imbitrid 243	. . . . . . . 8 ⊢ (𝜑 → (∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
219	218	reximdv 3170	. . . . . . 7 ⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
220	205, 219	mpd 15	. . . . . 6 ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)
221		bddmulibl 25363	. . . . . 6 ⊢ (((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ MblFn ∧ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿¹ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘_f · (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) ∈ 𝐿¹)
222	202, 203, 220, 221	syl3anc 1371	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘_f · (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) ∈ 𝐿¹)
223	196, 222	eqeltrd 2833	. . . 4 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) ∈ 𝐿¹)
224	3, 4, 1, 184, 223, 129	ftc2 25568	. . 3 ⊢ (𝜑 → ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) d𝑡 = (((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) − ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋)))
225		fveq2 6891	. . . . 5 ⊢ (𝑡 = 𝑥 → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) = ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥))
226		nfcv 2903	. . . . . . 7 ⊢ Ⅎ𝑥ℝ
227		nfcv 2903	. . . . . . 7 ⊢ Ⅎ𝑥 D
228		nfmpt1 5256	. . . . . . 7 ⊢ Ⅎ𝑥(𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)
229	226, 227, 228	nfov 7441	. . . . . 6 ⊢ Ⅎ𝑥(ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))
230		nfcv 2903	. . . . . 6 ⊢ Ⅎ𝑥𝑡
231	229, 230	nffv 6901	. . . . 5 ⊢ Ⅎ𝑥((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡)
232		nfcv 2903	. . . . 5 ⊢ Ⅎ𝑡((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥)
233	225, 231, 232	cbvitg 25300	. . . 4 ⊢ ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) d𝑡 = ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) d𝑥
234	173	fveq1d 6893	. . . . . 6 ⊢ (𝜑 → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) = ((𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))‘𝑥))
235		ovex 7444	. . . . . . 7 ⊢ (𝐸 · 𝐵) ∈ V
236		eqid 2732	. . . . . . . 8 ⊢ (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))
237	236	fvmpt2 7009	. . . . . . 7 ⊢ ((𝑥 ∈ (𝑋(,)𝑌) ∧ (𝐸 · 𝐵) ∈ V) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))‘𝑥) = (𝐸 · 𝐵))
238	235, 237	mpan2 689	. . . . . 6 ⊢ (𝑥 ∈ (𝑋(,)𝑌) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))‘𝑥) = (𝐸 · 𝐵))
239	234, 238	sylan9eq 2792	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) = (𝐸 · 𝐵))
240	239	itgeq2dv 25306	. . . 4 ⊢ (𝜑 → ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) d𝑥 = ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥)
241	233, 240	eqtrid 2784	. . 3 ⊢ (𝜑 → ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) d𝑡 = ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥)
242	17, 9	sselid 3980	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑀[,]𝑁))
243		elicc2 13391	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝐴 ∈ (𝑀[,]𝑁) ↔ (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁)))
244	43, 40, 243	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 ∈ (𝑀[,]𝑁) ↔ (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁)))
245	244	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → (𝐴 ∈ (𝑀[,]𝑁) ↔ (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁)))
246	242, 245	mpbid 231	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁))
247	246	simp2d 1143	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝑀 ≤ 𝐴)
248	247	ditgpos 25380	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ∫(𝑀(,)𝐴)𝐶 d𝑢)
249	248	mpteq2dva 5248	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢) = (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))
250	249	fveq1d 6893	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑌) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌))
251		ubicc2 13444	. . . . . . . 8 ⊢ ((𝑋 ∈ ℝ^* ∧ 𝑌 ∈ ℝ^* ∧ 𝑋 ≤ 𝑌) → 𝑌 ∈ (𝑋[,]𝑌))
252	91, 92, 1, 251	syl3anc 1371	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ (𝑋[,]𝑌))
253		itgsubst.l	. . . . . . . . 9 ⊢ (𝑥 = 𝑌 → 𝐴 = 𝐿)
254		ditgeq2 25373	. . . . . . . . 9 ⊢ (𝐴 = 𝐿 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐿]𝐶 d𝑢)
255	253, 254	syl 17	. . . . . . . 8 ⊢ (𝑥 = 𝑌 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐿]𝐶 d𝑢)
256		eqid 2732	. . . . . . . 8 ⊢ (𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢) = (𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)
257		ditgex 25376	. . . . . . . 8 ⊢ ⨜[𝑀 → 𝐿]𝐶 d𝑢 ∈ V
258	255, 256, 257	fvmpt 6998	. . . . . . 7 ⊢ (𝑌 ∈ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑌) = ⨜[𝑀 → 𝐿]𝐶 d𝑢)
259	252, 258	syl 17	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑌) = ⨜[𝑀 → 𝐿]𝐶 d𝑢)
260	250, 259	eqtr3d 2774	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) = ⨜[𝑀 → 𝐿]𝐶 d𝑢)
261	249	fveq1d 6893	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑋) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋))
262		itgsubst.k	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → 𝐴 = 𝐾)
263		ditgeq2 25373	. . . . . . . . 9 ⊢ (𝐴 = 𝐾 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐾]𝐶 d𝑢)
264	262, 263	syl 17	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐾]𝐶 d𝑢)
265		ditgex 25376	. . . . . . . 8 ⊢ ⨜[𝑀 → 𝐾]𝐶 d𝑢 ∈ V
266	264, 256, 265	fvmpt 6998	. . . . . . 7 ⊢ (𝑋 ∈ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑋) = ⨜[𝑀 → 𝐾]𝐶 d𝑢)
267	94, 266	syl 17	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑋) = ⨜[𝑀 → 𝐾]𝐶 d𝑢)
268	261, 267	eqtr3d 2774	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋) = ⨜[𝑀 → 𝐾]𝐶 d𝑢)
269	260, 268	oveq12d 7429	. . . 4 ⊢ (𝜑 → (((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) − ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋)) = (⨜[𝑀 → 𝐿]𝐶 d𝑢 − ⨜[𝑀 → 𝐾]𝐶 d𝑢))
270		lbicc2 13443	. . . . . . 7 ⊢ ((𝑀 ∈ ℝ^* ∧ 𝑁 ∈ ℝ^* ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ (𝑀[,]𝑁))
271	103, 41, 109, 270	syl3anc 1371	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ (𝑀[,]𝑁))
272	262	eleq1d 2818	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (𝐴 ∈ (𝑀[,]𝑁) ↔ 𝐾 ∈ (𝑀[,]𝑁)))
273	242	ralrimiva 3146	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ (𝑋[,]𝑌)𝐴 ∈ (𝑀[,]𝑁))
274	272, 273, 94	rspcdva 3613	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ (𝑀[,]𝑁))
275	253	eleq1d 2818	. . . . . . 7 ⊢ (𝑥 = 𝑌 → (𝐴 ∈ (𝑀[,]𝑁) ↔ 𝐿 ∈ (𝑀[,]𝑁)))
276	275, 273, 252	rspcdva 3613	. . . . . 6 ⊢ (𝜑 → 𝐿 ∈ (𝑀[,]𝑁))
277	43, 40, 271, 274, 276, 56, 72	ditgsplit 25385	. . . . 5 ⊢ (𝜑 → ⨜[𝑀 → 𝐿]𝐶 d𝑢 = (⨜[𝑀 → 𝐾]𝐶 d𝑢 + ⨜[𝐾 → 𝐿]𝐶 d𝑢))
278	277	oveq1d 7426	. . . 4 ⊢ (𝜑 → (⨜[𝑀 → 𝐿]𝐶 d𝑢 − ⨜[𝑀 → 𝐾]𝐶 d𝑢) = ((⨜[𝑀 → 𝐾]𝐶 d𝑢 + ⨜[𝐾 → 𝐿]𝐶 d𝑢) − ⨜[𝑀 → 𝐾]𝐶 d𝑢))
279	43, 40, 271, 274, 56, 72	ditgcl 25382	. . . . 5 ⊢ (𝜑 → ⨜[𝑀 → 𝐾]𝐶 d𝑢 ∈ ℂ)
280	43, 40, 274, 276, 56, 72	ditgcl 25382	. . . . 5 ⊢ (𝜑 → ⨜[𝐾 → 𝐿]𝐶 d𝑢 ∈ ℂ)
281	279, 280	pncan2d 11575	. . . 4 ⊢ (𝜑 → ((⨜[𝑀 → 𝐾]𝐶 d𝑢 + ⨜[𝐾 → 𝐿]𝐶 d𝑢) − ⨜[𝑀 → 𝐾]𝐶 d𝑢) = ⨜[𝐾 → 𝐿]𝐶 d𝑢)
282	269, 278, 281	3eqtrd 2776	. . 3 ⊢ (𝜑 → (((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) − ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋)) = ⨜[𝐾 → 𝐿]𝐶 d𝑢)
283	224, 241, 282	3eqtr3d 2780	. 2 ⊢ (𝜑 → ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥 = ⨜[𝐾 → 𝐿]𝐶 d𝑢)
284	2, 283	eqtr2d 2773	1 ⊢ (𝜑 → ⨜[𝐾 → 𝐿]𝐶 d𝑢 = ⨜[𝑋 → 𝑌](𝐸 · 𝐵) d𝑥)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ∀wral 3061 ∃wrex 3070 Vcvv 3474 ⦋csb 3893 ∩ cin 3947 ⊆ wss 3948 ∅c0 4322 {cpr 4630 class class class wbr 5148 ↦ cmpt 5231 dom cdm 5676 ran crn 5677 ↾ cres 5678 ∘ ccom 5680 ⟶wf 6539 ‘cfv 6543 (class class class)co 7411 ∘_f cof 7670 ℂcc 11110 ℝcr 11111 + caddc 11115 · cmul 11117 ℝ^*cxr 11249 < clt 11250 ≤ cle 11251 − cmin 11446 (,)cioo 13326 [,]cicc 13329 abscabs 15183 TopOpenctopn 17369 topGenctg 17385 ℂ_fldccnfld 20950 intcnt 22528 –cn→ccncf 24399 volcvol 24987 MblFncmbf 25138 𝐿¹cibl 25141 ∫citg 25142 ⨜cdit 25370 D cdv 25387

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7727 ax-inf2 9638 ax-cc 10432 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189 ax-pre-sup 11190 ax-addf 11191 ax-mulf 11192

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-symdif 4242 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-tp 4633 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-iin 5000 df-disj 5114 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-se 5632 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-of 7672 df-ofr 7673 df-om 7858 df-1st 7977 df-2nd 7978 df-supp 8149 df-frecs 8268 df-wrecs 8299 df-recs 8373 df-rdg 8412 df-1o 8468 df-2o 8469 df-oadd 8472 df-omul 8473 df-er 8705 df-map 8824 df-pm 8825 df-ixp 8894 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-fsupp 9364 df-fi 9408 df-sup 9439 df-inf 9440 df-oi 9507 df-dju 9898 df-card 9936 df-acn 9939 df-pnf 11252 df-mnf 11253 df-xr 11254 df-ltxr 11255 df-le 11256 df-sub 11448 df-neg 11449 df-div 11874 df-nn 12215 df-2 12277 df-3 12278 df-4 12279 df-5 12280 df-6 12281 df-7 12282 df-8 12283 df-9 12284 df-n0 12475 df-z 12561 df-dec 12680 df-uz 12825 df-q 12935 df-rp 12977 df-xneg 13094 df-xadd 13095 df-xmul 13096 df-ioo 13330 df-ioc 13331 df-ico 13332 df-icc 13333 df-fz 13487 df-fzo 13630 df-fl 13759 df-mod 13837 df-seq 13969 df-exp 14030 df-hash 14293 df-cj 15048 df-re 15049 df-im 15050 df-sqrt 15184 df-abs 15185 df-limsup 15417 df-clim 15434 df-rlim 15435 df-sum 15635 df-struct 17082 df-sets 17099 df-slot 17117 df-ndx 17129 df-base 17147 df-ress 17176 df-plusg 17212 df-mulr 17213 df-starv 17214 df-sca 17215 df-vsca 17216 df-ip 17217 df-tset 17218 df-ple 17219 df-ds 17221 df-unif 17222 df-hom 17223 df-cco 17224 df-rest 17370 df-topn 17371 df-0g 17389 df-gsum 17390 df-topgen 17391 df-pt 17392 df-prds 17395 df-xrs 17450 df-qtop 17455 df-imas 17456 df-xps 17458 df-mre 17532 df-mrc 17533 df-acs 17535 df-mgm 18563 df-sgrp 18612 df-mnd 18628 df-submnd 18674 df-mulg 18953 df-cntz 19183 df-cmn 19652 df-psmet 20942 df-xmet 20943 df-met 20944 df-bl 20945 df-mopn 20946 df-fbas 20947 df-fg 20948 df-cnfld 20951 df-top 22403 df-topon 22420 df-topsp 22442 df-bases 22456 df-cld 22530 df-ntr 22531 df-cls 22532 df-nei 22609 df-lp 22647 df-perf 22648 df-cn 22738 df-cnp 22739 df-haus 22826 df-cmp 22898 df-tx 23073 df-hmeo 23266 df-fil 23357 df-fm 23449 df-flim 23450 df-flf 23451 df-xms 23833 df-ms 23834 df-tms 23835 df-cncf 24401 df-ovol 24988 df-vol 24989 df-mbf 25143 df-itg1 25144 df-itg2 25145 df-ibl 25146 df-itg 25147 df-0p 25194 df-ditg 25371 df-limc 25390 df-dv 25391

This theorem is referenced by: itgsubst 25573

W3C validator