itgsubstlem

	Ref	Expression
Hypotheses	itgsubst.x	$⊢ φ \to X \in ℝ$
	itgsubst.y	$⊢ φ \to Y \in ℝ$
	itgsubst.le	$⊢ φ \to X \leq Y$
	itgsubst.z	$⊢ φ \to Z \in ℝ^{*}$
	itgsubst.w	$⊢ φ \to W \in ℝ^{*}$
	itgsubst.a	$⊢ φ \to (x \in [X, Y] ⟼ A) : [X, Y] \underset{cn}{⟶} (Z, W)$
	itgsubst.b	$⊢ φ \to (x \in (X, Y) ⟼ B) \in (((X, Y) \underset{cn}{⟶} ℂ) \cap 𝐿^{1})$
	itgsubst.c	$⊢ φ \to (u \in (Z, W) ⟼ C) : (Z, W) \underset{cn}{⟶} ℂ$
	itgsubst.da	$⊢ φ \to \frac{d (x \in [X, Y]⟼ A)}{d_{ℝ} x} = (x \in (X, Y) ⟼ B)$
	itgsubst.e	$⊢ u = A \to C = E$
	itgsubst.k	$⊢ x = X \to A = K$
	itgsubst.l	$⊢ x = Y \to A = L$
	itgsubst.m	$⊢ φ \to M \in (Z, W)$
	itgsubst.n	$⊢ φ \to N \in (Z, W)$
	itgsubst.cl2	$⊢ (φ \land x \in [X, Y]) \to A \in (M, N)$
Assertion	itgsubstlem	$⊢ φ \to \int_{K}^{L} C d u = \int_{X}^{Y} E B d x$

Proof

