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

Metamath Proof Explorer

Theorem itgitg2

Description: Transfer an integral using S.2 to an equivalent integral using S. . (Contributed by Mario Carneiro, 6-Aug-2014)

Ref Expression
Hypotheses itgitg2.1 ⊢ φ ∧ x ∈ ℝ → A ∈ ℝ
itgitg2.2 ⊢ φ ∧ x ∈ ℝ → 0 ≤ A
itgitg2.3 ⊢ φ → x ∈ ℝ ⟼ A ∈ 𝐿 1
Assertion itgitg2 ⊢ φ → ∫ ℝ A dx = ∫ 2 ⁡ x ∈ ℝ ⟼ A

Proof

Step Hyp Ref Expression
1 itgitg2.1 ⊢ φ ∧ x ∈ ℝ → A ∈ ℝ
2 itgitg2.2 ⊢ φ ∧ x ∈ ℝ → 0 ≤ A
3 itgitg2.3 ⊢ φ → x ∈ ℝ ⟼ A ∈ 𝐿 1
4 1 3 2 itgposval ⊢ φ → ∫ ℝ A dx = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ ℝ A 0
5 iftrue ⊢ x ∈ ℝ → if x ∈ ℝ A 0 = A
6 5 mpteq2ia ⊢ x ∈ ℝ ⟼ if x ∈ ℝ A 0 = x ∈ ℝ ⟼ A
7 6 fveq2i ⊢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ ℝ A 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ A
8 4 7 eqtrdi ⊢ φ → ∫ ℝ A dx = ∫ 2 ⁡ x ∈ ℝ ⟼ A