Metamath Proof Explorer

Theorem 3factsumint4

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

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

Proof

Step Hyp Ref Expression
1 3factsumint4.1 ⊢ φ → B ∈ Fin
2 3factsumint4.2 ⊢ φ ∧ x ∈ A → F ∈ ℂ
3 3factsumint4.3 ⊢ φ ∧ k ∈ B → G ∈ ℂ
4 3factsumint4.4 ⊢ φ ∧ x ∈ A ∧ k ∈ B → H ∈ ℂ
5 1 adantr ⊢ φ ∧ x ∈ A → B ∈ Fin
6 3 adantlr ⊢ φ ∧ x ∈ A ∧ k ∈ B → G ∈ ℂ
7 anass ⊢ φ ∧ x ∈ A ∧ k ∈ B ↔ φ ∧ x ∈ A ∧ k ∈ B
8 7 bicomi ⊢ φ ∧ x ∈ A ∧ k ∈ B ↔ φ ∧ x ∈ A ∧ k ∈ B
9 8 imbi1i ⊢ φ ∧ x ∈ A ∧ k ∈ B → H ∈ ℂ ↔ φ ∧ x ∈ A ∧ k ∈ B → H ∈ ℂ
10 4 9 mpbi ⊢ φ ∧ x ∈ A ∧ k ∈ B → H ∈ ℂ
11 6 10 mulcld ⊢ φ ∧ x ∈ A ∧ k ∈ B → G ⁢ H ∈ ℂ
12 5 2 11 fsummulc2 ⊢ φ ∧ x ∈ A → F ⁢ ∑ k ∈ B G ⁢ H = ∑ k ∈ B F ⁢ G ⁢ H
13 12 eqcomd ⊢ φ ∧ x ∈ A → ∑ k ∈ B F ⁢ G ⁢ H = F ⁢ ∑ k ∈ B G ⁢ H
14 13 itgeq2dv ⊢ φ → ∫ A ∑ k ∈ B F ⁢ G ⁢ H dx = ∫ A F ⁢ ∑ k ∈ B G ⁢ H dx