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