Metamath Proof Explorer

Theorem 3factsumint2

Description: Move constants out of integrals or sums and/or commute sum and integral. (Contributed by metakunt, 26-Apr-2024)

Ref Expression
Hypotheses 3factsumint2.1 ⊢ φ ∧ x ∈ A → F ∈ ℂ
3factsumint2.2 ⊢ φ ∧ k ∈ B → G ∈ ℂ
3factsumint2.3 ⊢ φ ∧ x ∈ A ∧ k ∈ B → H ∈ ℂ
Assertion 3factsumint2 ⊢ φ → ∑ k ∈ B ∫ A F ⁢ G ⁢ H dx = ∑ k ∈ B ∫ A G ⁢ F ⁢ H dx

Proof

Step Hyp Ref Expression
1 3factsumint2.1 ⊢ φ ∧ x ∈ A → F ∈ ℂ
2 3factsumint2.2 ⊢ φ ∧ k ∈ B → G ∈ ℂ
3 3factsumint2.3 ⊢ φ ∧ x ∈ A ∧ k ∈ B → H ∈ ℂ
4 1 adantlr ⊢ φ ∧ k ∈ B ∧ x ∈ A → F ∈ ℂ
5 2 adantr ⊢ φ ∧ k ∈ B ∧ x ∈ A → G ∈ ℂ
6 ancom ⊢ x ∈ A ∧ k ∈ B ↔ k ∈ B ∧ x ∈ A
7 6 anbi2i ⊢ φ ∧ x ∈ A ∧ k ∈ B ↔ φ ∧ k ∈ B ∧ x ∈ A
8 anass ⊢ φ ∧ k ∈ B ∧ x ∈ A ↔ φ ∧ k ∈ B ∧ x ∈ A
9 8 bicomi ⊢ φ ∧ k ∈ B ∧ x ∈ A ↔ φ ∧ k ∈ B ∧ x ∈ A
10 7 9 bitri ⊢ φ ∧ x ∈ A ∧ k ∈ B ↔ φ ∧ k ∈ B ∧ x ∈ A
11 10 imbi1i ⊢ φ ∧ x ∈ A ∧ k ∈ B → H ∈ ℂ ↔ φ ∧ k ∈ B ∧ x ∈ A → H ∈ ℂ
12 3 11 mpbi ⊢ φ ∧ k ∈ B ∧ x ∈ A → H ∈ ℂ
13 4 5 12 mul12d ⊢ φ ∧ k ∈ B ∧ x ∈ A → F ⁢ G ⁢ H = G ⁢ F ⁢ H
14 13 itgeq2dv ⊢ φ ∧ k ∈ B → ∫ A F ⁢ G ⁢ H dx = ∫ A G ⁢ F ⁢ H dx
15 14 sumeq2dv ⊢ φ → ∑ k ∈ B ∫ A F ⁢ G ⁢ H dx = ∑ k ∈ B ∫ A G ⁢ F ⁢ H dx