itgsbtaddcnst

Description: Integral substitution, adding a constant to the function's argument. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	itgsbtaddcnst.a	$⊢ φ \to A \in ℝ$
	itgsbtaddcnst.b	$⊢ φ \to B \in ℝ$
	itgsbtaddcnst.aleb	$⊢ φ \to A \leq B$
	itgsbtaddcnst.x	$⊢ φ \to X \in ℝ$
	itgsbtaddcnst.f	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℂ$
Assertion	itgsbtaddcnst	$⊢ φ \to \int_{(A - X)}^{(B - X)} F (X + s) d s = \int_{A}^{B} F (t) d t$

Proof

Step	Hyp	Ref	Expression
1		itgsbtaddcnst.a	$⊢ φ \to A \in ℝ$
2		itgsbtaddcnst.b	$⊢ φ \to B \in ℝ$
3		itgsbtaddcnst.aleb	$⊢ φ \to A \leq B$
4		itgsbtaddcnst.x	$⊢ φ \to X \in ℝ$
5		itgsbtaddcnst.f	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℂ$
6	1 2	iccssred	$⊢ φ \to [A, B] \subseteq ℝ$
7	6	sselda	$⊢ (φ \land t \in [A, B]) \to t \in ℝ$
8	7	recnd	$⊢ (φ \land t \in [A, B]) \to t \in ℂ$
9	4	recnd	$⊢ φ \to X \in ℂ$
10	9	adantr	$⊢ (φ \land t \in [A, B]) \to X \in ℂ$
11	8 10	negsubd	$⊢ (φ \land t \in [A, B]) \to t + (- X) = t - X$
12	11	eqcomd	$⊢ (φ \land t \in [A, B]) \to t - X = t + (- X)$
13	12	mpteq2dva	$⊢ φ \to (t \in [A, B] ⟼ t - X) = (t \in [A, B] ⟼ t + (- X))$
14	1	adantr	$⊢ (φ \land t \in [A, B]) \to A \in ℝ$
15	4	adantr	$⊢ (φ \land t \in [A, B]) \to X \in ℝ$
16	14 15	resubcld	$⊢ (φ \land t \in [A, B]) \to A - X \in ℝ$
17	2	adantr	$⊢ (φ \land t \in [A, B]) \to B \in ℝ$
18	17 15	resubcld	$⊢ (φ \land t \in [A, B]) \to B - X \in ℝ$
19	7 15	resubcld	$⊢ (φ \land t \in [A, B]) \to t - X \in ℝ$
20		simpr	$⊢ (φ \land t \in [A, B]) \to t \in [A, B]$
21	1 2	jca	$⊢ φ \to (A \in ℝ \land B \in ℝ)$
22	21	adantr	$⊢ (φ \land t \in [A, B]) \to (A \in ℝ \land B \in ℝ)$
23		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (t \in [A, B] \leftrightarrow (t \in ℝ \land A \leq t \land t \leq B))$
24	22 23	syl	$⊢ (φ \land t \in [A, B]) \to (t \in [A, B] \leftrightarrow (t \in ℝ \land A \leq t \land t \leq B))$
25	20 24	mpbid	$⊢ (φ \land t \in [A, B]) \to (t \in ℝ \land A \leq t \land t \leq B)$
26	25	simp2d	$⊢ (φ \land t \in [A, B]) \to A \leq t$
27	14 7 15 26	lesub1dd	$⊢ (φ \land t \in [A, B]) \to A - X \leq t - X$
28	25	simp3d	$⊢ (φ \land t \in [A, B]) \to t \leq B$
29	7 17 15 28	lesub1dd	$⊢ (φ \land t \in [A, B]) \to t - X \leq B - X$
30	16 18 19 27 29	eliccd	$⊢ (φ \land t \in [A, B]) \to t - X \in [A - X, B - X]$
31	30	fmpttd	$⊢ φ \to (t \in [A, B] ⟼ t - X) : [A, B] ⟶ [A - X, B - X]$
32	13 31	feq1dd	$⊢ φ \to (t \in [A, B] ⟼ t + (- X)) : [A, B] ⟶ [A - X, B - X]$
33	1 4	resubcld	$⊢ φ \to A - X \in ℝ$
34	2 4	resubcld	$⊢ φ \to B - X \in ℝ$
35	33 34	iccssred	$⊢ φ \to [A - X, B - X] \subseteq ℝ$
36		ax-resscn	$⊢ ℝ \subseteq ℂ$
37	35 36	sstrdi	$⊢ φ \to [A - X, B - X] \subseteq ℂ$
38	6 36	sstrdi	$⊢ φ \to [A, B] \subseteq ℂ$
39	38	resmptd	$⊢ φ \to {(t \in ℂ ⟼ t - X) ↾}_{[A, B]} = (t \in [A, B] ⟼ t - X)$
40		ssid	$⊢ ℂ \subseteq ℂ$
41		cncfmptid	$⊢ (ℂ \subseteq ℂ \land ℂ \subseteq ℂ) \to (t \in ℂ ⟼ t) : ℂ \underset{cn}{⟶} ℂ$
42	40 40 41	mp2an	$⊢ (t \in ℂ ⟼ t) : ℂ \underset{cn}{⟶} ℂ$
43	42	a1i	$⊢ X \in ℂ \to (t \in ℂ ⟼ t) : ℂ \underset{cn}{⟶} ℂ$
44	40	a1i	$⊢ X \in ℂ \to ℂ \subseteq ℂ$
45		id	$⊢ X \in ℂ \to X \in ℂ$
46	44 45 44	constcncfg	$⊢ X \in ℂ \to (t \in ℂ ⟼ X) : ℂ \underset{cn}{⟶} ℂ$
47	43 46	subcncf	$⊢ X \in ℂ \to (t \in ℂ ⟼ t - X) : ℂ \underset{cn}{⟶} ℂ$
48	9 47	syl	$⊢ φ \to (t \in ℂ ⟼ t - X) : ℂ \underset{cn}{⟶} ℂ$
49		rescncf	$⊢ [A, B] \subseteq ℂ \to ((t \in ℂ ⟼ t - X) : ℂ \underset{cn}{⟶} ℂ \to ({(t \in ℂ ⟼ t - X) ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℂ)$
50	38 48 49	sylc	$⊢ φ \to ({(t \in ℂ ⟼ t - X) ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℂ$
51	39 50	eqeltrrd	$⊢ φ \to (t \in [A, B] ⟼ t - X) : [A, B] \underset{cn}{⟶} ℂ$
52	13 51	eqeltrrd	$⊢ φ \to (t \in [A, B] ⟼ t + (- X)) : [A, B] \underset{cn}{⟶} ℂ$
53		cncffvrn	$⊢ ([A - X, B - X] \subseteq ℂ \land (t \in [A, B] ⟼ t + (- X)) : [A, B] \underset{cn}{⟶} ℂ) \to ((t \in [A, B] ⟼ t + (- X)) : [A, B] \underset{cn}{⟶} [A - X, B - X] \leftrightarrow (t \in [A, B] ⟼ t + (- X)) : [A, B] ⟶ [A - X, B - X])$
54	37 52 53	syl2anc	$⊢ φ \to ((t \in [A, B] ⟼ t + (- X)) : [A, B] \underset{cn}{⟶} [A - X, B - X] \leftrightarrow (t \in [A, B] ⟼ t + (- X)) : [A, B] ⟶ [A - X, B - X])$
55	32 54	mpbird	$⊢ φ \to (t \in [A, B] ⟼ t + (- X)) : [A, B] \underset{cn}{⟶} [A - X, B - X]$
56	13 55	eqeltrd	$⊢ φ \to (t \in [A, B] ⟼ t - X) : [A, B] \underset{cn}{⟶} [A - X, B - X]$
57		eqid	$⊢ (s \in ℂ ⟼ X + s) = (s \in ℂ ⟼ X + s)$
58	9	adantr	$⊢ (φ \land s \in ℂ) \to X \in ℂ$
59		simpr	$⊢ (φ \land s \in ℂ) \to s \in ℂ$
60	58 59	addcomd	$⊢ (φ \land s \in ℂ) \to X + s = s + X$
61	60	mpteq2dva	$⊢ φ \to (s \in ℂ ⟼ X + s) = (s \in ℂ ⟼ s + X)$
62		eqid	$⊢ (s \in ℂ ⟼ s + X) = (s \in ℂ ⟼ s + X)$
63	62	addccncf	$⊢ X \in ℂ \to (s \in ℂ ⟼ s + X) : ℂ \underset{cn}{⟶} ℂ$
64	9 63	syl	$⊢ φ \to (s \in ℂ ⟼ s + X) : ℂ \underset{cn}{⟶} ℂ$
65	61 64	eqeltrd	$⊢ φ \to (s \in ℂ ⟼ X + s) : ℂ \underset{cn}{⟶} ℂ$
66	1	adantr	$⊢ (φ \land s \in [A - X, B - X]) \to A \in ℝ$
67	2	adantr	$⊢ (φ \land s \in [A - X, B - X]) \to B \in ℝ$
68	4	adantr	$⊢ (φ \land s \in [A - X, B - X]) \to X \in ℝ$
69	35	sselda	$⊢ (φ \land s \in [A - X, B - X]) \to s \in ℝ$
70	68 69	readdcld	$⊢ (φ \land s \in [A - X, B - X]) \to X + s \in ℝ$
71		simpr	$⊢ (φ \land s \in [A - X, B - X]) \to s \in [A - X, B - X]$
72	33	adantr	$⊢ (φ \land s \in [A - X, B - X]) \to A - X \in ℝ$
73	34	adantr	$⊢ (φ \land s \in [A - X, B - X]) \to B - X \in ℝ$
74		elicc2	$⊢ (A - X \in ℝ \land B - X \in ℝ) \to (s \in [A - X, B - X] \leftrightarrow (s \in ℝ \land A - X \leq s \land s \leq B - X))$
75	72 73 74	syl2anc	$⊢ (φ \land s \in [A - X, B - X]) \to (s \in [A - X, B - X] \leftrightarrow (s \in ℝ \land A - X \leq s \land s \leq B - X))$
76	71 75	mpbid	$⊢ (φ \land s \in [A - X, B - X]) \to (s \in ℝ \land A - X \leq s \land s \leq B - X)$
77	76	simp2d	$⊢ (φ \land s \in [A - X, B - X]) \to A - X \leq s$
78	66 68 69	lesubadd2d	$⊢ (φ \land s \in [A - X, B - X]) \to (A - X \leq s \leftrightarrow A \leq X + s)$
79	77 78	mpbid	$⊢ (φ \land s \in [A - X, B - X]) \to A \leq X + s$
80	76	simp3d	$⊢ (φ \land s \in [A - X, B - X]) \to s \leq B - X$
81	68 69 67	leaddsub2d	$⊢ (φ \land s \in [A - X, B - X]) \to (X + s \leq B \leftrightarrow s \leq B - X)$
82	80 81	mpbird	$⊢ (φ \land s \in [A - X, B - X]) \to X + s \leq B$
83	66 67 70 79 82	eliccd	$⊢ (φ \land s \in [A - X, B - X]) \to X + s \in [A, B]$
84	57 65 37 38 83	cncfmptssg	$⊢ φ \to (s \in [A - X, B - X] ⟼ X + s) : [A - X, B - X] \underset{cn}{⟶} [A, B]$
85	84 5	cncfcompt	$⊢ φ \to (s \in [A - X, B - X] ⟼ F (X + s)) : [A - X, B - X] \underset{cn}{⟶} ℂ$
86		ax-1cn	$⊢ 1 \in ℂ$
87		ioosscn	$⊢ (A, B) \subseteq ℂ$
88		cncfmptc	$⊢ (1 \in ℂ \land (A, B) \subseteq ℂ \land ℂ \subseteq ℂ) \to (t \in (A, B) ⟼ 1) : (A, B) \underset{cn}{⟶} ℂ$
89	86 87 40 88	mp3an	$⊢ (t \in (A, B) ⟼ 1) : (A, B) \underset{cn}{⟶} ℂ$
90	89	a1i	$⊢ φ \to (t \in (A, B) ⟼ 1) : (A, B) \underset{cn}{⟶} ℂ$
91		fconstmpt	$⊢ (A, B) \times \{1\} = (t \in (A, B) ⟼ 1)$
92		ioombl	$⊢ (A, B) \in dom vol$
93	92	a1i	$⊢ φ \to (A, B) \in dom vol$
94		volioo	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to vol ((A, B)) = B - A$
95	1 2 3 94	syl3anc	$⊢ φ \to vol ((A, B)) = B - A$
96	2 1	resubcld	$⊢ φ \to B - A \in ℝ$
97	95 96	eqeltrd	$⊢ φ \to vol ((A, B)) \in ℝ$
98		1cnd	$⊢ φ \to 1 \in ℂ$
99		iblconst	$⊢ ((A, B) \in dom vol \land vol ((A, B)) \in ℝ \land 1 \in ℂ) \to (A, B) \times \{1\} \in 𝐿^{1}$
100	93 97 98 99	syl3anc	$⊢ φ \to (A, B) \times \{1\} \in 𝐿^{1}$
101	91 100	eqeltrrid	$⊢ φ \to (t \in (A, B) ⟼ 1) \in 𝐿^{1}$
102	90 101	elind	$⊢ φ \to (t \in (A, B) ⟼ 1) \in (((A, B) \underset{cn}{⟶} ℂ) \cap 𝐿^{1})$
103	36	a1i	$⊢ φ \to ℝ \subseteq ℂ$
104	19	recnd	$⊢ (φ \land t \in [A, B]) \to t - X \in ℂ$
105		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
106	105	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
107		iccntr	$⊢ (A \in ℝ \land B \in ℝ) \to int (topGen (ran (.))) ([A, B]) = (A, B)$
108	21 107	syl	$⊢ φ \to int (topGen (ran (.))) ([A, B]) = (A, B)$
109	103 6 104 106 105 108	dvmptntr	$⊢ φ \to \frac{d (t \in [A, B]⟼ t - X)}{d_{ℝ} t} = \frac{d (t \in (A, B)⟼ t - X)}{d_{ℝ} t}$
110		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
111	110	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
112		ioossre	$⊢ (A, B) \subseteq ℝ$
113	112	sseli	$⊢ t \in (A, B) \to t \in ℝ$
114	113	adantl	$⊢ (φ \land t \in (A, B)) \to t \in ℝ$
115	114	recnd	$⊢ (φ \land t \in (A, B)) \to t \in ℂ$
116		1cnd	$⊢ (φ \land t \in (A, B)) \to 1 \in ℂ$
117	103	sselda	$⊢ (φ \land t \in ℝ) \to t \in ℂ$
118		1cnd	$⊢ (φ \land t \in ℝ) \to 1 \in ℂ$
119	111	dvmptid	$⊢ φ \to \frac{d (t \in ℝ⟼ t)}{d_{ℝ} t} = (t \in ℝ ⟼ 1)$
120	112	a1i	$⊢ φ \to (A, B) \subseteq ℝ$
121		iooretop	$⊢ (A, B) \in topGen (ran (.))$
122	121	a1i	$⊢ φ \to (A, B) \in topGen (ran (.))$
123	111 117 118 119 120 106 105 122	dvmptres	$⊢ φ \to \frac{d (t \in (A, B)⟼ t)}{d_{ℝ} t} = (t \in (A, B) ⟼ 1)$
124	9	adantr	$⊢ (φ \land t \in (A, B)) \to X \in ℂ$
125		0cnd	$⊢ (φ \land t \in (A, B)) \to 0 \in ℂ$
126	9	adantr	$⊢ (φ \land t \in ℝ) \to X \in ℂ$
127		0cnd	$⊢ (φ \land t \in ℝ) \to 0 \in ℂ$
128	111 9	dvmptc	$⊢ φ \to \frac{d (t \in ℝ⟼ X)}{d_{ℝ} t} = (t \in ℝ ⟼ 0)$
129	111 126 127 128 120 106 105 122	dvmptres	$⊢ φ \to \frac{d (t \in (A, B)⟼ X)}{d_{ℝ} t} = (t \in (A, B) ⟼ 0)$
130	111 115 116 123 124 125 129	dvmptsub	$⊢ φ \to \frac{d (t \in (A, B)⟼ t - X)}{d_{ℝ} t} = (t \in (A, B) ⟼ 1 - 0)$
131	116	subid1d	$⊢ (φ \land t \in (A, B)) \to 1 - 0 = 1$
132	131	mpteq2dva	$⊢ φ \to (t \in (A, B) ⟼ 1 - 0) = (t \in (A, B) ⟼ 1)$
133	109 130 132	3eqtrd	$⊢ φ \to \frac{d (t \in [A, B]⟼ t - X)}{d_{ℝ} t} = (t \in (A, B) ⟼ 1)$
134		oveq2	$⊢ s = t - X \to X + s = X + t - X$
135	134	fveq2d	$⊢ s = t - X \to F (X + s) = F (X + t - X)$
136		oveq1	$⊢ t = A \to t - X = A - X$
137		oveq1	$⊢ t = B \to t - X = B - X$
138	1 2 3 56 85 102 133 135 136 137 33 34	itgsubsticc	$⊢ φ \to \int_{(A - X)}^{(B - X)} F (X + s) d s = \int_{A}^{B} F (X + t - X) \cdot 1 d t$
139	124 115	pncan3d	$⊢ (φ \land t \in (A, B)) \to X + t - X = t$
140	139	fveq2d	$⊢ (φ \land t \in (A, B)) \to F (X + t - X) = F (t)$
141	140	oveq1d	$⊢ (φ \land t \in (A, B)) \to F (X + t - X) \cdot 1 = F (t) \cdot 1$
142		cncff	$⊢ F : [A, B] \underset{cn}{⟶} ℂ \to F : [A, B] ⟶ ℂ$
143	5 142	syl	$⊢ φ \to F : [A, B] ⟶ ℂ$
144	143	adantr	$⊢ (φ \land t \in (A, B)) \to F : [A, B] ⟶ ℂ$
145		ioossicc	$⊢ (A, B) \subseteq [A, B]$
146	145	sseli	$⊢ t \in (A, B) \to t \in [A, B]$
147	146	adantl	$⊢ (φ \land t \in (A, B)) \to t \in [A, B]$
148	144 147	ffvelrnd	$⊢ (φ \land t \in (A, B)) \to F (t) \in ℂ$
149	148	mulid1d	$⊢ (φ \land t \in (A, B)) \to F (t) \cdot 1 = F (t)$
150	141 149	eqtrd	$⊢ (φ \land t \in (A, B)) \to F (X + t - X) \cdot 1 = F (t)$
151	3 150	ditgeq3d	$⊢ φ \to \int_{A}^{B} F (X + t - X) \cdot 1 d t = \int_{A}^{B} F (t) d t$
152	138 151	eqtrd	$⊢ φ \to \int_{(A - X)}^{(B - X)} F (X + s) d s = \int_{A}^{B} F (t) d t$

Metamath Proof Explorer

Theorem itgsbtaddcnst

Proof