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

Metamath Proof Explorer

Theorem itgeq1f

Description: Equality theorem for an integral. (Contributed by Mario Carneiro, 28-Jun-2014) Avoid axioms. (Revised by GG, 1-Sep-2025)

Ref Expression
Hypotheses itgeq1f.1 ⊢ Ⅎ _ x A
itgeq1f.2 ⊢ Ⅎ _ x B
Assertion itgeq1f ⊢ A = B → ∫ A C dx = ∫ B C dx

Proof

Step Hyp Ref Expression
1 itgeq1f.1 ⊢ Ⅎ _ x A
2 itgeq1f.2 ⊢ Ⅎ _ x B
3 1 2 nfeq ⊢ Ⅎ x A = B
4 eleq2 ⊢ A = B → x ∈ A ↔ x ∈ B
5 4 anbi1d ⊢ A = B → x ∈ A ∧ 0 ≤ y ↔ x ∈ B ∧ 0 ≤ y
6 5 ifbid ⊢ A = B → if x ∈ A ∧ 0 ≤ y y 0 = if x ∈ B ∧ 0 ≤ y y 0
7 6 csbeq2dv ⊢ A = B → ⦋ ℜ ⁡ C i k / y⦌ if x ∈ A ∧ 0 ≤ y y 0 = ⦋ ℜ ⁡ C i k / y⦌ if x ∈ B ∧ 0 ≤ y y 0
8 7 adantr ⊢ A = B ∧ x ∈ ℝ → ⦋ ℜ ⁡ C i k / y⦌ if x ∈ A ∧ 0 ≤ y y 0 = ⦋ ℜ ⁡ C i k / y⦌ if x ∈ B ∧ 0 ≤ y y 0
9 3 8 mpteq2da ⊢ A = B → x ∈ ℝ ⟼ ⦋ ℜ ⁡ C i k / y⦌ if x ∈ A ∧ 0 ≤ y y 0 = x ∈ ℝ ⟼ ⦋ ℜ ⁡ C i k / y⦌ if x ∈ B ∧ 0 ≤ y y 0
10 9 fveq2d ⊢ A = B → ∫ 2 ⁡ x ∈ ℝ ⟼ ⦋ ℜ ⁡ C i k / y⦌ if x ∈ A ∧ 0 ≤ y y 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ ⦋ ℜ ⁡ C i k / y⦌ if x ∈ B ∧ 0 ≤ y y 0
11 10 oveq2d ⊢ A = B → i k ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ ⦋ ℜ ⁡ C i k / y⦌ if x ∈ A ∧ 0 ≤ y y 0 = i k ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ ⦋ ℜ ⁡ C i k / y⦌ if x ∈ B ∧ 0 ≤ y y 0
12 11 sumeq2sdv ⊢ A = B → ∑ k = 0 3 i k ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ ⦋ ℜ ⁡ C i k / y⦌ if x ∈ A ∧ 0 ≤ y y 0 = ∑ k = 0 3 i k ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ ⦋ ℜ ⁡ C i k / y⦌ if x ∈ B ∧ 0 ≤ y y 0
13 df-itg ⊢ ∫ A C dx = ∑ k = 0 3 i k ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ ⦋ ℜ ⁡ C i k / y⦌ if x ∈ A ∧ 0 ≤ y y 0
14 df-itg ⊢ ∫ B C dx = ∑ k = 0 3 i k ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ ⦋ ℜ ⁡ C i k / y⦌ if x ∈ B ∧ 0 ≤ y y 0
15 12 13 14 3eqtr4g ⊢ A = B → ∫ A C dx = ∫ B C dx