Metamath Proof Explorer


Theorem 3factsumint1

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

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

Proof

Step Hyp Ref Expression
1 3factsumint1.1 A = L U
2 3factsumint1.2 φ B Fin
3 3factsumint1.3 φ L
4 3factsumint1.4 φ U
5 3factsumint1.5 φ x A F
6 3factsumint1.6 φ x A F : A cn
7 3factsumint1.7 φ k B G
8 3factsumint1.8 φ x A k B H
9 3factsumint1.9 φ k B x A H : A cn
10 iccmbl L U L U dom vol
11 3 4 10 syl2anc φ L U dom vol
12 1 11 eqeltrid φ A dom vol
13 5 adantrr φ x A k B F
14 7 adantrl φ x A k B G
15 14 8 mulcld φ x A k B G H
16 13 15 mulcld φ x A k B F G H
17 ovex L U V
18 1 17 eqeltri A V
19 18 a1i φ k B A V
20 13 anass1rs φ k B x A F
21 15 anass1rs φ k B x A G H
22 eqidd φ k B x A F = x A F
23 eqidd φ k B x A G H = x A G H
24 19 20 21 22 23 offval2 φ k B x A F × f x A G H = x A F G H
25 cnmbf A dom vol x A F : A cn x A F MblFn
26 12 6 25 syl2anc φ x A F MblFn
27 26 adantr φ k B x A F MblFn
28 8 anass1rs φ k B x A H
29 3 adantr φ k B L
30 4 adantr φ k B U
31 1 oveq1i A cn = L U cn
32 31 eleq2i x A H : A cn x A H : L U cn
33 9 32 sylib φ k B x A H : L U cn
34 cnicciblnc L U x A H : L U cn x A H 𝐿 1
35 29 30 33 34 syl3anc φ k B x A H 𝐿 1
36 7 28 35 iblmulc2 φ k B x A G H 𝐿 1
37 31 eleq2i x A F : A cn x A F : L U cn
38 6 37 sylib φ x A F : L U cn
39 cniccbdd L U x A F : L U cn q r L U x A F r q
40 3 4 38 39 syl3anc φ q r L U x A F r q
41 40 adantr φ k B q r L U x A F r q
42 5 ralrimiva φ x A F
43 dmmptg x A F dom x A F = A
44 42 43 syl φ dom x A F = A
45 44 1 eqtrdi φ dom x A F = L U
46 45 raleqdv φ r dom x A F x A F r q r L U x A F r q
47 46 rexbidv φ q r dom x A F x A F r q q r L U x A F r q
48 47 adantr φ k B q r dom x A F x A F r q q r L U x A F r q
49 41 48 mpbird φ k B q r dom x A F x A F r q
50 bddmulibl x A F MblFn x A G H 𝐿 1 q r dom x A F x A F r q x A F × f x A G H 𝐿 1
51 27 36 49 50 syl3anc φ k B x A F × f x A G H 𝐿 1
52 24 51 eqeltrrd φ k B x A F G H 𝐿 1
53 12 2 16 52 itgfsum φ x A k B F G H 𝐿 1 A k B F G H dx = k B A F G H dx
54 53 simprd φ A k B F G H dx = k B A F G H dx