Step	Hyp	Ref	Expression
1		itgsubst.x	$⊢ φ \to X \in ℝ$
2		itgsubst.y	$⊢ φ \to Y \in ℝ$
3		itgsubst.le	$⊢ φ \to X \leq Y$
4		itgsubst.z	$⊢ φ \to Z \in ℝ^{*}$
5		itgsubst.w	$⊢ φ \to W \in ℝ^{*}$
6		itgsubst.a	$⊢ φ \to (x \in [X, Y] ⟼ A) : [X, Y] \underset{cn}{⟶} (Z, W)$
7		itgsubst.b	$⊢ φ \to (x \in (X, Y) ⟼ B) \in (((X, Y) \underset{cn}{⟶} ℂ) \cap 𝐿^{1})$
8		itgsubst.c	$⊢ φ \to (u \in (Z, W) ⟼ C) : (Z, W) \underset{cn}{⟶} ℂ$
9		itgsubst.da	$⊢ φ \to \frac{d (x \in [X, Y]⟼ A)}{d_{ℝ} x} = (x \in (X, Y) ⟼ B)$
10		itgsubst.e	$⊢ u = A \to C = E$
11		itgsubst.k	$⊢ x = X \to A = K$
12		itgsubst.l	$⊢ x = Y \to A = L$
13		itgsubst.m	$⊢ φ \to M \in (Z, W)$
14		itgsubst.n	$⊢ φ \to N \in (Z, W)$
15		itgsubst.cl2	$⊢ (φ \land x \in [X, Y]) \to A \in (M, N)$
16	3	ditgpos	$⊢ φ \to \int_{X}^{Y} E B d x = \int_{(X, Y)} E B d x$
17		ax-resscn	$⊢ ℝ \subseteq ℂ$
18	17	a1i	$⊢ φ \to ℝ \subseteq ℂ$
19		iccssre	$⊢ (X \in ℝ \land Y \in ℝ) \to [X, Y] \subseteq ℝ$
20	1 2 19	syl2anc	$⊢ φ \to [X, Y] \subseteq ℝ$
21		eqidd	$⊢ φ \to (x \in [X, Y] ⟼ A) = (x \in [X, Y] ⟼ A)$
22		eqidd	$⊢ φ \to (v \in (M, N) ⟼ \int_{(M, v)} C d u) = (v \in (M, N) ⟼ \int_{(M, v)} C d u)$
23		oveq2	$⊢ v = A \to (M, v) = (M, A)$
24		itgeq1	$⊢ (M, v) = (M, A) \to \int_{(M, v)} C d u = \int_{(M, A)} C d u$
25	23 24	syl	$⊢ v = A \to \int_{(M, v)} C d u = \int_{(M, A)} C d u$
26	15 21 22 25	fmptco	$⊢ φ \to (v \in (M, N) ⟼ \int_{(M, v)} C d u) \circ (x \in [X, Y] ⟼ A) = (x \in [X, Y] ⟼ \int_{(M, A)} C d u)$
27	15	fmpttd	$⊢ φ \to (x \in [X, Y] ⟼ A) : [X, Y] ⟶ (M, N)$
28		ioossicc	$⊢ (M, N) \subseteq [M, N]$
29		eliooord	$⊢ M \in (Z, W) \to (Z < M \land M < W)$
30	13 29	syl	$⊢ φ \to (Z < M \land M < W)$
31	30	simpld	$⊢ φ \to Z < M$
32		eliooord	$⊢ N \in (Z, W) \to (Z < N \land N < W)$
33	14 32	syl	$⊢ φ \to (Z < N \land N < W)$
34	33	simprd	$⊢ φ \to N < W$
35		iccssioo	$⊢ ((Z \in ℝ^{} \land W \in ℝ^{}) \land (Z < M \land N < W)) \to [M, N] \subseteq (Z, W)$
36	4 5 31 34 35	syl22anc	$⊢ φ \to [M, N] \subseteq (Z, W)$
37	28 36	sstrid	$⊢ φ \to (M, N) \subseteq (Z, W)$
38		ioossre	$⊢ (Z, W) \subseteq ℝ$
39	38	a1i	$⊢ φ \to (Z, W) \subseteq ℝ$
40	39 17	sstrdi	$⊢ φ \to (Z, W) \subseteq ℂ$
41	37 40	sstrd	$⊢ φ \to (M, N) \subseteq ℂ$
42		cncffvrn	$⊢ ((M, N) \subseteq ℂ \land (x \in [X, Y] ⟼ A) : [X, Y] \underset{cn}{⟶} (Z, W)) \to ((x \in [X, Y] ⟼ A) : [X, Y] \underset{cn}{⟶} (M, N) \leftrightarrow (x \in [X, Y] ⟼ A) : [X, Y] ⟶ (M, N))$
43	41 6 42	syl2anc	$⊢ φ \to ((x \in [X, Y] ⟼ A) : [X, Y] \underset{cn}{⟶} (M, N) \leftrightarrow (x \in [X, Y] ⟼ A) : [X, Y] ⟶ (M, N))$
44	27 43	mpbird	$⊢ φ \to (x \in [X, Y] ⟼ A) : [X, Y] \underset{cn}{⟶} (M, N)$
45	28	sseli	$⊢ v \in (M, N) \to v \in [M, N]$
46	38 14	sseldi	$⊢ φ \to N \in ℝ$
47	46	rexrd	$⊢ φ \to N \in ℝ^{*}$
48	47	adantr	$⊢ (φ \land v \in [M, N]) \to N \in ℝ^{*}$
49	38 13	sseldi	$⊢ φ \to M \in ℝ$
50		elicc2	$⊢ (M \in ℝ \land N \in ℝ) \to (v \in [M, N] \leftrightarrow (v \in ℝ \land M \leq v \land v \leq N))$
51	49 46 50	syl2anc	$⊢ φ \to (v \in [M, N] \leftrightarrow (v \in ℝ \land M \leq v \land v \leq N))$
52	51	biimpa	$⊢ (φ \land v \in [M, N]) \to (v \in ℝ \land M \leq v \land v \leq N)$
53	52	simp3d	$⊢ (φ \land v \in [M, N]) \to v \leq N$
54		iooss2	$⊢ (N \in ℝ^{*} \land v \leq N) \to (M, v) \subseteq (M, N)$
55	48 53 54	syl2anc	$⊢ (φ \land v \in [M, N]) \to (M, v) \subseteq (M, N)$
56	55	sselda	$⊢ ((φ \land v \in [M, N]) \land u \in (M, v)) \to u \in (M, N)$
57	37	sselda	$⊢ (φ \land u \in (M, N)) \to u \in (Z, W)$
58		cncff	$⊢ (u \in (Z, W) ⟼ C) : (Z, W) \underset{cn}{⟶} ℂ \to (u \in (Z, W) ⟼ C) : (Z, W) ⟶ ℂ$
59	8 58	syl	$⊢ φ \to (u \in (Z, W) ⟼ C) : (Z, W) ⟶ ℂ$
60	59	fvmptelrn	$⊢ (φ \land u \in (Z, W)) \to C \in ℂ$
61	57 60	syldan	$⊢ (φ \land u \in (M, N)) \to C \in ℂ$
62	61	adantlr	$⊢ ((φ \land v \in [M, N]) \land u \in (M, N)) \to C \in ℂ$
63	56 62	syldan	$⊢ ((φ \land v \in [M, N]) \land u \in (M, v)) \to C \in ℂ$
64		ioombl	$⊢ (M, v) \in dom vol$
65	64	a1i	$⊢ (φ \land v \in [M, N]) \to (M, v) \in dom vol$
66	28	a1i	$⊢ φ \to (M, N) \subseteq [M, N]$
67		ioombl	$⊢ (M, N) \in dom vol$
68	67	a1i	$⊢ φ \to (M, N) \in dom vol$
69	36	sselda	$⊢ (φ \land u \in [M, N]) \to u \in (Z, W)$
70	69 60	syldan	$⊢ (φ \land u \in [M, N]) \to C \in ℂ$
71	36	resmptd	$⊢ φ \to {(u \in (Z, W) ⟼ C) ↾}_{[M, N]} = (u \in [M, N] ⟼ C)$
72		rescncf	$⊢ [M, N] \subseteq (Z, W) \to ((u \in (Z, W) ⟼ C) : (Z, W) \underset{cn}{⟶} ℂ \to ({(u \in (Z, W) ⟼ C) ↾}_{[M, N]}) : [M, N] \underset{cn}{⟶} ℂ)$
73	36 8 72	sylc	$⊢ φ \to ({(u \in (Z, W) ⟼ C) ↾}_{[M, N]}) : [M, N] \underset{cn}{⟶} ℂ$
74	71 73	eqeltrrd	$⊢ φ \to (u \in [M, N] ⟼ C) : [M, N] \underset{cn}{⟶} ℂ$
75		cniccibl	$⊢ (M \in ℝ \land N \in ℝ \land (u \in [M, N] ⟼ C) : [M, N] \underset{cn}{⟶} ℂ) \to (u \in [M, N] ⟼ C) \in 𝐿^{1}$
76	49 46 74 75	syl3anc	$⊢ φ \to (u \in [M, N] ⟼ C) \in 𝐿^{1}$
77	66 68 70 76	iblss	$⊢ φ \to (u \in (M, N) ⟼ C) \in 𝐿^{1}$
78	77	adantr	$⊢ (φ \land v \in [M, N]) \to (u \in (M, N) ⟼ C) \in 𝐿^{1}$
79	55 65 62 78	iblss	$⊢ (φ \land v \in [M, N]) \to (u \in (M, v) ⟼ C) \in 𝐿^{1}$
80	63 79	itgcl	$⊢ (φ \land v \in [M, N]) \to \int_{(M, v)} C d u \in ℂ$
81	45 80	sylan2	$⊢ (φ \land v \in (M, N)) \to \int_{(M, v)} C d u \in ℂ$
82	81	fmpttd	$⊢ φ \to (v \in (M, N) ⟼ \int_{(M, v)} C d u) : (M, N) ⟶ ℂ$
83	37 38	sstrdi	$⊢ φ \to (M, N) \subseteq ℝ$
84		fveq2	$⊢ t = u \to (u \in (M, N) ⟼ C) (t) = (u \in (M, N) ⟼ C) (u)$
85		nffvmpt1	$⊢ \underline{Ⅎ} u (u \in (M, N) ⟼ C) (t)$
86		nfcv	$⊢ \underline{Ⅎ} t (u \in (M, N) ⟼ C) (u)$
87	84 85 86	cbvitg	$⊢ \int_{(M, v)} (u \in (M, N) ⟼ C) (t) d t = \int_{(M, v)} (u \in (M, N) ⟼ C) (u) d u$
88		eqid	$⊢ (u \in (M, N) ⟼ C) = (u \in (M, N) ⟼ C)$
89	88	fvmpt2	$⊢ (u \in (M, N) \land C \in ℂ) \to (u \in (M, N) ⟼ C) (u) = C$
90	56 63 89	syl2anc	$⊢ ((φ \land v \in [M, N]) \land u \in (M, v)) \to (u \in (M, N) ⟼ C) (u) = C$
91	90	itgeq2dv	$⊢ (φ \land v \in [M, N]) \to \int_{(M, v)} (u \in (M, N) ⟼ C) (u) d u = \int_{(M, v)} C d u$
92	87 91	syl5eq	$⊢ (φ \land v \in [M, N]) \to \int_{(M, v)} (u \in (M, N) ⟼ C) (t) d t = \int_{(M, v)} C d u$
93	92	mpteq2dva	$⊢ φ \to (v \in [M, N] ⟼ \int_{(M, v)} (u \in (M, N) ⟼ C) (t) d t) = (v \in [M, N] ⟼ \int_{(M, v)} C d u)$
94	93	oveq2d	$⊢ φ \to \frac{d (v \in [M, N]⟼ \int_{(M, v)} (u \in (M, N) ⟼ C) (t) d t)}{d_{ℝ} v} = \frac{d (v \in [M, N]⟼ \int_{(M, v)} C d u)}{d_{ℝ} v}$
95		eqid	$⊢ (v \in [M, N] ⟼ \int_{(M, v)} (u \in (M, N) ⟼ C) (t) d t) = (v \in [M, N] ⟼ \int_{(M, v)} (u \in (M, N) ⟼ C) (t) d t)$
96	1	rexrd	$⊢ φ \to X \in ℝ^{*}$
97	2	rexrd	$⊢ φ \to Y \in ℝ^{*}$
98		lbicc2	$⊢ (X \in ℝ^{} \land Y \in ℝ^{} \land X \leq Y) \to X \in [X, Y]$
99	96 97 3 98	syl3anc	$⊢ φ \to X \in [X, Y]$
100		n0i	$⊢ X \in [X, Y] \to \neg [X, Y] = \emptyset$
101	99 100	syl	$⊢ φ \to \neg [X, Y] = \emptyset$
102		feq3	$⊢ (M, N) = \emptyset \to ((x \in [X, Y] ⟼ A) : [X, Y] ⟶ (M, N) \leftrightarrow (x \in [X, Y] ⟼ A) : [X, Y] ⟶ \emptyset)$
103	27 102	syl5ibcom	$⊢ φ \to ((M, N) = \emptyset \to (x \in [X, Y] ⟼ A) : [X, Y] ⟶ \emptyset)$
104		f00	$⊢ (x \in [X, Y] ⟼ A) : [X, Y] ⟶ \emptyset \leftrightarrow ((x \in [X, Y] ⟼ A) = \emptyset \land [X, Y] = \emptyset)$
105	104	simprbi	$⊢ (x \in [X, Y] ⟼ A) : [X, Y] ⟶ \emptyset \to [X, Y] = \emptyset$
106	103 105	syl6	$⊢ φ \to ((M, N) = \emptyset \to [X, Y] = \emptyset)$
107	101 106	mtod	$⊢ φ \to \neg (M, N) = \emptyset$
108	49	rexrd	$⊢ φ \to M \in ℝ^{*}$
109		ioo0	$⊢ (M \in ℝ^{} \land N \in ℝ^{}) \to ((M, N) = \emptyset \leftrightarrow N \leq M)$
110	108 47 109	syl2anc	$⊢ φ \to ((M, N) = \emptyset \leftrightarrow N \leq M)$
111	107 110	mtbid	$⊢ φ \to \neg N \leq M$
112	46 49	letrid	$⊢ φ \to (N \leq M \lor M \leq N)$
113	112	ord	$⊢ φ \to (\neg N \leq M \to M \leq N)$
114	111 113	mpd	$⊢ φ \to M \leq N$
115		resmpt	$⊢ (M, N) \subseteq [M, N] \to {(u \in [M, N] ⟼ C) ↾}_{(M, N)} = (u \in (M, N) ⟼ C)$
116	28 115	ax-mp	$⊢ {(u \in [M, N] ⟼ C) ↾}_{(M, N)} = (u \in (M, N) ⟼ C)$
117		rescncf	$⊢ (M, N) \subseteq [M, N] \to ((u \in [M, N] ⟼ C) : [M, N] \underset{cn}{⟶} ℂ \to ({(u \in [M, N] ⟼ C) ↾}_{(M, N)}) : (M, N) \underset{cn}{⟶} ℂ)$
118	28 74 117	mpsyl	$⊢ φ \to ({(u \in [M, N] ⟼ C) ↾}_{(M, N)}) : (M, N) \underset{cn}{⟶} ℂ$
119	116 118	eqeltrrid	$⊢ φ \to (u \in (M, N) ⟼ C) : (M, N) \underset{cn}{⟶} ℂ$
120	95 49 46 114 119 77	ftc1cn	$⊢ φ \to \frac{d (v \in [M, N]⟼ \int_{(M, v)} (u \in (M, N) ⟼ C) (t) d t)}{d_{ℝ} v} = (u \in (M, N) ⟼ C)$
121	36 38	sstrdi	$⊢ φ \to [M, N] \subseteq ℝ$
122		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
123	122	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
124		iccntr	$⊢ (M \in ℝ \land N \in ℝ) \to int (topGen (ran (.))) ([M, N]) = (M, N)$
125	49 46 124	syl2anc	$⊢ φ \to int (topGen (ran (.))) ([M, N]) = (M, N)$
126	18 121 80 123 122 125	dvmptntr	$⊢ φ \to \frac{d (v \in [M, N]⟼ \int_{(M, v)} C d u)}{d_{ℝ} v} = \frac{d (v \in (M, N)⟼ \int_{(M, v)} C d u)}{d_{ℝ} v}$
127	94 120 126	3eqtr3rd	$⊢ φ \to \frac{d (v \in (M, N)⟼ \int_{(M, v)} C d u)}{d_{ℝ} v} = (u \in (M, N) ⟼ C)$
128	127	dmeqd	$⊢ φ \to dom \frac{d (v \in (M, N)⟼ \int_{(M, v)} C d u)}{d_{ℝ} v} = dom (u \in (M, N) ⟼ C)$
129	88 61	dmmptd	$⊢ φ \to dom (u \in (M, N) ⟼ C) = (M, N)$
130	128 129	eqtrd	$⊢ φ \to dom \frac{d (v \in (M, N)⟼ \int_{(M, v)} C d u)}{d_{ℝ} v} = (M, N)$
131		dvcn	$⊢ ((ℝ \subseteq ℂ \land (v \in (M, N) ⟼ \int_{(M, v)} C d u) : (M, N) ⟶ ℂ \land (M, N) \subseteq ℝ) \land dom \frac{d (v \in (M, N)⟼ \int_{(M, v)} C d u)}{d_{ℝ} v} = (M, N)) \to (v \in (M, N) ⟼ \int_{(M, v)} C d u) : (M, N) \underset{cn}{⟶} ℂ$
132	18 82 83 130 131	syl31anc	$⊢ φ \to (v \in (M, N) ⟼ \int_{(M, v)} C d u) : (M, N) \underset{cn}{⟶} ℂ$
133	44 132	cncfco	$⊢ φ \to ((v \in (M, N) ⟼ \int_{(M, v)} C d u) \circ (x \in [X, Y] ⟼ A)) : [X, Y] \underset{cn}{⟶} ℂ$
134	26 133	eqeltrrd	$⊢ φ \to (x \in [X, Y] ⟼ \int_{(M, A)} C d u) : [X, Y] \underset{cn}{⟶} ℂ$
135		cncff	$⊢ (x \in [X, Y] ⟼ \int_{(M, A)} C d u) : [X, Y] \underset{cn}{⟶} ℂ \to (x \in [X, Y] ⟼ \int_{(M, A)} C d u) : [X, Y] ⟶ ℂ$
136	134 135	syl	$⊢ φ \to (x \in [X, Y] ⟼ \int_{(M, A)} C d u) : [X, Y] ⟶ ℂ$
137	136	fvmptelrn	$⊢ (φ \land x \in [X, Y]) \to \int_{(M, A)} C d u \in ℂ$
138		iccntr	$⊢ (X \in ℝ \land Y \in ℝ) \to int (topGen (ran (.))) ([X, Y]) = (X, Y)$
139	1 2 138	syl2anc	$⊢ φ \to int (topGen (ran (.))) ([X, Y]) = (X, Y)$
140	18 20 137 123 122 139	dvmptntr	$⊢ φ \to \frac{d (x \in [X, Y]⟼ \int_{(M, A)} C d u)}{d_{ℝ} x} = \frac{d (x \in (X, Y)⟼ \int_{(M, A)} C d u)}{d_{ℝ} x}$
141		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
142	141	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
143		ioossicc	$⊢ (X, Y) \subseteq [X, Y]$
144	143	sseli	$⊢ x \in (X, Y) \to x \in [X, Y]$
145	144 15	sylan2	$⊢ (φ \land x \in (X, Y)) \to A \in (M, N)$
146		elin	$⊢ (x \in (X, Y) ⟼ B) \in (((X, Y) \underset{cn}{⟶} ℂ) \cap 𝐿^{1}) \leftrightarrow ((x \in (X, Y) ⟼ B) : (X, Y) \underset{cn}{⟶} ℂ \land (x \in (X, Y) ⟼ B) \in 𝐿^{1})$
147	7 146	sylib	$⊢ φ \to ((x \in (X, Y) ⟼ B) : (X, Y) \underset{cn}{⟶} ℂ \land (x \in (X, Y) ⟼ B) \in 𝐿^{1})$
148	147	simpld	$⊢ φ \to (x \in (X, Y) ⟼ B) : (X, Y) \underset{cn}{⟶} ℂ$
149		cncff	$⊢ (x \in (X, Y) ⟼ B) : (X, Y) \underset{cn}{⟶} ℂ \to (x \in (X, Y) ⟼ B) : (X, Y) ⟶ ℂ$
150	148 149	syl	$⊢ φ \to (x \in (X, Y) ⟼ B) : (X, Y) ⟶ ℂ$
151	150	fvmptelrn	$⊢ (φ \land x \in (X, Y)) \to B \in ℂ$
152	61	fmpttd	$⊢ φ \to (u \in (M, N) ⟼ C) : (M, N) ⟶ ℂ$
153		nfcv	$⊢ \underline{Ⅎ} v C$
154		nfcsb1v	$⊢ \underline{Ⅎ} u ⦋ v / u ⦌ C$
155		csbeq1a	$⊢ u = v \to C = ⦋ v / u ⦌ C$
156	153 154 155	cbvmpt	$⊢ (u \in (M, N) ⟼ C) = (v \in (M, N) ⟼ ⦋ v / u ⦌ C)$
157	156	fmpt	$⊢ \forall v \in (M, N) ⦋ v / u ⦌ C \in ℂ \leftrightarrow (u \in (M, N) ⟼ C) : (M, N) ⟶ ℂ$
158	152 157	sylibr	$⊢ φ \to \forall v \in (M, N) ⦋ v / u ⦌ C \in ℂ$
159	158	r19.21bi	$⊢ (φ \land v \in (M, N)) \to ⦋ v / u ⦌ C \in ℂ$
160	38 17	sstri	$⊢ (Z, W) \subseteq ℂ$
161		cncff	$⊢ (x \in [X, Y] ⟼ A) : [X, Y] \underset{cn}{⟶} (Z, W) \to (x \in [X, Y] ⟼ A) : [X, Y] ⟶ (Z, W)$
162	6 161	syl	$⊢ φ \to (x \in [X, Y] ⟼ A) : [X, Y] ⟶ (Z, W)$
163	162	fvmptelrn	$⊢ (φ \land x \in [X, Y]) \to A \in (Z, W)$
164	160 163	sseldi	$⊢ (φ \land x \in [X, Y]) \to A \in ℂ$
165	18 20 164 123 122 139	dvmptntr	$⊢ φ \to \frac{d (x \in [X, Y]⟼ A)}{d_{ℝ} x} = \frac{d (x \in (X, Y)⟼ A)}{d_{ℝ} x}$
166	165 9	eqtr3d	$⊢ φ \to \frac{d (x \in (X, Y)⟼ A)}{d_{ℝ} x} = (x \in (X, Y) ⟼ B)$
167	127 156	syl6eq	$⊢ φ \to \frac{d (v \in (M, N)⟼ \int_{(M, v)} C d u)}{d_{ℝ} v} = (v \in (M, N) ⟼ ⦋ v / u ⦌ C)$
168		csbeq1	$⊢ v = A \to ⦋ v / u ⦌ C = ⦋ A / u ⦌ C$
169	142 142 145 151 81 159 166 167 25 168	dvmptco	$⊢ φ \to \frac{d (x \in (X, Y)⟼ \int_{(M, A)} C d u)}{d_{ℝ} x} = (x \in (X, Y) ⟼ ⦋ A / u ⦌ C B)$
170		nfcvd	$⊢ A \in (M, N) \to \underline{Ⅎ} u E$
171	170 10	csbiegf	$⊢ A \in (M, N) \to ⦋ A / u ⦌ C = E$
172	145 171	syl	$⊢ (φ \land x \in (X, Y)) \to ⦋ A / u ⦌ C = E$
173	172	oveq1d	$⊢ (φ \land x \in (X, Y)) \to ⦋ A / u ⦌ C B = E B$
174	173	mpteq2dva	$⊢ φ \to (x \in (X, Y) ⟼ ⦋ A / u ⦌ C B) = (x \in (X, Y) ⟼ E B)$
175	140 169 174	3eqtrd	$⊢ φ \to \frac{d (x \in [X, Y]⟼ \int_{(M, A)} C d u)}{d_{ℝ} x} = (x \in (X, Y) ⟼ E B)$
176		resmpt	$⊢ (X, Y) \subseteq [X, Y] \to {(x \in [X, Y] ⟼ E) ↾}_{(X, Y)} = (x \in (X, Y) ⟼ E)$
177	143 176	ax-mp	$⊢ {(x \in [X, Y] ⟼ E) ↾}_{(X, Y)} = (x \in (X, Y) ⟼ E)$
178		eqidd	$⊢ φ \to (u \in (Z, W) ⟼ C) = (u \in (Z, W) ⟼ C)$
179	163 21 178 10	fmptco	$⊢ φ \to (u \in (Z, W) ⟼ C) \circ (x \in [X, Y] ⟼ A) = (x \in [X, Y] ⟼ E)$
180	6 8	cncfco	$⊢ φ \to ((u \in (Z, W) ⟼ C) \circ (x \in [X, Y] ⟼ A)) : [X, Y] \underset{cn}{⟶} ℂ$
181	179 180	eqeltrrd	$⊢ φ \to (x \in [X, Y] ⟼ E) : [X, Y] \underset{cn}{⟶} ℂ$
182		rescncf	$⊢ (X, Y) \subseteq [X, Y] \to ((x \in [X, Y] ⟼ E) : [X, Y] \underset{cn}{⟶} ℂ \to ({(x \in [X, Y] ⟼ E) ↾}_{(X, Y)}) : (X, Y) \underset{cn}{⟶} ℂ)$
183	143 181 182	mpsyl	$⊢ φ \to ({(x \in [X, Y] ⟼ E) ↾}_{(X, Y)}) : (X, Y) \underset{cn}{⟶} ℂ$
184	177 183	eqeltrrid	$⊢ φ \to (x \in (X, Y) ⟼ E) : (X, Y) \underset{cn}{⟶} ℂ$
185	184 148	mulcncf	$⊢ φ \to (x \in (X, Y) ⟼ E B) : (X, Y) \underset{cn}{⟶} ℂ$
186	175 185	eqeltrd	$⊢ φ \to \frac{d (x \in [X, Y]⟼ \int_{(M, A)} C d u)}{d_{ℝ} x} : (X, Y) \underset{cn}{⟶} ℂ$
187		ioombl	$⊢ (X, Y) \in dom vol$
188	187	a1i	$⊢ φ \to (X, Y) \in dom vol$
189		fco	$⊢ ((u \in (Z, W) ⟼ C) : (Z, W) ⟶ ℂ \land (x \in [X, Y] ⟼ A) : [X, Y] ⟶ (Z, W)) \to ((u \in (Z, W) ⟼ C) \circ (x \in [X, Y] ⟼ A)) : [X, Y] ⟶ ℂ$
190	59 162 189	syl2anc	$⊢ φ \to ((u \in (Z, W) ⟼ C) \circ (x \in [X, Y] ⟼ A)) : [X, Y] ⟶ ℂ$
191	179	feq1d	$⊢ φ \to (((u \in (Z, W) ⟼ C) \circ (x \in [X, Y] ⟼ A)) : [X, Y] ⟶ ℂ \leftrightarrow (x \in [X, Y] ⟼ E) : [X, Y] ⟶ ℂ)$
192	190 191	mpbid	$⊢ φ \to (x \in [X, Y] ⟼ E) : [X, Y] ⟶ ℂ$
193	192	fvmptelrn	$⊢ (φ \land x \in [X, Y]) \to E \in ℂ$
194	144 193	sylan2	$⊢ (φ \land x \in (X, Y)) \to E \in ℂ$
195		eqidd	$⊢ φ \to (x \in (X, Y) ⟼ E) = (x \in (X, Y) ⟼ E)$
196		eqidd	$⊢ φ \to (x \in (X, Y) ⟼ B) = (x \in (X, Y) ⟼ B)$
197	188 194 151 195 196	offval2	$⊢ φ \to (x \in (X, Y) ⟼ E) \times_{f} (x \in (X, Y) ⟼ B) = (x \in (X, Y) ⟼ E B)$
198	175 197	eqtr4d	$⊢ φ \to \frac{d (x \in [X, Y]⟼ \int_{(M, A)} C d u)}{d_{ℝ} x} = (x \in (X, Y) ⟼ E) \times_{f} (x \in (X, Y) ⟼ B)$
199	143	a1i	$⊢ φ \to (X, Y) \subseteq [X, Y]$
200		cniccibl	$⊢ (X \in ℝ \land Y \in ℝ \land (x \in [X, Y] ⟼ E) : [X, Y] \underset{cn}{⟶} ℂ) \to (x \in [X, Y] ⟼ E) \in 𝐿^{1}$
201	1 2 181 200	syl3anc	$⊢ φ \to (x \in [X, Y] ⟼ E) \in 𝐿^{1}$
202	199 188 193 201	iblss	$⊢ φ \to (x \in (X, Y) ⟼ E) \in 𝐿^{1}$
203		iblmbf	$⊢ (x \in (X, Y) ⟼ E) \in 𝐿^{1} \to (x \in (X, Y) ⟼ E) \in MblFn$
204	202 203	syl	$⊢ φ \to (x \in (X, Y) ⟼ E) \in MblFn$
205	147	simprd	$⊢ φ \to (x \in (X, Y) ⟼ B) \in 𝐿^{1}$
206		cniccbdd	$⊢ (X \in ℝ \land Y \in ℝ \land (x \in [X, Y] ⟼ E) : [X, Y] \underset{cn}{⟶} ℂ) \to \exists y \in ℝ \forall z \in [X, Y] \|(x \in [X, Y] ⟼ E) (z)\| \leq y$
207	1 2 181 206	syl3anc	$⊢ φ \to \exists y \in ℝ \forall z \in [X, Y] \|(x \in [X, Y] ⟼ E) (z)\| \leq y$
208		ssralv	$⊢ (X, Y) \subseteq [X, Y] \to (\forall z \in [X, Y] \|(x \in [X, Y] ⟼ E) (z)\| \leq y \to \forall z \in (X, Y) \|(x \in [X, Y] ⟼ E) (z)\| \leq y)$
209	143 208	ax-mp	$⊢ \forall z \in [X, Y] \|(x \in [X, Y] ⟼ E) (z)\| \leq y \to \forall z \in (X, Y) \|(x \in [X, Y] ⟼ E) (z)\| \leq y$
210		eqid	$⊢ (x \in (X, Y) ⟼ E) = (x \in (X, Y) ⟼ E)$
211	210 194	dmmptd	$⊢ φ \to dom (x \in (X, Y) ⟼ E) = (X, Y)$
212	211	raleqdv	$⊢ φ \to (\forall z \in dom (x \in (X, Y) ⟼ E) \|(x \in (X, Y) ⟼ E) (z)\| \leq y \leftrightarrow \forall z \in (X, Y) \|(x \in (X, Y) ⟼ E) (z)\| \leq y)$
213	177	fveq1i	$⊢ ({(x \in [X, Y] ⟼ E) ↾}_{(X, Y)}) (z) = (x \in (X, Y) ⟼ E) (z)$
214		fvres	$⊢ z \in (X, Y) \to ({(x \in [X, Y] ⟼ E) ↾}_{(X, Y)}) (z) = (x \in [X, Y] ⟼ E) (z)$
215	213 214	syl5eqr	$⊢ z \in (X, Y) \to (x \in (X, Y) ⟼ E) (z) = (x \in [X, Y] ⟼ E) (z)$
216	215	fveq2d	$⊢ z \in (X, Y) \to \|(x \in (X, Y) ⟼ E) (z)\| = \|(x \in [X, Y] ⟼ E) (z)\|$
217	216	breq1d	$⊢ z \in (X, Y) \to (\|(x \in (X, Y) ⟼ E) (z)\| \leq y \leftrightarrow \|(x \in [X, Y] ⟼ E) (z)\| \leq y)$
218	217	ralbiia	$⊢ \forall z \in (X, Y) \|(x \in (X, Y) ⟼ E) (z)\| \leq y \leftrightarrow \forall z \in (X, Y) \|(x \in [X, Y] ⟼ E) (z)\| \leq y$
219	212 218	syl6rbb	$⊢ φ \to (\forall z \in (X, Y) \|(x \in [X, Y] ⟼ E) (z)\| \leq y \leftrightarrow \forall z \in dom (x \in (X, Y) ⟼ E) \|(x \in (X, Y) ⟼ E) (z)\| \leq y)$
220	209 219	syl5ib	$⊢ φ \to (\forall z \in [X, Y] \|(x \in [X, Y] ⟼ E) (z)\| \leq y \to \forall z \in dom (x \in (X, Y) ⟼ E) \|(x \in (X, Y) ⟼ E) (z)\| \leq y)$
221	220	reximdv	$⊢ φ \to (\exists y \in ℝ \forall z \in [X, Y] \|(x \in [X, Y] ⟼ E) (z)\| \leq y \to \exists y \in ℝ \forall z \in dom (x \in (X, Y) ⟼ E) \|(x \in (X, Y) ⟼ E) (z)\| \leq y)$
222	207 221	mpd	$⊢ φ \to \exists y \in ℝ \forall z \in dom (x \in (X, Y) ⟼ E) \|(x \in (X, Y) ⟼ E) (z)\| \leq y$
223		bddmulibl	$⊢ ((x \in (X, Y) ⟼ E) \in MblFn \land (x \in (X, Y) ⟼ B) \in 𝐿^{1} \land \exists y \in ℝ \forall z \in dom (x \in (X, Y) ⟼ E) \|(x \in (X, Y) ⟼ E) (z)\| \leq y) \to (x \in (X, Y) ⟼ E) \times_{f} (x \in (X, Y) ⟼ B) \in 𝐿^{1}$
224	204 205 222 223	syl3anc	$⊢ φ \to (x \in (X, Y) ⟼ E) \times_{f} (x \in (X, Y) ⟼ B) \in 𝐿^{1}$
225	198 224	eqeltrd	$⊢ φ \to \frac{d (x \in [X, Y]⟼ \int_{(M, A)} C d u)}{d_{ℝ} x} \in 𝐿^{1}$
226	1 2 3 186 225 134	ftc2	$⊢ φ \to \int_{(X, Y)} \frac{d (x \in [X, Y]⟼ \int_{(M, A)} C d u)}{d_{ℝ} x} (t) d t = (x \in [X, Y] ⟼ \int_{(M, A)} C d u) (Y) - (x \in [X, Y] ⟼ \int_{(M, A)} C d u) (X)$
227		fveq2	$⊢ t = x \to \frac{d (x \in [X, Y]⟼ \int_{(M, A)} C d u)}{d_{ℝ} x} (t) = \frac{d (x \in [X, Y]⟼ \int_{(M, A)} C d u)}{d_{ℝ} x} (x)$
228		nfcv	$⊢ \underline{Ⅎ} x ℝ$
229		nfcv	$⊢ \underline{Ⅎ} x D$
230		nfmpt1	$⊢ \underline{Ⅎ} x (x \in [X, Y] ⟼ \int_{(M, A)} C d u)$
231	228 229 230	nfov	$⊢ \underline{Ⅎ} x \frac{d (x \in [X, Y]⟼ \int_{(M, A)} C d u)}{d_{ℝ} x}$
232		nfcv	$⊢ \underline{Ⅎ} x t$
233	231 232	nffv	$⊢ \underline{Ⅎ} x \frac{d (x \in [X, Y]⟼ \int_{(M, A)} C d u)}{d_{ℝ} x} (t)$
234		nfcv	$⊢ \underline{Ⅎ} t \frac{d (x \in [X, Y]⟼ \int_{(M, A)} C d u)}{d_{ℝ} x} (x)$
235	227 233 234	cbvitg	$⊢ \int_{(X, Y)} \frac{d (x \in [X, Y]⟼ \int_{(M, A)} C d u)}{d_{ℝ} x} (t) d t = \int_{(X, Y)} \frac{d (x \in [X, Y]⟼ \int_{(M, A)} C d u)}{d_{ℝ} x} (x) d x$
236	175	fveq1d	$⊢ φ \to \frac{d (x \in [X, Y]⟼ \int_{(M, A)} C d u)}{d_{ℝ} x} (x) = (x \in (X, Y) ⟼ E B) (x)$
237		ovex	$⊢ E B \in V$
238		eqid	$⊢ (x \in (X, Y) ⟼ E B) = (x \in (X, Y) ⟼ E B)$
239	238	fvmpt2	$⊢ (x \in (X, Y) \land E B \in V) \to (x \in (X, Y) ⟼ E B) (x) = E B$
240	237 239	mpan2	$⊢ x \in (X, Y) \to (x \in (X, Y) ⟼ E B) (x) = E B$
241	236 240	sylan9eq	$⊢ (φ \land x \in (X, Y)) \to \frac{d (x \in [X, Y]⟼ \int_{(M, A)} C d u)}{d_{ℝ} x} (x) = E B$
242	241	itgeq2dv	$⊢ φ \to \int_{(X, Y)} \frac{d (x \in [X, Y]⟼ \int_{(M, A)} C d u)}{d_{ℝ} x} (x) d x = \int_{(X, Y)} E B d x$
243	235 242	syl5eq	$⊢ φ \to \int_{(X, Y)} \frac{d (x \in [X, Y]⟼ \int_{(M, A)} C d u)}{d_{ℝ} x} (t) d t = \int_{(X, Y)} E B d x$
244	28 15	sseldi	$⊢ (φ \land x \in [X, Y]) \to A \in [M, N]$
245		elicc2	$⊢ (M \in ℝ \land N \in ℝ) \to (A \in [M, N] \leftrightarrow (A \in ℝ \land M \leq A \land A \leq N))$
246	49 46 245	syl2anc	$⊢ φ \to (A \in [M, N] \leftrightarrow (A \in ℝ \land M \leq A \land A \leq N))$
247	246	adantr	$⊢ (φ \land x \in [X, Y]) \to (A \in [M, N] \leftrightarrow (A \in ℝ \land M \leq A \land A \leq N))$
248	244 247	mpbid	$⊢ (φ \land x \in [X, Y]) \to (A \in ℝ \land M \leq A \land A \leq N)$
249	248	simp2d	$⊢ (φ \land x \in [X, Y]) \to M \leq A$
250	249	ditgpos	$⊢ (φ \land x \in [X, Y]) \to \int_{M}^{A} C d u = \int_{(M, A)} C d u$
251	250	mpteq2dva	$⊢ φ \to (x \in [X, Y] ⟼ \int_{M}^{A} C d u) = (x \in [X, Y] ⟼ \int_{(M, A)} C d u)$
252	251	fveq1d	$⊢ φ \to (x \in [X, Y] ⟼ \int_{M}^{A} C d u) (Y) = (x \in [X, Y] ⟼ \int_{(M, A)} C d u) (Y)$
253		ubicc2	$⊢ (X \in ℝ^{} \land Y \in ℝ^{} \land X \leq Y) \to Y \in [X, Y]$
254	96 97 3 253	syl3anc	$⊢ φ \to Y \in [X, Y]$
255		ditgeq2	$⊢ A = L \to \int_{M}^{A} C d u = \int_{M}^{L} C d u$
256	12 255	syl	$⊢ x = Y \to \int_{M}^{A} C d u = \int_{M}^{L} C d u$
257		eqid	$⊢ (x \in [X, Y] ⟼ \int_{M}^{A} C d u) = (x \in [X, Y] ⟼ \int_{M}^{A} C d u)$
258		ditgex	$⊢ \int_{M}^{L} C d u \in V$
259	256 257 258	fvmpt	$⊢ Y \in [X, Y] \to (x \in [X, Y] ⟼ \int_{M}^{A} C d u) (Y) = \int_{M}^{L} C d u$
260	254 259	syl	$⊢ φ \to (x \in [X, Y] ⟼ \int_{M}^{A} C d u) (Y) = \int_{M}^{L} C d u$
261	252 260	eqtr3d	$⊢ φ \to (x \in [X, Y] ⟼ \int_{(M, A)} C d u) (Y) = \int_{M}^{L} C d u$
262	251	fveq1d	$⊢ φ \to (x \in [X, Y] ⟼ \int_{M}^{A} C d u) (X) = (x \in [X, Y] ⟼ \int_{(M, A)} C d u) (X)$
263		ditgeq2	$⊢ A = K \to \int_{M}^{A} C d u = \int_{M}^{K} C d u$
264	11 263	syl	$⊢ x = X \to \int_{M}^{A} C d u = \int_{M}^{K} C d u$
265		ditgex	$⊢ \int_{M}^{K} C d u \in V$
266	264 257 265	fvmpt	$⊢ X \in [X, Y] \to (x \in [X, Y] ⟼ \int_{M}^{A} C d u) (X) = \int_{M}^{K} C d u$
267	99 266	syl	$⊢ φ \to (x \in [X, Y] ⟼ \int_{M}^{A} C d u) (X) = \int_{M}^{K} C d u$
268	262 267	eqtr3d	$⊢ φ \to (x \in [X, Y] ⟼ \int_{(M, A)} C d u) (X) = \int_{M}^{K} C d u$
269	261 268	oveq12d	$⊢ φ \to (x \in [X, Y] ⟼ \int_{(M, A)} C d u) (Y) - (x \in [X, Y] ⟼ \int_{(M, A)} C d u) (X) = \int_{M}^{L} C d u - \int_{M}^{K} C d u$
270		lbicc2	$⊢ (M \in ℝ^{} \land N \in ℝ^{} \land M \leq N) \to M \in [M, N]$
271	108 47 114 270	syl3anc	$⊢ φ \to M \in [M, N]$
272	11	eleq1d	$⊢ x = X \to (A \in [M, N] \leftrightarrow K \in [M, N])$
273	244	ralrimiva	$⊢ φ \to \forall x \in [X, Y] A \in [M, N]$
274	272 273 99	rspcdva	$⊢ φ \to K \in [M, N]$
275	12	eleq1d	$⊢ x = Y \to (A \in [M, N] \leftrightarrow L \in [M, N])$
276	275 273 254	rspcdva	$⊢ φ \to L \in [M, N]$
277	49 46 271 274 276 61 77	ditgsplit	$⊢ φ \to \int_{M}^{L} C d u = \int_{M}^{K} C d u + \int_{K}^{L} C d u$
278	277	oveq1d	$⊢ φ \to \int_{M}^{L} C d u - \int_{M}^{K} C d u = \int_{M}^{K} C d u + \int_{K}^{L} C d u - \int_{M}^{K} C d u$
279	49 46 271 274 61 77	ditgcl	$⊢ φ \to \int_{M}^{K} C d u \in ℂ$
280	49 46 274 276 61 77	ditgcl	$⊢ φ \to \int_{K}^{L} C d u \in ℂ$
281	279 280	pncan2d	$⊢ φ \to \int_{M}^{K} C d u + \int_{K}^{L} C d u - \int_{M}^{K} C d u = \int_{K}^{L} C d u$
282	269 278 281	3eqtrd	$⊢ φ \to (x \in [X, Y] ⟼ \int_{(M, A)} C d u) (Y) - (x \in [X, Y] ⟼ \int_{(M, A)} C d u) (X) = \int_{K}^{L} C d u$
283	226 243 282	3eqtr3d	$⊢ φ \to \int_{(X, Y)} E B d x = \int_{K}^{L} C d u$
284	16 283	eqtr2d	$⊢ φ \to \int_{K}^{L} C d u = \int_{X}^{Y} E B d x$

Metamath Proof Explorer

Theorem itgsubstlem

Proof