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	⊢ 𝐴 = ( 𝐿 [,] 𝑈 )
	3factsumint3.2	⊢ ( 𝜑 → 𝐿 ∈ ℝ )
	3factsumint3.3	⊢ ( 𝜑 → 𝑈 ∈ ℝ )
	3factsumint3.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐹 ∈ ℂ )
	3factsumint3.5	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ∈ ( 𝐴 –cn→ ℂ ) )
	3factsumint3.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐺 ∈ ℂ )
	3factsumint3.7	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐻 ∈ ℂ )
	3factsumint3.8	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐻 ) ∈ ( 𝐴 –cn→ ℂ ) )
Assertion	3factsumint3	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐵 ∫ 𝐴 ( 𝐺 · ( 𝐹 · 𝐻 ) ) d 𝑥 = Σ 𝑘 ∈ 𝐵 ( 𝐺 · ∫ 𝐴 ( 𝐹 · 𝐻 ) d 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		3factsumint3.1	⊢ 𝐴 = ( 𝐿 [,] 𝑈 )
2		3factsumint3.2	⊢ ( 𝜑 → 𝐿 ∈ ℝ )
3		3factsumint3.3	⊢ ( 𝜑 → 𝑈 ∈ ℝ )
4		3factsumint3.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐹 ∈ ℂ )
5		3factsumint3.5	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ∈ ( 𝐴 –cn→ ℂ ) )
6		3factsumint3.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐺 ∈ ℂ )
7		3factsumint3.7	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐻 ∈ ℂ )
8		3factsumint3.8	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐻 ) ∈ ( 𝐴 –cn→ ℂ ) )
9	4	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐹 ∈ ℂ )
10		ancom	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ↔ ( 𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) )
11	10	anbi2i	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) ↔ ( 𝜑 ∧ ( 𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ) )
12		anass	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝜑 ∧ ( 𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ) )
13	12	bicomi	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ) ↔ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) )
14	11 13	bitri	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) ↔ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) )
15	14	imbi1i	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐻 ∈ ℂ ) ↔ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐻 ∈ ℂ ) )
16	7 15	mpbi	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐻 ∈ ℂ )
17	9 16	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 · 𝐻 ) ∈ ℂ )
18	2	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐿 ∈ ℝ )
19	3	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝑈 ∈ ℝ )
20	5	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ∈ ( 𝐴 –cn→ ℂ ) )
21	20 8	mulcncf	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 · 𝐻 ) ) ∈ ( 𝐴 –cn→ ℂ ) )
22	1	oveq1i	⊢ ( 𝐴 –cn→ ℂ ) = ( ( 𝐿 [,] 𝑈 ) –cn→ ℂ )
23	21 22	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 · 𝐻 ) ) ∈ ( ( 𝐿 [,] 𝑈 ) –cn→ ℂ ) )
24		cnicciblnc	⊢ ( ( 𝐿 ∈ ℝ ∧ 𝑈 ∈ ℝ ∧ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 · 𝐻 ) ) ∈ ( ( 𝐿 [,] 𝑈 ) –cn→ ℂ ) ) → ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 · 𝐻 ) ) ∈ 𝐿¹ )
25	18 19 23 24	syl3anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 · 𝐻 ) ) ∈ 𝐿¹ )
26	6 17 25	itgmulc2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝐺 · ∫ 𝐴 ( 𝐹 · 𝐻 ) d 𝑥 ) = ∫ 𝐴 ( 𝐺 · ( 𝐹 · 𝐻 ) ) d 𝑥 )
27	26	eqcomd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ∫ 𝐴 ( 𝐺 · ( 𝐹 · 𝐻 ) ) d 𝑥 = ( 𝐺 · ∫ 𝐴 ( 𝐹 · 𝐻 ) d 𝑥 ) )
28	27	sumeq2dv	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐵 ∫ 𝐴 ( 𝐺 · ( 𝐹 · 𝐻 ) ) d 𝑥 = Σ 𝑘 ∈ 𝐵 ( 𝐺 · ∫ 𝐴 ( 𝐹 · 𝐻 ) d 𝑥 ) )

Metamath Proof Explorer

Theorem 3factsumint3

Proof