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

Proof

Step Hyp Ref Expression
1 3factsumint3.1 
 |-  A = ( L [,] U )
2 3factsumint3.2 
 |-  ( ph -> L e. RR )
3 3factsumint3.3 
 |-  ( ph -> U e. RR )
4 3factsumint3.4 
 |-  ( ( ph /\ x e. A ) -> F e. CC )
5 3factsumint3.5 
 |-  ( ph -> ( x e. A |-> F ) e. ( A -cn-> CC ) )
6 3factsumint3.6 
 |-  ( ( ph /\ k e. B ) -> G e. CC )
7 3factsumint3.7 
 |-  ( ( ph /\ ( x e. A /\ k e. B ) ) -> H e. CC )
8 3factsumint3.8 
 |-  ( ( ph /\ k e. B ) -> ( x e. A |-> H ) e. ( A -cn-> CC ) )
9 4 adantlr 
 |-  ( ( ( ph /\ k e. B ) /\ x e. A ) -> F e. CC )
10 ancom 
 |-  ( ( x e. A /\ k e. B ) <-> ( k e. B /\ x e. A ) )
11 10 anbi2i 
 |-  ( ( ph /\ ( x e. A /\ k e. B ) ) <-> ( ph /\ ( k e. B /\ x e. A ) ) )
12 anass 
 |-  ( ( ( ph /\ k e. B ) /\ x e. A ) <-> ( ph /\ ( k e. B /\ x e. A ) ) )
13 12 bicomi 
 |-  ( ( ph /\ ( k e. B /\ x e. A ) ) <-> ( ( ph /\ k e. B ) /\ x e. A ) )
14 11 13 bitri 
 |-  ( ( ph /\ ( x e. A /\ k e. B ) ) <-> ( ( ph /\ k e. B ) /\ x e. A ) )
15 14 imbi1i 
 |-  ( ( ( ph /\ ( x e. A /\ k e. B ) ) -> H e. CC ) <-> ( ( ( ph /\ k e. B ) /\ x e. A ) -> H e. CC ) )
16 7 15 mpbi 
 |-  ( ( ( ph /\ k e. B ) /\ x e. A ) -> H e. CC )
17 9 16 mulcld 
 |-  ( ( ( ph /\ k e. B ) /\ x e. A ) -> ( F x. H ) e. CC )
18 2 adantr 
 |-  ( ( ph /\ k e. B ) -> L e. RR )
19 3 adantr 
 |-  ( ( ph /\ k e. B ) -> U e. RR )
20 5 adantr 
 |-  ( ( ph /\ k e. B ) -> ( x e. A |-> F ) e. ( A -cn-> CC ) )
21 20 8 mulcncf 
 |-  ( ( ph /\ k e. B ) -> ( x e. A |-> ( F x. H ) ) e. ( A -cn-> CC ) )
22 1 oveq1i 
 |-  ( A -cn-> CC ) = ( ( L [,] U ) -cn-> CC )
23 21 22 eleqtrdi 
 |-  ( ( ph /\ k e. B ) -> ( x e. A |-> ( F x. H ) ) e. ( ( L [,] U ) -cn-> CC ) )
24 cnicciblnc 
 |-  ( ( L e. RR /\ U e. RR /\ ( x e. A |-> ( F x. H ) ) e. ( ( L [,] U ) -cn-> CC ) ) -> ( x e. A |-> ( F x. H ) ) e. L^1 )
25 18 19 23 24 syl3anc 
 |-  ( ( ph /\ k e. B ) -> ( x e. A |-> ( F x. H ) ) e. L^1 )
26 6 17 25 itgmulc2 
 |-  ( ( ph /\ k e. B ) -> ( G x. S. A ( F x. H ) _d x ) = S. A ( G x. ( F x. H ) ) _d x )
27 26 eqcomd 
 |-  ( ( ph /\ k e. B ) -> S. A ( G x. ( F x. H ) ) _d x = ( G x. S. A ( F x. H ) _d x ) )
28 27 sumeq2dv 
 |-  ( ph -> sum_ k e. B S. A ( G x. ( F x. H ) ) _d x = sum_ k e. B ( G x. S. A ( F x. H ) _d x ) )