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 K = T
Assertion itgvallem ⊢ k = K → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B T ℜ ⁡ B T 0

Proof

Step Hyp Ref Expression
1 itgvallem.1 ⊢ i K = T
2 oveq2 ⊢ k = K → i k = i K
3 2 1 eqtrdi ⊢ k = K → i k = T
4 3 oveq2d ⊢ k = K → B i k = B T
5 4 fveq2d ⊢ k = K → ℜ ⁡ B i k = ℜ ⁡ B T
6 5 breq2d ⊢ k = K → 0 ≤ ℜ ⁡ B i k ↔ 0 ≤ ℜ ⁡ B T
7 6 anbi2d ⊢ k = K → x ∈ A ∧ 0 ≤ ℜ ⁡ B i k ↔ x ∈ A ∧ 0 ≤ ℜ ⁡ B T
8 7 5 ifbieq1d ⊢ k = K → if x ∈ A ∧ 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 = if x ∈ A ∧ 0 ≤ ℜ ⁡ B T ℜ ⁡ B T 0
9 8 mpteq2dv ⊢ k = K → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 = x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B T ℜ ⁡ B T 0
10 9 fveq2d ⊢ k = K → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B T ℜ ⁡ B T 0