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

Metamath Proof Explorer

Theorem itgresr

Description: The domain of an integral only matters in its intersection with RR . (Contributed by Mario Carneiro, 29-Jun-2014)

Ref Expression
Assertion itgresr ⊢ ∫ A B dx = ∫ A ∩ ℝ B dx

Proof

Step Hyp Ref Expression
1 simpr ⊢ k ∈ 0 … 3 ∧ x ∈ ℝ → x ∈ ℝ
2 1 biantrud ⊢ k ∈ 0 … 3 ∧ x ∈ ℝ → x ∈ A ↔ x ∈ A ∧ x ∈ ℝ
3 elin ⊢ x ∈ A ∩ ℝ ↔ x ∈ A ∧ x ∈ ℝ
4 2 3 bitr4di ⊢ k ∈ 0 … 3 ∧ x ∈ ℝ → x ∈ A ↔ x ∈ A ∩ ℝ
5 4 anbi1d ⊢ k ∈ 0 … 3 ∧ x ∈ ℝ → x ∈ A ∧ 0 ≤ ℜ ⁡ B i k ↔ x ∈ A ∩ ℝ ∧ 0 ≤ ℜ ⁡ B i k
6 5 ifbid ⊢ k ∈ 0 … 3 ∧ x ∈ ℝ → if x ∈ A ∧ 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 = if x ∈ A ∩ ℝ ∧ 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0
7 6 mpteq2dva ⊢ k ∈ 0 … 3 → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 = x ∈ ℝ ⟼ if x ∈ A ∩ ℝ ∧ 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0
8 7 fveq2d ⊢ k ∈ 0 … 3 → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∩ ℝ ∧ 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0
9 8 oveq2d ⊢ k ∈ 0 … 3 → i k ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 = i k ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∩ ℝ ∧ 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0
10 9 sumeq2i ⊢ ∑ k = 0 3 i k ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 = ∑ k = 0 3 i k ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∩ ℝ ∧ 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0
11 eqid ⊢ ℜ ⁡ B i k = ℜ ⁡ B i k
12 11 dfitg ⊢ ∫ A B dx = ∑ k = 0 3 i k ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0
13 11 dfitg ⊢ ∫ A ∩ ℝ B dx = ∑ k = 0 3 i k ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∩ ℝ ∧ 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0
14 10 12 13 3eqtr4i ⊢ ∫ A B dx = ∫ A ∩ ℝ B dx