Metamath Proof Explorer

Theorem cbvitg

Description: Change bound variable in an integral. (Contributed by Mario Carneiro, 28-Jun-2014)

Ref Expression
Hypotheses cbvitg.1 ⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐶 )
cbvitg.2 ⊢ Ⅎ 𝑦 𝐵
cbvitg.3 ⊢ Ⅎ 𝑥 𝐶
Assertion cbvitg ∫ 𝐴 𝐵 d 𝑥 = ∫ 𝐴 𝐶 d 𝑦

Proof

Step Hyp Ref Expression
1 cbvitg.1 ⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐶 )
2 cbvitg.2 ⊢ Ⅎ 𝑦 𝐵
3 cbvitg.3 ⊢ Ⅎ 𝑥 𝐶
4 nfv ⊢ Ⅎ 𝑦 𝑥 ∈ 𝐴
5 nfcv ⊢ Ⅎ 𝑦 0
6 nfcv ⊢ Ⅎ 𝑦 ≤
7 nfcv ⊢ Ⅎ 𝑦 ℜ
8 nfcv ⊢ Ⅎ 𝑦 /
9 nfcv ⊢ Ⅎ 𝑦 ( i ↑ 𝑘 )
10 2 8 9 nfov ⊢ Ⅎ 𝑦 ( 𝐵 / ( i ↑ 𝑘 ) )
11 7 10 nffv ⊢ Ⅎ 𝑦 ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) )
12 5 6 11 nfbr ⊢ Ⅎ 𝑦 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) )
13 4 12 nfan ⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) )
14 13 11 5 nfif ⊢ Ⅎ 𝑦 if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 )
15 nfv ⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴
16 nfcv ⊢ Ⅎ 𝑥 0
17 nfcv ⊢ Ⅎ 𝑥 ≤
18 nfcv ⊢ Ⅎ 𝑥 ℜ
19 nfcv ⊢ Ⅎ 𝑥 /
20 nfcv ⊢ Ⅎ 𝑥 ( i ↑ 𝑘 )
21 3 19 20 nfov ⊢ Ⅎ 𝑥 ( 𝐶 / ( i ↑ 𝑘 ) )
22 18 21 nffv ⊢ Ⅎ 𝑥 ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) )
23 16 17 22 nfbr ⊢ Ⅎ 𝑥 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) )
24 15 23 nfan ⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) )
25 24 22 16 nfif ⊢ Ⅎ 𝑥 if ( ( 𝑦 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 )
26 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
27 1 fvoveq1d ⊢ ( 𝑥 = 𝑦 → ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) )
28 27 breq2d ⊢ ( 𝑥 = 𝑦 → ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ↔ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) )
29 26 28 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) ↔ ( 𝑦 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) ) )
30 29 27 ifbieq1d ⊢ ( 𝑥 = 𝑦 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( ( 𝑦 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) )
31 14 25 30 cbvmpt ⊢ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) )
32 31 a1i ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
33 32 fveq2d ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) )
34 33 oveq2d ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) )
35 34 sumeq2i ⊢ Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) )
36 eqid ⊢ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) )
37 36 dfitg ⊢ ∫ 𝐴 𝐵 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) )
38 eqid ⊢ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) )
39 38 dfitg ⊢ ∫ 𝐴 𝐶 d 𝑦 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) )
40 35 37 39 3eqtr4i ⊢ ∫ 𝐴 𝐵 d 𝑥 = ∫ 𝐴 𝐶 d 𝑦