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	$⊢ φ \to L \in ℝ$
	3factsumint3.3	$⊢ φ \to U \in ℝ$
	3factsumint3.4	$⊢ (φ \land x \in A) \to F \in ℂ$
	3factsumint3.5	$⊢ φ \to (x \in A ⟼ F) : A \underset{cn}{⟶} ℂ$
	3factsumint3.6	$⊢ (φ \land k \in B) \to G \in ℂ$
	3factsumint3.7	$⊢ (φ \land (x \in A \land k \in B)) \to H \in ℂ$
	3factsumint3.8	$⊢ (φ \land k \in B) \to (x \in A ⟼ H) : A \underset{cn}{⟶} ℂ$
Assertion	3factsumint3	$⊢ φ \to \sum_{k \in B} \int_{A} G F H d x = \sum_{k \in B} G \int_{A} F H d x$

Proof

Step	Hyp	Ref	Expression
1		3factsumint3.1	$⊢ A = [L, U]$
2		3factsumint3.2	$⊢ φ \to L \in ℝ$
3		3factsumint3.3	$⊢ φ \to U \in ℝ$
4		3factsumint3.4	$⊢ (φ \land x \in A) \to F \in ℂ$
5		3factsumint3.5	$⊢ φ \to (x \in A ⟼ F) : A \underset{cn}{⟶} ℂ$
6		3factsumint3.6	$⊢ (φ \land k \in B) \to G \in ℂ$
7		3factsumint3.7	$⊢ (φ \land (x \in A \land k \in B)) \to H \in ℂ$
8		3factsumint3.8	$⊢ (φ \land k \in B) \to (x \in A ⟼ H) : A \underset{cn}{⟶} ℂ$
9	4	adantlr	$⊢ ((φ \land k \in B) \land x \in A) \to F \in ℂ$
10		ancom	$⊢ (x \in A \land k \in B) \leftrightarrow (k \in B \land x \in A)$
11	10	anbi2i	$⊢ (φ \land (x \in A \land k \in B)) \leftrightarrow (φ \land (k \in B \land x \in A))$
12		anass	$⊢ ((φ \land k \in B) \land x \in A) \leftrightarrow (φ \land (k \in B \land x \in A))$
13	12	bicomi	$⊢ (φ \land (k \in B \land x \in A)) \leftrightarrow ((φ \land k \in B) \land x \in A)$
14	11 13	bitri	$⊢ (φ \land (x \in A \land k \in B)) \leftrightarrow ((φ \land k \in B) \land x \in A)$
15	14	imbi1i	$⊢ ((φ \land (x \in A \land k \in B)) \to H \in ℂ) \leftrightarrow (((φ \land k \in B) \land x \in A) \to H \in ℂ)$
16	7 15	mpbi	$⊢ ((φ \land k \in B) \land x \in A) \to H \in ℂ$
17	9 16	mulcld	$⊢ ((φ \land k \in B) \land x \in A) \to F H \in ℂ$
18	2	adantr	$⊢ (φ \land k \in B) \to L \in ℝ$
19	3	adantr	$⊢ (φ \land k \in B) \to U \in ℝ$
20	5	adantr	$⊢ (φ \land k \in B) \to (x \in A ⟼ F) : A \underset{cn}{⟶} ℂ$
21	20 8	mulcncf	$⊢ (φ \land k \in B) \to (x \in A ⟼ F H) : A \underset{cn}{⟶} ℂ$
22	1	oveq1i	$⊢ A \underset{cn}{⟶} ℂ = [L, U] \underset{cn}{⟶} ℂ$
23	21 22	eleqtrdi	$⊢ (φ \land k \in B) \to (x \in A ⟼ F H) : [L, U] \underset{cn}{⟶} ℂ$
24		cnicciblnc	$⊢ (L \in ℝ \land U \in ℝ \land (x \in A ⟼ F H) : [L, U] \underset{cn}{⟶} ℂ) \to (x \in A ⟼ F H) \in 𝐿^{1}$
25	18 19 23 24	syl3anc	$⊢ (φ \land k \in B) \to (x \in A ⟼ F H) \in 𝐿^{1}$
26	6 17 25	itgmulc2	$⊢ (φ \land k \in B) \to G \int_{A} F H d x = \int_{A} G F H d x$
27	26	eqcomd	$⊢ (φ \land k \in B) \to \int_{A} G F H d x = G \int_{A} F H d x$
28	27	sumeq2dv	$⊢ φ \to \sum_{k \in B} \int_{A} G F H d x = \sum_{k \in B} G \int_{A} F H d x$

Metamath Proof Explorer

Theorem 3factsumint3

Proof