itgsubsticclem

	Ref	Expression
Hypotheses	itgsubsticclem.1	$⊢ F = (u \in [K, L] ⟼ C)$
	itgsubsticclem.2	$⊢ G = (u \in ℝ ⟼ if (u \in [K, L], F (u), if (u < K, F (K), F (L))))$
	itgsubsticclem.3	$⊢ φ \to X \in ℝ$
	itgsubsticclem.4	$⊢ φ \to Y \in ℝ$
	itgsubsticclem.5	$⊢ φ \to X \leq Y$
	itgsubsticclem.6	$⊢ φ \to (x \in [X, Y] ⟼ A) : [X, Y] \underset{cn}{⟶} [K, L]$
	itgsubsticclem.7	$⊢ φ \to (x \in (X, Y) ⟼ B) \in (((X, Y) \underset{cn}{⟶} ℂ) \cap 𝐿^{1})$
	itgsubsticclem.8	$⊢ φ \to F : [K, L] \underset{cn}{⟶} ℂ$
	itgsubsticclem.9	$⊢ φ \to K \in ℝ$
	itgsubsticclem.10	$⊢ φ \to L \in ℝ$
	itgsubsticclem.11	$⊢ φ \to K \leq L$
	itgsubsticclem.12	$⊢ φ \to \frac{d (x \in [X, Y]⟼ A)}{d_{ℝ} x} = (x \in (X, Y) ⟼ B)$
	itgsubsticclem.13	$⊢ u = A \to C = E$
	itgsubsticclem.14	$⊢ x = X \to A = K$
	itgsubsticclem.15	$⊢ x = Y \to A = L$
Assertion	itgsubsticclem	$⊢ φ \to \int_{K}^{L} C d u = \int_{X}^{Y} E B d x$

Proof

