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 
|- ( ph -> B e. Fin )
3factsumint1.3 
|- ( ph -> L e. RR )
3factsumint1.4 
|- ( ph -> U e. RR )
3factsumint1.5 
|- ( ( ph /\ x e. A ) -> F e. CC )
3factsumint1.6 
|- ( ph -> ( x e. A |-> F ) e. ( A -cn-> CC ) )
3factsumint1.7 
|- ( ( ph /\ k e. B ) -> G e. CC )
3factsumint1.8 
|- ( ( ph /\ ( x e. A /\ k e. B ) ) -> H e. CC )
3factsumint1.9 
|- ( ( ph /\ k e. B ) -> ( x e. A |-> H ) e. ( A -cn-> CC ) )
Assertion 3factsumint1 
|- ( ph -> S. A sum_ k e. B ( F x. ( G x. H ) ) _d x = sum_ k e. B S. A ( F x. ( G x. H ) ) _d x )

Proof

Step Hyp Ref Expression
1 3factsumint1.1 
 |-  A = ( L [,] U )
2 3factsumint1.2 
 |-  ( ph -> B e. Fin )
3 3factsumint1.3 
 |-  ( ph -> L e. RR )
4 3factsumint1.4 
 |-  ( ph -> U e. RR )
5 3factsumint1.5 
 |-  ( ( ph /\ x e. A ) -> F e. CC )
6 3factsumint1.6 
 |-  ( ph -> ( x e. A |-> F ) e. ( A -cn-> CC ) )
7 3factsumint1.7 
 |-  ( ( ph /\ k e. B ) -> G e. CC )
8 3factsumint1.8 
 |-  ( ( ph /\ ( x e. A /\ k e. B ) ) -> H e. CC )
9 3factsumint1.9 
 |-  ( ( ph /\ k e. B ) -> ( x e. A |-> H ) e. ( A -cn-> CC ) )
10 iccmbl 
 |-  ( ( L e. RR /\ U e. RR ) -> ( L [,] U ) e. dom vol )
11 3 4 10 syl2anc 
 |-  ( ph -> ( L [,] U ) e. dom vol )
12 1 11 eqeltrid 
 |-  ( ph -> A e. dom vol )
13 5 adantrr 
 |-  ( ( ph /\ ( x e. A /\ k e. B ) ) -> F e. CC )
14 7 adantrl 
 |-  ( ( ph /\ ( x e. A /\ k e. B ) ) -> G e. CC )
15 14 8 mulcld 
 |-  ( ( ph /\ ( x e. A /\ k e. B ) ) -> ( G x. H ) e. CC )
16 13 15 mulcld 
 |-  ( ( ph /\ ( x e. A /\ k e. B ) ) -> ( F x. ( G x. H ) ) e. CC )
17 ovex 
 |-  ( L [,] U ) e. _V
18 1 17 eqeltri 
 |-  A e. _V
19 18 a1i 
 |-  ( ( ph /\ k e. B ) -> A e. _V )
20 13 anass1rs 
 |-  ( ( ( ph /\ k e. B ) /\ x e. A ) -> F e. CC )
21 15 anass1rs 
 |-  ( ( ( ph /\ k e. B ) /\ x e. A ) -> ( G x. H ) e. CC )
22 eqidd 
 |-  ( ( ph /\ k e. B ) -> ( x e. A |-> F ) = ( x e. A |-> F ) )
23 eqidd 
 |-  ( ( ph /\ k e. B ) -> ( x e. A |-> ( G x. H ) ) = ( x e. A |-> ( G x. H ) ) )
24 19 20 21 22 23 offval2 
 |-  ( ( ph /\ k e. B ) -> ( ( x e. A |-> F ) oF x. ( x e. A |-> ( G x. H ) ) ) = ( x e. A |-> ( F x. ( G x. H ) ) ) )
25 cnmbf 
 |-  ( ( A e. dom vol /\ ( x e. A |-> F ) e. ( A -cn-> CC ) ) -> ( x e. A |-> F ) e. MblFn )
26 12 6 25 syl2anc 
 |-  ( ph -> ( x e. A |-> F ) e. MblFn )
27 26 adantr 
 |-  ( ( ph /\ k e. B ) -> ( x e. A |-> F ) e. MblFn )
28 8 anass1rs 
 |-  ( ( ( ph /\ k e. B ) /\ x e. A ) -> H e. CC )
29 3 adantr 
 |-  ( ( ph /\ k e. B ) -> L e. RR )
30 4 adantr 
 |-  ( ( ph /\ k e. B ) -> U e. RR )
31 1 oveq1i 
 |-  ( A -cn-> CC ) = ( ( L [,] U ) -cn-> CC )
32 31 eleq2i 
 |-  ( ( x e. A |-> H ) e. ( A -cn-> CC ) <-> ( x e. A |-> H ) e. ( ( L [,] U ) -cn-> CC ) )
