Theorem 3factsumint2

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

	Ref	Expression
Hypotheses	3factsumint2.1	|- ( ( ph /\ x e. A ) -> F e. CC )
	3factsumint2.2	|- ( ( ph /\ k e. B ) -> G e. CC )
	3factsumint2.3	|- ( ( ph /\ ( x e. A /\ k e. B ) ) -> H e. CC )
Assertion	3factsumint2	|- ( ph -> sum_ k e. B S. A ( F x. ( G x. H ) ) _d x = sum_ k e. B S. A ( G x. ( F x. H ) ) _d x )

Proof

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