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	⊢ ( 𝜑 → 𝐵 ∈ Fin )
	3factsumint4.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐹 ∈ ℂ )
	3factsumint4.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐺 ∈ ℂ )
	3factsumint4.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐻 ∈ ℂ )
Assertion	3factsumint4	⊢ ( 𝜑 → ∫ 𝐴 Σ 𝑘 ∈ 𝐵 ( 𝐹 · ( 𝐺 · 𝐻 ) ) d 𝑥 = ∫ 𝐴 ( 𝐹 · Σ 𝑘 ∈ 𝐵 ( 𝐺 · 𝐻 ) ) d 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		3factsumint4.1	⊢ ( 𝜑 → 𝐵 ∈ Fin )
2		3factsumint4.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐹 ∈ ℂ )
3		3factsumint4.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐺 ∈ ℂ )
4		3factsumint4.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐻 ∈ ℂ )
5	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ Fin )
6	3	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → 𝐺 ∈ ℂ )
7		anass	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) ↔ ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) )
8	7	bicomi	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) ↔ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) )
9	8	imbi1i	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐻 ∈ ℂ ) ↔ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → 𝐻 ∈ ℂ ) )
10	4 9	mpbi	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → 𝐻 ∈ ℂ )
11	6 10	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → ( 𝐺 · 𝐻 ) ∈ ℂ )
12	5 2 11	fsummulc2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 · Σ 𝑘 ∈ 𝐵 ( 𝐺 · 𝐻 ) ) = Σ 𝑘 ∈ 𝐵 ( 𝐹 · ( 𝐺 · 𝐻 ) ) )
13	12	eqcomd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → Σ 𝑘 ∈ 𝐵 ( 𝐹 · ( 𝐺 · 𝐻 ) ) = ( 𝐹 · Σ 𝑘 ∈ 𝐵 ( 𝐺 · 𝐻 ) ) )
14	13	itgeq2dv	⊢ ( 𝜑 → ∫ 𝐴 Σ 𝑘 ∈ 𝐵 ( 𝐹 · ( 𝐺 · 𝐻 ) ) d 𝑥 = ∫ 𝐴 ( 𝐹 · Σ 𝑘 ∈ 𝐵 ( 𝐺 · 𝐻 ) ) d 𝑥 )