33 9 32 sylib 
 |-  ( ( ph /\ k e. B ) -> ( x e. A |-> H ) e. ( ( L [,] U ) -cn-> CC ) )
34 cnicciblnc 
 |-  ( ( L e. RR /\ U e. RR /\ ( x e. A |-> H ) e. ( ( L [,] U ) -cn-> CC ) ) -> ( x e. A |-> H ) e. L^1 )
35 29 30 33 34 syl3anc 
 |-  ( ( ph /\ k e. B ) -> ( x e. A |-> H ) e. L^1 )
36 7 28 35 iblmulc2 
 |-  ( ( ph /\ k e. B ) -> ( x e. A |-> ( G x. H ) ) e. L^1 )
37 31 eleq2i 
 |-  ( ( x e. A |-> F ) e. ( A -cn-> CC ) <-> ( x e. A |-> F ) e. ( ( L [,] U ) -cn-> CC ) )
38 6 37 sylib 
 |-  ( ph -> ( x e. A |-> F ) e. ( ( L [,] U ) -cn-> CC ) )
39 cniccbdd 
 |-  ( ( L e. RR /\ U e. RR /\ ( x e. A |-> F ) e. ( ( L [,] U ) -cn-> CC ) ) -> E. q e. RR A. r e. ( L [,] U ) ( abs ` ( ( x e. A |-> F ) ` r ) ) <_ q )
40 3 4 38 39 syl3anc 
 |-  ( ph -> E. q e. RR A. r e. ( L [,] U ) ( abs ` ( ( x e. A |-> F ) ` r ) ) <_ q )
41 40 adantr 
 |-  ( ( ph /\ k e. B ) -> E. q e. RR A. r e. ( L [,] U ) ( abs ` ( ( x e. A |-> F ) ` r ) ) <_ q )
42 5 ralrimiva 
 |-  ( ph -> A. x e. A F e. CC )
43 dmmptg 
 |-  ( A. x e. A F e. CC -> dom ( x e. A |-> F ) = A )
44 42 43 syl 
 |-  ( ph -> dom ( x e. A |-> F ) = A )
45 44 1 eqtrdi 
 |-  ( ph -> dom ( x e. A |-> F ) = ( L [,] U ) )
46 45 raleqdv 
 |-  ( ph -> ( A. r e. dom ( x e. A |-> F ) ( abs ` ( ( x e. A |-> F ) ` r ) ) <_ q <-> A. r e. ( L [,] U ) ( abs ` ( ( x e. A |-> F ) ` r ) ) <_ q ) )
47 46 rexbidv 
 |-  ( ph -> ( E. q e. RR A. r e. dom ( x e. A |-> F ) ( abs ` ( ( x e. A |-> F ) ` r ) ) <_ q <-> E. q e. RR A. r e. ( L [,] U ) ( abs ` ( ( x e. A |-> F ) ` r ) ) <_ q ) )
48 47 adantr 
 |-  ( ( ph /\ k e. B ) -> ( E. q e. RR A. r e. dom ( x e. A |-> F ) ( abs ` ( ( x e. A |-> F ) ` r ) ) <_ q <-> E. q e. RR A. r e. ( L [,] U ) ( abs ` ( ( x e. A |-> F ) ` r ) ) <_ q ) )
49 41 48 mpbird 
 |-  ( ( ph /\ k e. B ) -> E. q e. RR A. r e. dom ( x e. A |-> F ) ( abs ` ( ( x e. A |-> F ) ` r ) ) <_ q )
50 bddmulibl 
 |-  ( ( ( x e. A |-> F ) e. MblFn /\ ( x e. A |-> ( G x. H ) ) e. L^1 /\ E. q e. RR A. r e. dom ( x e. A |-> F ) ( abs ` ( ( x e. A |-> F ) ` r ) ) <_ q ) -> ( ( x e. A |-> F ) oF x. ( x e. A |-> ( G x. H ) ) ) e. L^1 )
51 27 36 49 50 syl3anc 
 |-  ( ( ph /\ k e. B ) -> ( ( x e. A |-> F ) oF x. ( x e. A |-> ( G x. H ) ) ) e. L^1 )
52 24 51 eqeltrrd 
 |-  ( ( ph /\ k e. B ) -> ( x e. A |-> ( F x. ( G x. H ) ) ) e. L^1 )
53 12 2 16 52 itgfsum 
 |-  ( ph -> ( ( x e. A |-> sum_ k e. B ( F x. ( G x. H ) ) ) e. L^1 /\ S. A sum_ k e. B ( F x. ( G x. H ) ) _d x = sum_ k e. B S. A ( F x. ( G x. H ) ) _d x ) )
54 53 simprd 
 |-  ( ph -> S. A sum_ k e. B ( F x. ( G x. H ) ) _d x = sum_ k e. B S. A ( F x. ( G x. H ) ) _d x )