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	|- ( ph -> B e. Fin )
	3factsumint4.2	|- ( ( ph /\ x e. A ) -> F e. CC )
	3factsumint4.3	|- ( ( ph /\ k e. B ) -> G e. CC )
	3factsumint4.4	|- ( ( ph /\ ( x e. A /\ k e. B ) ) -> H e. CC )
Assertion	3factsumint4	|- ( ph -> S. A sum_ k e. B ( F x. ( G x. H ) ) _d x = S. A ( F x. sum_ k e. B ( G x. H ) ) _d x )

Proof

Step	Hyp	Ref	Expression
1		3factsumint4.1	|- ( ph -> B e. Fin )
2		3factsumint4.2	|- ( ( ph /\ x e. A ) -> F e. CC )
3		3factsumint4.3	|- ( ( ph /\ k e. B ) -> G e. CC )
4		3factsumint4.4	|- ( ( ph /\ ( x e. A /\ k e. B ) ) -> H e. CC )
5	1	adantr	|- ( ( ph /\ x e. A ) -> B e. Fin )
6	3	adantlr	|- ( ( ( ph /\ x e. A ) /\ k e. B ) -> G e. CC )
7		anass	|- ( ( ( ph /\ x e. A ) /\ k e. B ) <-> ( ph /\ ( x e. A /\ k e. B ) ) )
8	7	bicomi	|- ( ( ph /\ ( x e. A /\ k e. B ) ) <-> ( ( ph /\ x e. A ) /\ k e. B ) )
9	8	imbi1i	|- ( ( ( ph /\ ( x e. A /\ k e. B ) ) -> H e. CC ) <-> ( ( ( ph /\ x e. A ) /\ k e. B ) -> H e. CC ) )
10	4 9	mpbi	|- ( ( ( ph /\ x e. A ) /\ k e. B ) -> H e. CC )
11	6 10	mulcld	|- ( ( ( ph /\ x e. A ) /\ k e. B ) -> ( G x. H ) e. CC )
12	5 2 11	fsummulc2	|- ( ( ph /\ x e. A ) -> ( F x. sum_ k e. B ( G x. H ) ) = sum_ k e. B ( F x. ( G x. H ) ) )
13	12	eqcomd	|- ( ( ph /\ x e. A ) -> sum_ k e. B ( F x. ( G x. H ) ) = ( F x. sum_ k e. B ( G x. H ) ) )
14	13	itgeq2dv	|- ( ph -> S. A sum_ k e. B ( F x. ( G x. H ) ) _d x = S. A ( F x. sum_ k e. B ( G x. H ) ) _d x )