This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ T = ℜ ⁡ B i k
Assertion dfitg ⊢ ∫ A B dx = ∑ k = 0 3 i k ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ T T 0

Proof

Step Hyp Ref Expression
1 dfitg.1 ⊢ T = ℜ ⁡ B i k
2 df-itg ⊢ ∫ A B dx = ∑ k = 0 3 i k ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ ⦋ ℜ ⁡ B i k / y⦌ if x ∈ A ∧ 0 ≤ y y 0
3 fvex ⊢ ℜ ⁡ B i k ∈ V
4 id ⊢ y = ℜ ⁡ B i k → y = ℜ ⁡ B i k
5 4 1 eqtr4di ⊢ y = ℜ ⁡ B i k → y = T
6 5 breq2d ⊢ y = ℜ ⁡ B i k → 0 ≤ y ↔ 0 ≤ T
7 6 anbi2d ⊢ y = ℜ ⁡ B i k → x ∈ A ∧ 0 ≤ y ↔ x ∈ A ∧ 0 ≤ T
8 7 5 ifbieq1d ⊢ y = ℜ ⁡ B i k → if x ∈ A ∧ 0 ≤ y y 0 = if x ∈ A ∧ 0 ≤ T T 0
9 3 8 csbie ⊢ ⦋ ℜ ⁡ B i k / y⦌ if x ∈ A ∧ 0 ≤ y y 0 = if x ∈ A ∧ 0 ≤ T T 0
10 9 mpteq2i ⊢ x ∈ ℝ ⟼ ⦋ ℜ ⁡ B i k / y⦌ if x ∈ A ∧ 0 ≤ y y 0 = x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ T T 0
11 10 fveq2i ⊢ ∫ 2 ⁡ x ∈ ℝ ⟼ ⦋ ℜ ⁡ B i k / y⦌ if x ∈ A ∧ 0 ≤ y y 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ T T 0
12 11 oveq2i ⊢ i k ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ ⦋ ℜ ⁡ B i k / y⦌ if x ∈ A ∧ 0 ≤ y y 0 = i k ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ T T 0
13 12 a1i ⊢ k ∈ 0 … 3 → i k ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ ⦋ ℜ ⁡ B i k / y⦌ if x ∈ A ∧ 0 ≤ y y 0 = i k ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ T T 0
14 13 sumeq2i ⊢ ∑ k = 0 3 i k ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ ⦋ ℜ ⁡ B i k / y⦌ if x ∈ A ∧ 0 ≤ y y 0 = ∑ k = 0 3 i k ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ T T 0
15 2 14 eqtri ⊢ ∫ A B dx = ∑ k = 0 3 i k ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ T T 0