Step	Hyp	Ref	Expression
1		itgsubsticclem.1	$⊢ F = (u \in [K, L] ⟼ C)$
2		itgsubsticclem.2	$⊢ G = (u \in ℝ ⟼ if (u \in [K, L], F (u), if (u < K, F (K), F (L))))$
3		itgsubsticclem.3	$⊢ φ \to X \in ℝ$
4		itgsubsticclem.4	$⊢ φ \to Y \in ℝ$
5		itgsubsticclem.5	$⊢ φ \to X \leq Y$
6		itgsubsticclem.6	$⊢ φ \to (x \in [X, Y] ⟼ A) : [X, Y] \underset{cn}{⟶} [K, L]$
7		itgsubsticclem.7	$⊢ φ \to (x \in (X, Y) ⟼ B) \in (((X, Y) \underset{cn}{⟶} ℂ) \cap 𝐿^{1})$
8		itgsubsticclem.8	$⊢ φ \to F : [K, L] \underset{cn}{⟶} ℂ$
9		itgsubsticclem.9	$⊢ φ \to K \in ℝ$
10		itgsubsticclem.10	$⊢ φ \to L \in ℝ$
11		itgsubsticclem.11	$⊢ φ \to K \leq L$
12		itgsubsticclem.12	$⊢ φ \to \frac{d (x \in [X, Y]⟼ A)}{d_{ℝ} x} = (x \in (X, Y) ⟼ B)$
13		itgsubsticclem.13	$⊢ u = A \to C = E$
14		itgsubsticclem.14	$⊢ x = X \to A = K$
15		itgsubsticclem.15	$⊢ x = Y \to A = L$
16		fveq2	$⊢ u = w \to G (u) = G (w)$
17		nfcv	$⊢ \underline{Ⅎ} w G (u)$
18		nfmpt1	$⊢ \underline{Ⅎ} u (u \in ℝ ⟼ if (u \in [K, L], F (u), if (u < K, F (K), F (L))))$
19	2 18	nfcxfr	$⊢ \underline{Ⅎ} u G$
20		nfcv	$⊢ \underline{Ⅎ} u w$
21	19 20	nffv	$⊢ \underline{Ⅎ} u G (w)$
22	16 17 21	cbvditg	$⊢ \int_{K}^{L} G (u) d u = \int_{K}^{L} G (w) d w$
23	9 10	iccssred	$⊢ φ \to [K, L] \subseteq ℝ$
24	23	adantr	$⊢ (φ \land u \in (K, L)) \to [K, L] \subseteq ℝ$
25		ioossicc	$⊢ (K, L) \subseteq [K, L]$
26	25	sseli	$⊢ u \in (K, L) \to u \in [K, L]$
27	26	adantl	$⊢ (φ \land u \in (K, L)) \to u \in [K, L]$
28	24 27	sseldd	$⊢ (φ \land u \in (K, L)) \to u \in ℝ$
29	27	iftrued	$⊢ (φ \land u \in (K, L)) \to if (u \in [K, L], F (u), if (u < K, F (K), F (L))) = F (u)$
30	1	a1i	$⊢ φ \to F = (u \in [K, L] ⟼ C)$
31		cncff	$⊢ F : [K, L] \underset{cn}{⟶} ℂ \to F : [K, L] ⟶ ℂ$
32	8 31	syl	$⊢ φ \to F : [K, L] ⟶ ℂ$
33	30 32	feq1dd	$⊢ φ \to (u \in [K, L] ⟼ C) : [K, L] ⟶ ℂ$
34	33	fvmptelcdm	$⊢ (φ \land u \in [K, L]) \to C \in ℂ$
35	27 34	syldan	$⊢ (φ \land u \in (K, L)) \to C \in ℂ$
36	1	fvmpt2	$⊢ (u \in [K, L] \land C \in ℂ) \to F (u) = C$
37	27 35 36	syl2anc	$⊢ (φ \land u \in (K, L)) \to F (u) = C$
38	37 35	eqeltrd	$⊢ (φ \land u \in (K, L)) \to F (u) \in ℂ$
39	29 38	eqeltrd	$⊢ (φ \land u \in (K, L)) \to if (u \in [K, L], F (u), if (u < K, F (K), F (L))) \in ℂ$
40	2	fvmpt2	$⊢ (u \in ℝ \land if (u \in [K, L], F (u), if (u < K, F (K), F (L))) \in ℂ) \to G (u) = if (u \in [K, L], F (u), if (u < K, F (K), F (L)))$
41	28 39 40	syl2anc	$⊢ (φ \land u \in (K, L)) \to G (u) = if (u \in [K, L], F (u), if (u < K, F (K), F (L)))$
42	41 29 37	3eqtrd	$⊢ (φ \land u \in (K, L)) \to G (u) = C$
43	11 42	ditgeq3d	$⊢ φ \to \int_{K}^{L} G (u) d u = \int_{K}^{L} C d u$
44		mnfxr	$⊢ −∞ \in ℝ^{*}$
45	44	a1i	$⊢ φ \to −∞ \in ℝ^{*}$
46		pnfxr	$⊢ +∞ \in ℝ^{*}$
47	46	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
48		ioomax	$⊢ (−∞, +∞) = ℝ$
49	48	eqcomi	$⊢ ℝ = (−∞, +∞)$
50	49	a1i	$⊢ φ \to ℝ = (−∞, +∞)$
51	23 50	sseqtrd	$⊢ φ \to [K, L] \subseteq (−∞, +∞)$
52		ax-resscn	$⊢ ℝ \subseteq ℂ$
53	50 52	eqsstrrdi	$⊢ φ \to (−∞, +∞) \subseteq ℂ$
54		cncfss	$⊢ ([K, L] \subseteq (−∞, +∞) \land (−∞, +∞) \subseteq ℂ) \to [X, Y] \underset{cn}{⟶} [K, L] \subseteq [X, Y] \underset{cn}{⟶} (−∞, +∞)$
55	51 53 54	syl2anc	$⊢ φ \to [X, Y] \underset{cn}{⟶} [K, L] \subseteq [X, Y] \underset{cn}{⟶} (−∞, +∞)$
56	55 6	sseldd	$⊢ φ \to (x \in [X, Y] ⟼ A) : [X, Y] \underset{cn}{⟶} (−∞, +∞)$
57		nfmpt1	$⊢ \underline{Ⅎ} u (u \in [K, L] ⟼ C)$
58	1 57	nfcxfr	$⊢ \underline{Ⅎ} u F$
59		eqid	$⊢ topGen (ran (.)) = topGen (ran (.))$
60		eqid	$⊢ ⋃ TopOpen (ℂ_{fld}) = ⋃ TopOpen (ℂ_{fld})$
61		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
62	61	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
63	62	a1i	$⊢ φ \to TopOpen (ℂ_{fld}) \in Top$
64	23 52	sstrdi	$⊢ φ \to [K, L] \subseteq ℂ$
65		ssid	$⊢ ℂ \subseteq ℂ$
66		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} [K, L] = TopOpen (ℂ_{fld}) ↾_{𝑡} [K, L]$
67		unicntop	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
68	67	restid	$⊢ TopOpen (ℂ_{fld}) \in Top \to TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ = TopOpen (ℂ_{fld})$
69	62 68	ax-mp	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ = TopOpen (ℂ_{fld})$
70	69	eqcomi	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
71	61 66 70	cncfcn	$⊢ ([K, L] \subseteq ℂ \land ℂ \subseteq ℂ) \to [K, L] \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} [K, L]) Cn TopOpen (ℂ_{fld})$
72	64 65 71	sylancl	$⊢ φ \to [K, L] \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} [K, L]) Cn TopOpen (ℂ_{fld})$
73		reex	$⊢ ℝ \in V$
74	73	a1i	$⊢ φ \to ℝ \in V$
75		restabs	$⊢ (TopOpen (ℂ_{fld}) \in Top \land [K, L] \subseteq ℝ \land ℝ \in V) \to (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ↾_{𝑡} [K, L] = TopOpen (ℂ_{fld}) ↾_{𝑡} [K, L]$
76	63 23 74 75	syl3anc	$⊢ φ \to (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ↾_{𝑡} [K, L] = TopOpen (ℂ_{fld}) ↾_{𝑡} [K, L]$
77	61	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
78	77	eqcomi	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ = topGen (ran (.))$
79	78	a1i	$⊢ φ \to TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ = topGen (ran (.))$
80	79	oveq1d	$⊢ φ \to (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ↾_{𝑡} [K, L] = topGen (ran (.)) ↾_{𝑡} [K, L]$
81	76 80	eqtr3d	$⊢ φ \to TopOpen (ℂ_{fld}) ↾_{𝑡} [K, L] = topGen (ran (.)) ↾_{𝑡} [K, L]$
82	81	oveq1d	$⊢ φ \to (TopOpen (ℂ_{fld}) ↾_{𝑡} [K, L]) Cn TopOpen (ℂ_{fld}) = (topGen (ran (.)) ↾_{𝑡} [K, L]) Cn TopOpen (ℂ_{fld})$
83	72 82	eqtrd	$⊢ φ \to [K, L] \underset{cn}{⟶} ℂ = (topGen (ran (.)) ↾_{𝑡} [K, L]) Cn TopOpen (ℂ_{fld})$
84	8 83	eleqtrd	$⊢ φ \to F \in ((topGen (ran (.)) ↾_{𝑡} [K, L]) Cn TopOpen (ℂ_{fld}))$
85	58 59 60 2 9 10 11 63 84	icccncfext	$⊢ φ \to (G \in (topGen (ran (.)) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ran F)) \land {G ↾}_{[K, L]} = F)$
86	85	simpld	$⊢ φ \to G \in (topGen (ran (.)) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ran F))$
87		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
88		eqid	$⊢ ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} ran F) = ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} ran F)$
89	87 88	cnf	$⊢ G \in (topGen (ran (.)) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ran F)) \to G : ℝ ⟶ ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} ran F)$
90	86 89	syl	$⊢ φ \to G : ℝ ⟶ ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} ran F)$
91	50	feq2d	$⊢ φ \to (G : ℝ ⟶ ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} ran F) \leftrightarrow G : (−∞, +∞) ⟶ ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} ran F))$
92	90 91	mpbid	$⊢ φ \to G : (−∞, +∞) ⟶ ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} ran F)$
93	92	feqmptd	$⊢ φ \to G = (w \in (−∞, +∞) ⟼ G (w))$
94	32	frnd	$⊢ φ \to ran F \subseteq ℂ$
95		cncfss	$⊢ (ran F \subseteq ℂ \land ℂ \subseteq ℂ) \to (−∞, +∞) \underset{cn}{⟶} ran F \subseteq (−∞, +∞) \underset{cn}{⟶} ℂ$
96	94 65 95	sylancl	$⊢ φ \to (−∞, +∞) \underset{cn}{⟶} ran F \subseteq (−∞, +∞) \underset{cn}{⟶} ℂ$
97	49	oveq2i	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ = TopOpen (ℂ_{fld}) ↾_{𝑡} (−∞, +∞)$
98	77 97	eqtri	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} (−∞, +∞)$
99		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ran F = TopOpen (ℂ_{fld}) ↾_{𝑡} ran F$
100	61 98 99	cncfcn	$⊢ ((−∞, +∞) \subseteq ℂ \land ran F \subseteq ℂ) \to (−∞, +∞) \underset{cn}{⟶} ran F = topGen (ran (.)) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ran F)$
101	53 94 100	syl2anc	$⊢ φ \to (−∞, +∞) \underset{cn}{⟶} ran F = topGen (ran (.)) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ran F)$
102	101	eqcomd	$⊢ φ \to topGen (ran (.)) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ran F) = (−∞, +∞) \underset{cn}{⟶} ran F$
103	86 102	eleqtrd	$⊢ φ \to G : (−∞, +∞) \underset{cn}{⟶} ran F$
104	96 103	sseldd	$⊢ φ \to G : (−∞, +∞) \underset{cn}{⟶} ℂ$
105	93 104	eqeltrrd	$⊢ φ \to (w \in (−∞, +∞) ⟼ G (w)) : (−∞, +∞) \underset{cn}{⟶} ℂ$
106		fveq2	$⊢ w = A \to G (w) = G (A)$
107	3 4 5 45 47 56 7 105 12 106 14 15	itgsubst	$⊢ φ \to \int_{K}^{L} G (w) d w = \int_{X}^{Y} G (A) B d x$
108	22 43 107	3eqtr3a	$⊢ φ \to \int_{K}^{L} C d u = \int_{X}^{Y} G (A) B d x$
109	2	a1i	$⊢ (φ \land x \in (X, Y)) \to G = (u \in ℝ ⟼ if (u \in [K, L], F (u), if (u < K, F (K), F (L))))$
110		simpr	$⊢ ((φ \land x \in (X, Y)) \land u = A) \to u = A$
111	61	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
112	3 4	iccssred	$⊢ φ \to [X, Y] \subseteq ℝ$
113	112 52	sstrdi	$⊢ φ \to [X, Y] \subseteq ℂ$
114		resttopon	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land [X, Y] \subseteq ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} [X, Y] \in TopOn ([X, Y])$
115	111 113 114	sylancr	$⊢ φ \to TopOpen (ℂ_{fld}) ↾_{𝑡} [X, Y] \in TopOn ([X, Y])$
116		resttopon	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land [K, L] \subseteq ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} [K, L] \in TopOn ([K, L])$
117	111 64 116	sylancr	$⊢ φ \to TopOpen (ℂ_{fld}) ↾_{𝑡} [K, L] \in TopOn ([K, L])$
118		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} [X, Y] = TopOpen (ℂ_{fld}) ↾_{𝑡} [X, Y]$
119	61 118 66	cncfcn	$⊢ ([X, Y] \subseteq ℂ \land [K, L] \subseteq ℂ) \to [X, Y] \underset{cn}{⟶} [K, L] = (TopOpen (ℂ_{fld}) ↾_{𝑡} [X, Y]) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} [K, L])$
120	113 64 119	syl2anc	$⊢ φ \to [X, Y] \underset{cn}{⟶} [K, L] = (TopOpen (ℂ_{fld}) ↾_{𝑡} [X, Y]) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} [K, L])$
121	6 120	eleqtrd	$⊢ φ \to (x \in [X, Y] ⟼ A) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [X, Y]) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} [K, L]))$
122		cnf2	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} [X, Y] \in TopOn ([X, Y]) \land TopOpen (ℂ_{fld}) ↾_{𝑡} [K, L] \in TopOn ([K, L]) \land (x \in [X, Y] ⟼ A) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [X, Y]) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} [K, L]))) \to (x \in [X, Y] ⟼ A) : [X, Y] ⟶ [K, L]$
123	115 117 121 122	syl3anc	$⊢ φ \to (x \in [X, Y] ⟼ A) : [X, Y] ⟶ [K, L]$
124	123	adantr	$⊢ (φ \land x \in (X, Y)) \to (x \in [X, Y] ⟼ A) : [X, Y] ⟶ [K, L]$
125		eqid	$⊢ (x \in [X, Y] ⟼ A) = (x \in [X, Y] ⟼ A)$
126	125	fmpt	$⊢ \forall x \in [X, Y] A \in [K, L] \leftrightarrow (x \in [X, Y] ⟼ A) : [X, Y] ⟶ [K, L]$
127	124 126	sylibr	$⊢ (φ \land x \in (X, Y)) \to \forall x \in [X, Y] A \in [K, L]$
128		ioossicc	$⊢ (X, Y) \subseteq [X, Y]$
129	128	sseli	$⊢ x \in (X, Y) \to x \in [X, Y]$
130	129	adantl	$⊢ (φ \land x \in (X, Y)) \to x \in [X, Y]$
131		rsp	$⊢ \forall x \in [X, Y] A \in [K, L] \to (x \in [X, Y] \to A \in [K, L])$
132	127 130 131	sylc	$⊢ (φ \land x \in (X, Y)) \to A \in [K, L]$
133	132	adantr	$⊢ ((φ \land x \in (X, Y)) \land u = A) \to A \in [K, L]$
134	110 133	eqeltrd	$⊢ ((φ \land x \in (X, Y)) \land u = A) \to u \in [K, L]$
135	134	iftrued	$⊢ ((φ \land x \in (X, Y)) \land u = A) \to if (u \in [K, L], F (u), if (u < K, F (K), F (L))) = F (u)$
136		simpll	$⊢ ((φ \land x \in (X, Y)) \land u = A) \to φ$
137	136 134 34	syl2anc	$⊢ ((φ \land x \in (X, Y)) \land u = A) \to C \in ℂ$
138	134 137 36	syl2anc	$⊢ ((φ \land x \in (X, Y)) \land u = A) \to F (u) = C$
139	13	adantl	$⊢ ((φ \land x \in (X, Y)) \land u = A) \to C = E$
140	135 138 139	3eqtrd	$⊢ ((φ \land x \in (X, Y)) \land u = A) \to if (u \in [K, L], F (u), if (u < K, F (K), F (L))) = E$
141	23	adantr	$⊢ (φ \land x \in (X, Y)) \to [K, L] \subseteq ℝ$
142	141 132	sseldd	$⊢ (φ \land x \in (X, Y)) \to A \in ℝ$
143		elex	$⊢ A \in [K, L] \to A \in V$
144	132 143	syl	$⊢ (φ \land x \in (X, Y)) \to A \in V$
145		isset	$⊢ A \in V \leftrightarrow \exists u u = A$
146	144 145	sylib	$⊢ (φ \land x \in (X, Y)) \to \exists u u = A$
147	139 137	eqeltrrd	$⊢ ((φ \land x \in (X, Y)) \land u = A) \to E \in ℂ$
148	146 147	exlimddv	$⊢ (φ \land x \in (X, Y)) \to E \in ℂ$
149	109 140 142 148	fvmptd	$⊢ (φ \land x \in (X, Y)) \to G (A) = E$
150	149	oveq1d	$⊢ (φ \land x \in (X, Y)) \to G (A) B = E B$
151	5 150	ditgeq3d	$⊢ φ \to \int_{X}^{Y} G (A) B d x = \int_{X}^{Y} E B d x$
152	108 151	eqtrd	$⊢ φ \to \int_{K}^{L} C d u = \int_{X}^{Y} E B d x$

Metamath Proof Explorer

Theorem itgsubsticclem

Proof