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 25798

Description: Lemma for itgsubst 25799. (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 25606	. 2 ⊢ (𝜑 → ⨜[𝑋 → 𝑌](𝐸 · 𝐵) d𝑥 = ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥)
3		itgsubst.x	. . . 4 ⊢ (𝜑 → 𝑋 ∈ ℝ)
4		itgsubst.y	. . . 4 ⊢ (𝜑 → 𝑌 ∈ ℝ)
5		ax-resscn 11170	. . . . . . . 8 ⊢ ℝ ⊆ ℂ
6	5	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℝ ⊆ ℂ)
7		iccssre 13411	. . . . . . . 8 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑋[,]𝑌) ⊆ ℝ)
8	3, 4, 7	syl2anc 583	. . . . . . 7 ⊢ (𝜑 → (𝑋[,]𝑌) ⊆ ℝ)
9		itgsubst.cl2	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑀(,)𝑁))
10		eqidd 2732	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) = (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴))
11		eqidd 2732	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) = (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢))
12		oveq2 7420	. . . . . . . . . . . 12 ⊢ (𝑣 = 𝐴 → (𝑀(,)𝑣) = (𝑀(,)𝐴))
13		itgeq1 25523	. . . . . . . . . . . 12 ⊢ ((𝑀(,)𝑣) = (𝑀(,)𝐴) → ∫(𝑀(,)𝑣)𝐶 d𝑢 = ∫(𝑀(,)𝐴)𝐶 d𝑢)
14	12, 13	syl 17	. . . . . . . . . . 11 ⊢ (𝑣 = 𝐴 → ∫(𝑀(,)𝑣)𝐶 d𝑢 = ∫(𝑀(,)𝐴)𝐶 d𝑢)
15	9, 10, 11, 14	fmptco 7130	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))
16	9	fmpttd 7117	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁))
17		ioossicc 13415	. . . . . . . . . . . . . . 15 ⊢ (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁)
18		itgsubst.z	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑍 ∈ ℝ^*)
19		itgsubst.w	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑊 ∈ ℝ^*)
20		itgsubst.m	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑀 ∈ (𝑍(,)𝑊))
21		eliooord 13388	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ∈ (𝑍(,)𝑊) → (𝑍 < 𝑀 ∧ 𝑀 < 𝑊))
22	20, 21	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑍 < 𝑀 ∧ 𝑀 < 𝑊))
23	22	simpld 494	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑍 < 𝑀)
24		itgsubst.n	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ (𝑍(,)𝑊))
25		eliooord 13388	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ (𝑍(,)𝑊) → (𝑍 < 𝑁 ∧ 𝑁 < 𝑊))
26	24, 25	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑍 < 𝑁 ∧ 𝑁 < 𝑊))
27	26	simprd 495	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 < 𝑊)
28		iccssioo 13398	. . . . . . . . . . . . . . . 16 ⊢ (((𝑍 ∈ ℝ^* ∧ 𝑊 ∈ ℝ^*) ∧ (𝑍 < 𝑀 ∧ 𝑁 < 𝑊)) → (𝑀[,]𝑁) ⊆ (𝑍(,)𝑊))
29	18, 19, 23, 27, 28	syl22anc 836	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀[,]𝑁) ⊆ (𝑍(,)𝑊))
30	17, 29	sstrid 3994	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀(,)𝑁) ⊆ (𝑍(,)𝑊))
31		ioossre 13390	. . . . . . . . . . . . . . . 16 ⊢ (𝑍(,)𝑊) ⊆ ℝ
32	31	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑍(,)𝑊) ⊆ ℝ)
33	32, 5	sstrdi 3995	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑍(,)𝑊) ⊆ ℂ)
34	30, 33	sstrd 3993	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑀(,)𝑁) ⊆ ℂ)
35		itgsubst.a	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊)))
36		cncfcdm 24639	. . . . . . . . . . . . 13 ⊢ (((𝑀(,)𝑁) ⊆ ℂ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊))) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑀(,)𝑁)) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁)))
37	34, 35, 36	syl2anc 583	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑀(,)𝑁)) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁)))
38	16, 37	mpbird 256	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑀(,)𝑁)))
39	17	sseli 3979	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ (𝑀(,)𝑁) → 𝑣 ∈ (𝑀[,]𝑁))
40	31, 24	sselid 3981	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑁 ∈ ℝ)
41	40	rexrd 11269	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 ∈ ℝ^*)
42	41	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → 𝑁 ∈ ℝ^*)
43	31, 20	sselid 3981	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑀 ∈ ℝ)
44		elicc2 13394	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑣 ∈ (𝑀[,]𝑁) ↔ (𝑣 ∈ ℝ ∧ 𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁)))
45	43, 40, 44	syl2anc 583	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑣 ∈ (𝑀[,]𝑁) ↔ (𝑣 ∈ ℝ ∧ 𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁)))
46	45	biimpa 476	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑣 ∈ ℝ ∧ 𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁))
47	46	simp3d 1143	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → 𝑣 ≤ 𝑁)
48		iooss2 13365	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℝ^* ∧ 𝑣 ≤ 𝑁) → (𝑀(,)𝑣) ⊆ (𝑀(,)𝑁))
49	42, 47, 48	syl2anc 583	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑀(,)𝑣) ⊆ (𝑀(,)𝑁))
50	49	sselda 3983	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑣)) → 𝑢 ∈ (𝑀(,)𝑁))
51	30	sselda 3983	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀(,)𝑁)) → 𝑢 ∈ (𝑍(,)𝑊))
52		itgsubst.c	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ))
53		cncff 24634	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ) → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶):(𝑍(,)𝑊)⟶ℂ)
54	52, 53	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶):(𝑍(,)𝑊)⟶ℂ)
55	54	fvmptelcdm 7115	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝑍(,)𝑊)) → 𝐶 ∈ ℂ)
56	51, 55	syldan 590	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀(,)𝑁)) → 𝐶 ∈ ℂ)
57	56	adantlr 712	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑁)) → 𝐶 ∈ ℂ)
58	50, 57	syldan 590	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑣)) → 𝐶 ∈ ℂ)
59		ioombl 25315	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀(,)𝑣) ∈ dom vol
60	59	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑀(,)𝑣) ∈ dom vol)
61	17	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁))
62		ioombl 25315	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀(,)𝑁) ∈ dom vol
63	62	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑀(,)𝑁) ∈ dom vol)
64	29	sselda 3983	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀[,]𝑁)) → 𝑢 ∈ (𝑍(,)𝑊))
65	64, 55	syldan 590	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀[,]𝑁)) → 𝐶 ∈ ℂ)
66	29	resmptd 6041	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ↾ (𝑀[,]𝑁)) = (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶))
67		rescncf 24638	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀[,]𝑁) ⊆ (𝑍(,)𝑊) → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ) → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℂ)))
68	29, 52, 67	sylc 65	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℂ))
69	66, 68	eqeltrrd 2833	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℂ))
70		cniccibl 25591	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℂ)) → (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ 𝐿¹)
71	43, 40, 69, 70	syl3anc 1370	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ 𝐿¹)
72	61, 63, 65, 71	iblss 25555	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) ∈ 𝐿¹)
73	72	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) ∈ 𝐿¹)
74	49, 60, 57, 73	iblss 25555	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑢 ∈ (𝑀(,)𝑣) ↦ 𝐶) ∈ 𝐿¹)
75	58, 74	itgcl 25534	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → ∫(𝑀(,)𝑣)𝐶 d𝑢 ∈ ℂ)
76	39, 75	sylan2 592	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀(,)𝑁)) → ∫(𝑀(,)𝑣)𝐶 d𝑢 ∈ ℂ)
77	76	fmpttd 7117	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢):(𝑀(,)𝑁)⟶ℂ)
78	30, 31	sstrdi 3995	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀(,)𝑁) ⊆ ℝ)
79		fveq2 6892	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑢 → ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) = ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢))
80		nffvmpt1 6903	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑢((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡)
81		nfcv 2902	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢)
82	79, 80, 81	cbvitg 25526	. . . . . . . . . . . . . . . . . 18 ⊢ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡 = ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) d𝑢
83		eqid 2731	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)
84	83	fvmpt2 7010	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑢 ∈ (𝑀(,)𝑁) ∧ 𝐶 ∈ ℂ) → ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) = 𝐶)
85	50, 58, 84	syl2anc 583	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑣)) → ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) = 𝐶)
86	85	itgeq2dv 25532	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) d𝑢 = ∫(𝑀(,)𝑣)𝐶 d𝑢)
87	82, 86	eqtrid 2783	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡 = ∫(𝑀(,)𝑣)𝐶 d𝑢)
88	87	mpteq2dva 5249	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡) = (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢))
89	88	oveq2d 7428	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡)) = (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)))
90		eqid 2731	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡) = (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡)
91	3	rexrd 11269	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑋 ∈ ℝ^*)
92	4	rexrd 11269	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑌 ∈ ℝ^*)
93		lbicc2 13446	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑋 ∈ ℝ^* ∧ 𝑌 ∈ ℝ^* ∧ 𝑋 ≤ 𝑌) → 𝑋 ∈ (𝑋[,]𝑌))
94	91, 92, 1, 93	syl3anc 1370	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑋 ∈ (𝑋[,]𝑌))
95		n0i 4334	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑋 ∈ (𝑋[,]𝑌) → ¬ (𝑋[,]𝑌) = ∅)
96	94, 95	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ¬ (𝑋[,]𝑌) = ∅)
97		feq3 6701	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀(,)𝑁) = ∅ → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅))
98	16, 97	syl5ibcom 244	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑀(,)𝑁) = ∅ → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅))
99		f00 6774	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅ ↔ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) = ∅ ∧ (𝑋[,]𝑌) = ∅))
100	99	simprbi 496	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅ → (𝑋[,]𝑌) = ∅)
101	98, 100	syl6 35	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑀(,)𝑁) = ∅ → (𝑋[,]𝑌) = ∅))
102	96, 101	mtod 197	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ¬ (𝑀(,)𝑁) = ∅)
103	43	rexrd 11269	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ ℝ^*)
104		ioo0 13354	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ ℝ^* ∧ 𝑁 ∈ ℝ^*) → ((𝑀(,)𝑁) = ∅ ↔ 𝑁 ≤ 𝑀))
105	103, 41, 104	syl2anc 583	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑀(,)𝑁) = ∅ ↔ 𝑁 ≤ 𝑀))
106	102, 105	mtbid 323	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ¬ 𝑁 ≤ 𝑀)
107	40, 43	letrid 11371	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑁 ≤ 𝑀 ∨ 𝑀 ≤ 𝑁))
108	107	ord 861	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (¬ 𝑁 ≤ 𝑀 → 𝑀 ≤ 𝑁))
109	106, 108	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ≤ 𝑁)
110		resmpt 6038	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶))
111	17, 110	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)
112		rescncf 24638	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℂ) → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) ∈ ((𝑀(,)𝑁)–cn→ℂ)))
113	17, 69, 112	mpsyl 68	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) ∈ ((𝑀(,)𝑁)–cn→ℂ))
114	111, 113	eqeltrrid 2837	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) ∈ ((𝑀(,)𝑁)–cn→ℂ))
115	90, 43, 40, 109, 114, 72	ftc1cn 25793	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶))
116	29, 31	sstrdi 3995	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑀[,]𝑁) ⊆ ℝ)
117		eqid 2731	. . . . . . . . . . . . . . . . 17 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
118	117	tgioo2 24540	. . . . . . . . . . . . . . . 16 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
119		iccntr 24558	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝑀[,]𝑁)) = (𝑀(,)𝑁))
120	43, 40, 119	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘(𝑀[,]𝑁)) = (𝑀(,)𝑁))
121	6, 116, 75, 118, 117, 120	dvmptntr 25721	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)))
122	89, 115, 121	3eqtr3rd 2780	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶))
123	122	dmeqd 5906	. . . . . . . . . . . . 13 ⊢ (𝜑 → dom (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = dom (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶))
124	83, 56	dmmptd 6696	. . . . . . . . . . . . 13 ⊢ (𝜑 → dom (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) = (𝑀(,)𝑁))
125	123, 124	eqtrd 2771	. . . . . . . . . . . 12 ⊢ (𝜑 → dom (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑀(,)𝑁))
126		dvcn 25671	. . . . . . . . . . . 12 ⊢ (((ℝ ⊆ ℂ ∧ (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢):(𝑀(,)𝑁)⟶ℂ ∧ (𝑀(,)𝑁) ⊆ ℝ) ∧ dom (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑀(,)𝑁)) → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∈ ((𝑀(,)𝑁)–cn→ℂ))
127	6, 77, 78, 125, 126	syl31anc 1372	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∈ ((𝑀(,)𝑁)–cn→ℂ))
128	38, 127	cncfco 24648	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) ∈ ((𝑋[,]𝑌)–cn→ℂ))
129	15, 128	eqeltrrd 2833	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢) ∈ ((𝑋[,]𝑌)–cn→ℂ))
130		cncff 24634	. . . . . . . . 9 ⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢) ∈ ((𝑋[,]𝑌)–cn→ℂ) → (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢):(𝑋[,]𝑌)⟶ℂ)
131	129, 130	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢):(𝑋[,]𝑌)⟶ℂ)
132	131	fvmptelcdm 7115	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → ∫(𝑀(,)𝐴)𝐶 d𝑢 ∈ ℂ)
133		iccntr 24558	. . . . . . . 8 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝑋[,]𝑌)) = (𝑋(,)𝑌))
134	3, 4, 133	syl2anc 583	. . . . . . 7 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘(𝑋[,]𝑌)) = (𝑋(,)𝑌))
135	6, 8, 132, 118, 117, 134	dvmptntr 25721	. . . . . 6 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)))
136		reelprrecn 11205	. . . . . . . 8 ⊢ ℝ ∈ {ℝ, ℂ}
137	136	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
138		ioossicc 13415	. . . . . . . . 9 ⊢ (𝑋(,)𝑌) ⊆ (𝑋[,]𝑌)
139	138	sseli 3979	. . . . . . . 8 ⊢ (𝑥 ∈ (𝑋(,)𝑌) → 𝑥 ∈ (𝑋[,]𝑌))
140	139, 9	sylan2 592	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐴 ∈ (𝑀(,)𝑁))
141		itgsubst.b	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ (((𝑋(,)𝑌)–cn→ℂ) ∩ 𝐿¹))
142		elin 3965	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ (((𝑋(,)𝑌)–cn→ℂ) ∩ 𝐿¹) ↔ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ) ∧ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿¹))
143	141, 142	sylib 217	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ) ∧ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿¹))
144	143	simpld 494	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ))
145		cncff 24634	. . . . . . . . 9 ⊢ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ) → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵):(𝑋(,)𝑌)⟶ℂ)
146	144, 145	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵):(𝑋(,)𝑌)⟶ℂ)
147	146	fvmptelcdm 7115	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐵 ∈ ℂ)
148	56	fmpttd 7117	. . . . . . . . 9 ⊢ (𝜑 → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶):(𝑀(,)𝑁)⟶ℂ)
149		nfcv 2902	. . . . . . . . . . 11 ⊢ Ⅎ𝑣𝐶
150		nfcsb1v 3919	. . . . . . . . . . 11 ⊢ Ⅎ𝑢⦋𝑣 / 𝑢⦌𝐶
151		csbeq1a 3908	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑣 → 𝐶 = ⦋𝑣 / 𝑢⦌𝐶)
152	149, 150, 151	cbvmpt 5260	. . . . . . . . . 10 ⊢ (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) = (𝑣 ∈ (𝑀(,)𝑁) ↦ ⦋𝑣 / 𝑢⦌𝐶)
153	152	fmpt 7112	. . . . . . . . 9 ⊢ (∀𝑣 ∈ (𝑀(,)𝑁)⦋𝑣 / 𝑢⦌𝐶 ∈ ℂ ↔ (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶):(𝑀(,)𝑁)⟶ℂ)
154	148, 153	sylibr 233	. . . . . . . 8 ⊢ (𝜑 → ∀𝑣 ∈ (𝑀(,)𝑁)⦋𝑣 / 𝑢⦌𝐶 ∈ ℂ)
155	154	r19.21bi 3247	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀(,)𝑁)) → ⦋𝑣 / 𝑢⦌𝐶 ∈ ℂ)
156	31, 5	sstri 3992	. . . . . . . . . 10 ⊢ (𝑍(,)𝑊) ⊆ ℂ
157		cncff 24634	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊)) → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑍(,)𝑊))
158	35, 157	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑍(,)𝑊))
159	158	fvmptelcdm 7115	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑍(,)𝑊))
160	156, 159	sselid 3981	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ ℂ)
161	6, 8, 160, 118, 117, 134	dvmptntr 25721	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐴)))
162		itgsubst.da	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵))
163	161, 162	eqtr3d 2773	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵))
164	122, 152	eqtrdi 2787	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑣 ∈ (𝑀(,)𝑁) ↦ ⦋𝑣 / 𝑢⦌𝐶))
165		csbeq1 3897	. . . . . . 7 ⊢ (𝑣 = 𝐴 → ⦋𝑣 / 𝑢⦌𝐶 = ⦋𝐴 / 𝑢⦌𝐶)
166	137, 137, 140, 147, 76, 155, 163, 164, 14, 165	dvmptco 25722	. . . . . 6 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (⦋𝐴 / 𝑢⦌𝐶 · 𝐵)))
167		nfcvd 2903	. . . . . . . . . 10 ⊢ (𝐴 ∈ (𝑀(,)𝑁) → Ⅎ𝑢𝐸)
168		itgsubst.e	. . . . . . . . . 10 ⊢ (𝑢 = 𝐴 → 𝐶 = 𝐸)
169	167, 168	csbiegf 3928	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝑀(,)𝑁) → ⦋𝐴 / 𝑢⦌𝐶 = 𝐸)
170	140, 169	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ⦋𝐴 / 𝑢⦌𝐶 = 𝐸)
171	170	oveq1d 7427	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (⦋𝐴 / 𝑢⦌𝐶 · 𝐵) = (𝐸 · 𝐵))
172	171	mpteq2dva 5249	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ (⦋𝐴 / 𝑢⦌𝐶 · 𝐵)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)))
173	135, 166, 172	3eqtrd 2775	. . . . 5 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)))
174		resmpt 6038	. . . . . . . 8 ⊢ ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸))
175	138, 174	ax-mp 5	. . . . . . 7 ⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)
176		eqidd 2732	. . . . . . . . . 10 ⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) = (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶))
177	159, 10, 176, 168	fmptco 7130	. . . . . . . . 9 ⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸))
178	35, 52	cncfco 24648	. . . . . . . . 9 ⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) ∈ ((𝑋[,]𝑌)–cn→ℂ))
179	177, 178	eqeltrrd 2833	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ))
180		rescncf 24638	. . . . . . . 8 ⊢ ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ)))
181	138, 179, 180	mpsyl 68	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
182	175, 181	eqeltrrid 2837	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ ((𝑋(,)𝑌)–cn→ℂ))
183	182, 144	mulcncf 25195	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
184	173, 183	eqeltrd 2832	. . . 4 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
185		ioombl 25315	. . . . . . . 8 ⊢ (𝑋(,)𝑌) ∈ dom vol
186	185	a1i 11	. . . . . . 7 ⊢ (𝜑 → (𝑋(,)𝑌) ∈ dom vol)
187		fco 6742	. . . . . . . . . . 11 ⊢ (((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶):(𝑍(,)𝑊)⟶ℂ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑍(,)𝑊)) → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)):(𝑋[,]𝑌)⟶ℂ)
188	54, 158, 187	syl2anc 583	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)):(𝑋[,]𝑌)⟶ℂ)
189	177	feq1d 6703	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)):(𝑋[,]𝑌)⟶ℂ ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸):(𝑋[,]𝑌)⟶ℂ))
190	188, 189	mpbid 231	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸):(𝑋[,]𝑌)⟶ℂ)
191	190	fvmptelcdm 7115	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐸 ∈ ℂ)
192	139, 191	sylan2 592	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐸 ∈ ℂ)
193		eqidd 2732	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸))
194		eqidd 2732	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵))
195	186, 192, 147, 193, 194	offval2 7693	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘_f · (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)))
196	173, 195	eqtr4d 2774	. . . . 5 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘_f · (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)))
197	138	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (𝑋(,)𝑌) ⊆ (𝑋[,]𝑌))
198		cniccibl 25591	. . . . . . . . 9 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ)) → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ 𝐿¹)
199	3, 4, 179, 198	syl3anc 1370	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ 𝐿¹)
200	197, 186, 191, 199	iblss 25555	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ 𝐿¹)
201		iblmbf 25518	. . . . . . 7 ⊢ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ 𝐿¹ → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ MblFn)
202	200, 201	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ MblFn)
203	143	simprd 495	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿¹)
204		cniccbdd 25211	. . . . . . . 8 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ)) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)
205	3, 4, 179, 204	syl3anc 1370	. . . . . . 7 ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)
206		ssralv 4051	. . . . . . . . . 10 ⊢ ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → (∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
207	138, 206	ax-mp 5	. . . . . . . . 9 ⊢ (∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)
208		eqid 2731	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)
209	208, 192	dmmptd 6696	. . . . . . . . . . 11 ⊢ (𝜑 → dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) = (𝑋(,)𝑌))
210	209	raleqdv 3324	. . . . . . . . . 10 ⊢ (𝜑 → (∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
211	175	fveq1i 6893	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌))‘𝑧) = ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)
212		fvres 6911	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (𝑋(,)𝑌) → (((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌))‘𝑧) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧))
213	211, 212	eqtr3id 2785	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝑋(,)𝑌) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧))
214	213	fveq2d 6896	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (𝑋(,)𝑌) → (abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) = (abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)))
215	214	breq1d 5159	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (𝑋(,)𝑌) → ((abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ (abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
216	215	ralbiia 3090	. . . . . . . . . 10 ⊢ (∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)
217	210, 216	bitr2di 287	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
218	207, 217	imbitrid 243	. . . . . . . 8 ⊢ (𝜑 → (∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
219	218	reximdv 3169	. . . . . . 7 ⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
220	205, 219	mpd 15	. . . . . 6 ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)
221		bddmulibl 25589	. . . . . 6 ⊢ (((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ MblFn ∧ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿¹ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘_f · (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) ∈ 𝐿¹)
222	202, 203, 220, 221	syl3anc 1370	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘_f · (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) ∈ 𝐿¹)
223	196, 222	eqeltrd 2832	. . . 4 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) ∈ 𝐿¹)
224	3, 4, 1, 184, 223, 129	ftc2 25794	. . 3 ⊢ (𝜑 → ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) d𝑡 = (((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) − ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋)))
225		fveq2 6892	. . . . 5 ⊢ (𝑡 = 𝑥 → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) = ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥))
226		nfcv 2902	. . . . . . 7 ⊢ Ⅎ𝑥ℝ
227		nfcv 2902	. . . . . . 7 ⊢ Ⅎ𝑥 D
228		nfmpt1 5257	. . . . . . 7 ⊢ Ⅎ𝑥(𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)
229	226, 227, 228	nfov 7442	. . . . . 6 ⊢ Ⅎ𝑥(ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))
230		nfcv 2902	. . . . . 6 ⊢ Ⅎ𝑥𝑡
231	229, 230	nffv 6902	. . . . 5 ⊢ Ⅎ𝑥((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡)
232		nfcv 2902	. . . . 5 ⊢ Ⅎ𝑡((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥)
233	225, 231, 232	cbvitg 25526	. . . 4 ⊢ ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) d𝑡 = ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) d𝑥
234	173	fveq1d 6894	. . . . . 6 ⊢ (𝜑 → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) = ((𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))‘𝑥))
235		ovex 7445	. . . . . . 7 ⊢ (𝐸 · 𝐵) ∈ V
236		eqid 2731	. . . . . . . 8 ⊢ (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))
237	236	fvmpt2 7010	. . . . . . 7 ⊢ ((𝑥 ∈ (𝑋(,)𝑌) ∧ (𝐸 · 𝐵) ∈ V) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))‘𝑥) = (𝐸 · 𝐵))
238	235, 237	mpan2 688	. . . . . 6 ⊢ (𝑥 ∈ (𝑋(,)𝑌) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))‘𝑥) = (𝐸 · 𝐵))
239	234, 238	sylan9eq 2791	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) = (𝐸 · 𝐵))
240	239	itgeq2dv 25532	. . . 4 ⊢ (𝜑 → ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) d𝑥 = ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥)
241	233, 240	eqtrid 2783	. . 3 ⊢ (𝜑 → ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) d𝑡 = ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥)
242	17, 9	sselid 3981	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑀[,]𝑁))
243		elicc2 13394	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝐴 ∈ (𝑀[,]𝑁) ↔ (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁)))
244	43, 40, 243	syl2anc 583	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 ∈ (𝑀[,]𝑁) ↔ (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁)))
245	244	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → (𝐴 ∈ (𝑀[,]𝑁) ↔ (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁)))
246	242, 245	mpbid 231	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁))
247	246	simp2d 1142	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝑀 ≤ 𝐴)
248	247	ditgpos 25606	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ∫(𝑀(,)𝐴)𝐶 d𝑢)
249	248	mpteq2dva 5249	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢) = (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))
250	249	fveq1d 6894	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑌) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌))
251		ubicc2 13447	. . . . . . . 8 ⊢ ((𝑋 ∈ ℝ^* ∧ 𝑌 ∈ ℝ^* ∧ 𝑋 ≤ 𝑌) → 𝑌 ∈ (𝑋[,]𝑌))
252	91, 92, 1, 251	syl3anc 1370	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ (𝑋[,]𝑌))
253		itgsubst.l	. . . . . . . . 9 ⊢ (𝑥 = 𝑌 → 𝐴 = 𝐿)
254		ditgeq2 25599	. . . . . . . . 9 ⊢ (𝐴 = 𝐿 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐿]𝐶 d𝑢)
255	253, 254	syl 17	. . . . . . . 8 ⊢ (𝑥 = 𝑌 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐿]𝐶 d𝑢)
256		eqid 2731	. . . . . . . 8 ⊢ (𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢) = (𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)
257		ditgex 25602	. . . . . . . 8 ⊢ ⨜[𝑀 → 𝐿]𝐶 d𝑢 ∈ V
258	255, 256, 257	fvmpt 6999	. . . . . . 7 ⊢ (𝑌 ∈ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑌) = ⨜[𝑀 → 𝐿]𝐶 d𝑢)
259	252, 258	syl 17	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑌) = ⨜[𝑀 → 𝐿]𝐶 d𝑢)
260	250, 259	eqtr3d 2773	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) = ⨜[𝑀 → 𝐿]𝐶 d𝑢)
261	249	fveq1d 6894	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑋) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋))
262		itgsubst.k	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → 𝐴 = 𝐾)
263		ditgeq2 25599	. . . . . . . . 9 ⊢ (𝐴 = 𝐾 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐾]𝐶 d𝑢)
264	262, 263	syl 17	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐾]𝐶 d𝑢)
265		ditgex 25602	. . . . . . . 8 ⊢ ⨜[𝑀 → 𝐾]𝐶 d𝑢 ∈ V
266	264, 256, 265	fvmpt 6999	. . . . . . 7 ⊢ (𝑋 ∈ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑋) = ⨜[𝑀 → 𝐾]𝐶 d𝑢)
267	94, 266	syl 17	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑋) = ⨜[𝑀 → 𝐾]𝐶 d𝑢)
268	261, 267	eqtr3d 2773	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋) = ⨜[𝑀 → 𝐾]𝐶 d𝑢)
269	260, 268	oveq12d 7430	. . . 4 ⊢ (𝜑 → (((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) − ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋)) = (⨜[𝑀 → 𝐿]𝐶 d𝑢 − ⨜[𝑀 → 𝐾]𝐶 d𝑢))
270		lbicc2 13446	. . . . . . 7 ⊢ ((𝑀 ∈ ℝ^* ∧ 𝑁 ∈ ℝ^* ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ (𝑀[,]𝑁))
271	103, 41, 109, 270	syl3anc 1370	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ (𝑀[,]𝑁))
272	262	eleq1d 2817	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (𝐴 ∈ (𝑀[,]𝑁) ↔ 𝐾 ∈ (𝑀[,]𝑁)))
273	242	ralrimiva 3145	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ (𝑋[,]𝑌)𝐴 ∈ (𝑀[,]𝑁))
274	272, 273, 94	rspcdva 3614	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ (𝑀[,]𝑁))
275	253	eleq1d 2817	. . . . . . 7 ⊢ (𝑥 = 𝑌 → (𝐴 ∈ (𝑀[,]𝑁) ↔ 𝐿 ∈ (𝑀[,]𝑁)))
276	275, 273, 252	rspcdva 3614	. . . . . 6 ⊢ (𝜑 → 𝐿 ∈ (𝑀[,]𝑁))
277	43, 40, 271, 274, 276, 56, 72	ditgsplit 25611	. . . . 5 ⊢ (𝜑 → ⨜[𝑀 → 𝐿]𝐶 d𝑢 = (⨜[𝑀 → 𝐾]𝐶 d𝑢 + ⨜[𝐾 → 𝐿]𝐶 d𝑢))
278	277	oveq1d 7427	. . . 4 ⊢ (𝜑 → (⨜[𝑀 → 𝐿]𝐶 d𝑢 − ⨜[𝑀 → 𝐾]𝐶 d𝑢) = ((⨜[𝑀 → 𝐾]𝐶 d𝑢 + ⨜[𝐾 → 𝐿]𝐶 d𝑢) − ⨜[𝑀 → 𝐾]𝐶 d𝑢))
279	43, 40, 271, 274, 56, 72	ditgcl 25608	. . . . 5 ⊢ (𝜑 → ⨜[𝑀 → 𝐾]𝐶 d𝑢 ∈ ℂ)
280	43, 40, 274, 276, 56, 72	ditgcl 25608	. . . . 5 ⊢ (𝜑 → ⨜[𝐾 → 𝐿]𝐶 d𝑢 ∈ ℂ)
281	279, 280	pncan2d 11578	. . . 4 ⊢ (𝜑 → ((⨜[𝑀 → 𝐾]𝐶 d𝑢 + ⨜[𝐾 → 𝐿]𝐶 d𝑢) − ⨜[𝑀 → 𝐾]𝐶 d𝑢) = ⨜[𝐾 → 𝐿]𝐶 d𝑢)
282	269, 278, 281	3eqtrd 2775	. . 3 ⊢ (𝜑 → (((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) − ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋)) = ⨜[𝐾 → 𝐿]𝐶 d𝑢)
283	224, 241, 282	3eqtr3d 2779	. 2 ⊢ (𝜑 → ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥 = ⨜[𝐾 → 𝐿]𝐶 d𝑢)
284	2, 283	eqtr2d 2772	1 ⊢ (𝜑 → ⨜[𝐾 → 𝐿]𝐶 d𝑢 = ⨜[𝑋 → 𝑌](𝐸 · 𝐵) d𝑥)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2105 ∀wral 3060 ∃wrex 3069 Vcvv 3473 ⦋csb 3894 ∩ cin 3948 ⊆ wss 3949 ∅c0 4323 {cpr 4631 class class class wbr 5149 ↦ cmpt 5232 dom cdm 5677 ran crn 5678 ↾ cres 5679 ∘ ccom 5681 ⟶wf 6540 ‘cfv 6544 (class class class)co 7412 ∘_f cof 7671 ℂcc 11111 ℝcr 11112 + caddc 11116 · cmul 11118 ℝ^*cxr 11252 < clt 11253 ≤ cle 11254 − cmin 11449 (,)cioo 13329 [,]cicc 13332 abscabs 15186 TopOpenctopn 17372 topGenctg 17388 ℂ_fldccnfld 21145 intcnt 22742 –cn→ccncf 24617 volcvol 25213 MblFncmbf 25364 𝐿¹cibl 25367 ∫citg 25368 ⨜cdit 25596 D cdv 25613

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 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7728 ax-inf2 9639 ax-cc 10433 ax-cnex 11169 ax-resscn 11170 ax-1cn 11171 ax-icn 11172 ax-addcl 11173 ax-addrcl 11174 ax-mulcl 11175 ax-mulrcl 11176 ax-mulcom 11177 ax-addass 11178 ax-mulass 11179 ax-distr 11180 ax-i2m1 11181 ax-1ne0 11182 ax-1rid 11183 ax-rnegex 11184 ax-rrecex 11185 ax-cnre 11186 ax-pre-lttri 11187 ax-pre-lttrn 11188 ax-pre-ltadd 11189 ax-pre-mulgt0 11190 ax-pre-sup 11191 ax-addf 11192 ax-mulf 11193

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3375 df-reu 3376 df-rab 3432 df-v 3475 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-symdif 4243 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-tp 4634 df-op 4636 df-uni 4910 df-int 4952 df-iun 5000 df-iin 5001 df-disj 5115 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-se 5633 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-isom 6553 df-riota 7368 df-ov 7415 df-oprab 7416 df-mpo 7417 df-of 7673 df-ofr 7674 df-om 7859 df-1st 7978 df-2nd 7979 df-supp 8150 df-frecs 8269 df-wrecs 8300 df-recs 8374 df-rdg 8413 df-1o 8469 df-2o 8470 df-oadd 8473 df-omul 8474 df-er 8706 df-map 8825 df-pm 8826 df-ixp 8895 df-en 8943 df-dom 8944 df-sdom 8945 df-fin 8946 df-fsupp 9365 df-fi 9409 df-sup 9440 df-inf 9441 df-oi 9508 df-dju 9899 df-card 9937 df-acn 9940 df-pnf 11255 df-mnf 11256 df-xr 11257 df-ltxr 11258 df-le 11259 df-sub 11451 df-neg 11452 df-div 11877 df-nn 12218 df-2 12280 df-3 12281 df-4 12282 df-5 12283 df-6 12284 df-7 12285 df-8 12286 df-9 12287 df-n0 12478 df-z 12564 df-dec 12683 df-uz 12828 df-q 12938 df-rp 12980 df-xneg 13097 df-xadd 13098 df-xmul 13099 df-ioo 13333 df-ioc 13334 df-ico 13335 df-icc 13336 df-fz 13490 df-fzo 13633 df-fl 13762 df-mod 13840 df-seq 13972 df-exp 14033 df-hash 14296 df-cj 15051 df-re 15052 df-im 15053 df-sqrt 15187 df-abs 15188 df-limsup 15420 df-clim 15437 df-rlim 15438 df-sum 15638 df-struct 17085 df-sets 17102 df-slot 17120 df-ndx 17132 df-base 17150 df-ress 17179 df-plusg 17215 df-mulr 17216 df-starv 17217 df-sca 17218 df-vsca 17219 df-ip 17220 df-tset 17221 df-ple 17222 df-ds 17224 df-unif 17225 df-hom 17226 df-cco 17227 df-rest 17373 df-topn 17374 df-0g 17392 df-gsum 17393 df-topgen 17394 df-pt 17395 df-prds 17398 df-xrs 17453 df-qtop 17458 df-imas 17459 df-xps 17461 df-mre 17535 df-mrc 17536 df-acs 17538 df-mgm 18566 df-sgrp 18645 df-mnd 18661 df-submnd 18707 df-mulg 18988 df-cntz 19223 df-cmn 19692 df-psmet 21137 df-xmet 21138 df-met 21139 df-bl 21140 df-mopn 21141 df-fbas 21142 df-fg 21143 df-cnfld 21146 df-top 22617 df-topon 22634 df-topsp 22656 df-bases 22670 df-cld 22744 df-ntr 22745 df-cls 22746 df-nei 22823 df-lp 22861 df-perf 22862 df-cn 22952 df-cnp 22953 df-haus 23040 df-cmp 23112 df-tx 23287 df-hmeo 23480 df-fil 23571 df-fm 23663 df-flim 23664 df-flf 23665 df-xms 24047 df-ms 24048 df-tms 24049 df-cncf 24619 df-ovol 25214 df-vol 25215 df-mbf 25369 df-itg1 25370 df-itg2 25371 df-ibl 25372 df-itg 25373 df-0p 25420 df-ditg 25597 df-limc 25616 df-dv 25617

This theorem is referenced by: itgsubst 25799

W3C validator