Metamath Proof Explorer

Theorem dfitg

Description: Evaluate the class substitution in df-itg . (Contributed by Mario Carneiro, 28-Jun-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypothesis dfitg.1 ⊢ 𝑇 = ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) )
Assertion dfitg ∫ 𝐴 𝐵 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇 ) , 𝑇 , 0 ) ) ) )

Proof

Step Hyp Ref Expression
1 dfitg.1 ⊢ 𝑇 = ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) )
2 df-itg ⊢ ∫ 𝐴 𝐵 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) )
3 fvex ⊢ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ∈ V
4 id ⊢ ( 𝑦 = ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) → 𝑦 = ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) )
5 4 1 eqtr4di ⊢ ( 𝑦 = ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) → 𝑦 = 𝑇 )
6 5 breq2d ⊢ ( 𝑦 = ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) → ( 0 ≤ 𝑦 ↔ 0 ≤ 𝑇 ) )
7 6 anbi2d ⊢ ( 𝑦 = ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) → ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇 ) ) )
8 7 5 ifbieq1d ⊢ ( 𝑦 = ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) = if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇 ) , 𝑇 , 0 ) )
9 3 8 csbie ⊢ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) = if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇 ) , 𝑇 , 0 )
10 9 mpteq2i ⊢ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇 ) , 𝑇 , 0 ) )
11 10 fveq2i ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇 ) , 𝑇 , 0 ) ) )
12 11 oveq2i ⊢ ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) ) = ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇 ) , 𝑇 , 0 ) ) ) )
13 12 a1i ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) ) = ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇 ) , 𝑇 , 0 ) ) ) ) )
14 13 sumeq2i ⊢ Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇 ) , 𝑇 , 0 ) ) ) )
15 2 14 eqtri ⊢ ∫ 𝐴 𝐵 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇 ) , 𝑇 , 0 ) ) ) )