Metamath Proof Explorer

Theorem itgvallem

Description: Substitution lemma. (Contributed by Mario Carneiro, 7-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypothesis itgvallem.1 ⊢ ( i ↑ 𝐾 ) = 𝑇
Assertion itgvallem ( 𝑘 = 𝐾 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / 𝑇 ) ) ) , ( ℜ ‘ ( 𝐵 / 𝑇 ) ) , 0 ) ) ) )

Proof

Step Hyp Ref Expression
1 itgvallem.1 ⊢ ( i ↑ 𝐾 ) = 𝑇
2 oveq2 ⊢ ( 𝑘 = 𝐾 → ( i ↑ 𝑘 ) = ( i ↑ 𝐾 ) )
3 2 1 eqtrdi ⊢ ( 𝑘 = 𝐾 → ( i ↑ 𝑘 ) = 𝑇 )
4 3 oveq2d ⊢ ( 𝑘 = 𝐾 → ( 𝐵 / ( i ↑ 𝑘 ) ) = ( 𝐵 / 𝑇 ) )
5 4 fveq2d ⊢ ( 𝑘 = 𝐾 → ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐵 / 𝑇 ) ) )
6 5 breq2d ⊢ ( 𝑘 = 𝐾 → ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ↔ 0 ≤ ( ℜ ‘ ( 𝐵 / 𝑇 ) ) ) )
7 6 anbi2d ⊢ ( 𝑘 = 𝐾 → ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / 𝑇 ) ) ) ) )
8 7 5 ifbieq1d ⊢ ( 𝑘 = 𝐾 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / 𝑇 ) ) ) , ( ℜ ‘ ( 𝐵 / 𝑇 ) ) , 0 ) )
9 8 mpteq2dv ⊢ ( 𝑘 = 𝐾 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / 𝑇 ) ) ) , ( ℜ ‘ ( 𝐵 / 𝑇 ) ) , 0 ) ) )
10 9 fveq2d ⊢ ( 𝑘 = 𝐾 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / 𝑇 ) ) ) , ( ℜ ‘ ( 𝐵 / 𝑇 ) ) , 0 ) ) ) )