Metamath Proof Explorer


Theorem 3factsumint3

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

Ref Expression
Hypotheses 3factsumint3.1 A = L U
3factsumint3.2 φ L
3factsumint3.3 φ U
3factsumint3.4 φ x A F
3factsumint3.5 φ x A F : A cn
3factsumint3.6 φ k B G
3factsumint3.7 φ x A k B H
3factsumint3.8 φ k B x A H : A cn
Assertion 3factsumint3 φ k B A G F H dx = k B G A F H dx

Proof

Step Hyp Ref Expression
1 3factsumint3.1 A = L U
2 3factsumint3.2 φ L
3 3factsumint3.3 φ U
4 3factsumint3.4 φ x A F
5 3factsumint3.5 φ x A F : A cn
6 3factsumint3.6 φ k B G
7 3factsumint3.7 φ x A k B H
8 3factsumint3.8 φ k B x A H : A cn
9 4 adantlr φ k B x A F
10 ancom x A k B k B x A
11 10 anbi2i φ x A k B φ k B x A
12 anass φ k B x A φ k B x A
13 12 bicomi φ k B x A φ k B x A
14 11 13 bitri φ x A k B φ k B x A
15 14 imbi1i φ x A k B H φ k B x A H
16 7 15 mpbi φ k B x A H
17 9 16 mulcld φ k B x A F H
18 2 adantr φ k B L
19 3 adantr φ k B U
20 5 adantr φ k B x A F : A cn
21 20 8 mulcncf φ k B x A F H : A cn
22 1 oveq1i A cn = L U cn
23 21 22 eleqtrdi φ k B x A F H : L U cn
24 cnicciblnc L U x A F H : L U cn x A F H 𝐿 1
25 18 19 23 24 syl3anc φ k B x A F H 𝐿 1
26 6 17 25 itgmulc2 φ k B G A F H dx = A G F H dx
27 26 eqcomd φ k B A G F H dx = G A F H dx
28 27 sumeq2dv φ k B A G F H dx = k B G A F H dx