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	$⊢ (φ \land x \in A) \to F \in ℂ$
	3factsumint2.2	$⊢ (φ \land k \in B) \to G \in ℂ$
	3factsumint2.3	$⊢ (φ \land (x \in A \land k \in B)) \to H \in ℂ$
Assertion	3factsumint2	$⊢ φ \to \sum_{k \in B} \int_{A} F G H d x = \sum_{k \in B} \int_{A} G F H d x$

Step	Hyp	Ref	Expression
1		3factsumint2.1	$⊢ (φ \land x \in A) \to F \in ℂ$
2		3factsumint2.2	$⊢ (φ \land k \in B) \to G \in ℂ$
3		3factsumint2.3	$⊢ (φ \land (x \in A \land k \in B)) \to H \in ℂ$
4	1	adantlr	$⊢ ((φ \land k \in B) \land x \in A) \to F \in ℂ$
5	2	adantr	$⊢ ((φ \land k \in B) \land x \in A) \to G \in ℂ$
6		ancom	$⊢ (x \in A \land k \in B) \leftrightarrow (k \in B \land x \in A)$
7	6	anbi2i	$⊢ (φ \land (x \in A \land k \in B)) \leftrightarrow (φ \land (k \in B \land x \in A))$
8		anass	$⊢ ((φ \land k \in B) \land x \in A) \leftrightarrow (φ \land (k \in B \land x \in A))$
9	8	bicomi	$⊢ (φ \land (k \in B \land x \in A)) \leftrightarrow ((φ \land k \in B) \land x \in A)$
10	7 9	bitri	$⊢ (φ \land (x \in A \land k \in B)) \leftrightarrow ((φ \land k \in B) \land x \in A)$
11	10	imbi1i	$⊢ ((φ \land (x \in A \land k \in B)) \to H \in ℂ) \leftrightarrow (((φ \land k \in B) \land x \in A) \to H \in ℂ)$
12	3 11	mpbi	$⊢ ((φ \land k \in B) \land x \in A) \to H \in ℂ$
13	4 5 12	mul12d	$⊢ ((φ \land k \in B) \land x \in A) \to F G H = G F H$
14	13	itgeq2dv	$⊢ (φ \land k \in B) \to \int_{A} F G H d x = \int_{A} G F H d x$
15	14	sumeq2dv	$⊢ φ \to \sum_{k \in B} \int_{A} F G H d x = \sum_{k \in B} \int_{A} G F H d x$

Metamath Proof Explorer