Metamath Proof Explorer

Theorem 3factsumint1

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

Ref Expression
Hypotheses 3factsumint1.1 ⊢ 𝐴 = ( 𝐿 [,] 𝑈 )
3factsumint1.2 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
3factsumint1.3 ⊢ ( 𝜑 → 𝐿 ∈ ℝ )
3factsumint1.4 ⊢ ( 𝜑 → 𝑈 ∈ ℝ )
3factsumint1.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐹 ∈ ℂ )
3factsumint1.6 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ∈ ( 𝐴 –cn→ ℂ ) )
3factsumint1.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐺 ∈ ℂ )
3factsumint1.8 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐻 ∈ ℂ )
3factsumint1.9 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐻 ) ∈ ( 𝐴 –cn→ ℂ ) )
Assertion 3factsumint1 ( 𝜑 → ∫ 𝐴 Σ 𝑘 ∈ 𝐵 ( 𝐹 · ( 𝐺 · 𝐻 ) ) d 𝑥 = Σ 𝑘 ∈ 𝐵 ∫ 𝐴 ( 𝐹 · ( 𝐺 · 𝐻 ) ) d 𝑥 )

Proof

Step Hyp Ref Expression
1 3factsumint1.1 ⊢ 𝐴 = ( 𝐿 [,] 𝑈 )
2 3factsumint1.2 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
3 3factsumint1.3 ⊢ ( 𝜑 → 𝐿 ∈ ℝ )
4 3factsumint1.4 ⊢ ( 𝜑 → 𝑈 ∈ ℝ )
5 3factsumint1.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐹 ∈ ℂ )
6 3factsumint1.6 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ∈ ( 𝐴 –cn→ ℂ ) )
7 3factsumint1.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐺 ∈ ℂ )
8 3factsumint1.8 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐻 ∈ ℂ )
9 3factsumint1.9 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐻 ) ∈ ( 𝐴 –cn→ ℂ ) )
10 iccmbl ⊢ ( ( 𝐿 ∈ ℝ ∧ 𝑈 ∈ ℝ ) → ( 𝐿 [,] 𝑈 ) ∈ dom vol )
11 3 4 10 syl2anc ⊢ ( 𝜑 → ( 𝐿 [,] 𝑈 ) ∈ dom vol )
12 1 11 eqeltrid ⊢ ( 𝜑 → 𝐴 ∈ dom vol )
13 5 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐹 ∈ ℂ )
14 7 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐺 ∈ ℂ )
15 14 8 mulcld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → ( 𝐺 · 𝐻 ) ∈ ℂ )
16 13 15 mulcld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → ( 𝐹 · ( 𝐺 · 𝐻 ) ) ∈ ℂ )
17 ovex ⊢ ( 𝐿 [,] 𝑈 ) ∈ V
18 1 17 eqeltri ⊢ 𝐴 ∈ V
19 18 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐴 ∈ V )
20 13 anass1rs ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐹 ∈ ℂ )
21 15 anass1rs ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 · 𝐻 ) ∈ ℂ )
22 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) )
23 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ ( 𝐺 · 𝐻 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐺 · 𝐻 ) ) )
24 19 20 21 22 23 offval2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( 𝐺 · 𝐻 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 · ( 𝐺 · 𝐻 ) ) ) )
25 cnmbf ⊢ ( ( 𝐴 ∈ dom vol ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ∈ ( 𝐴 –cn→ ℂ ) ) → ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ∈ MblFn )
26 12 6 25 syl2anc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ∈ MblFn )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ∈ MblFn )
28 8 anass1rs ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐻 ∈ ℂ )
29 3 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐿 ∈ ℝ )
30 4 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝑈 ∈ ℝ )
31 1 oveq1i ⊢ ( 𝐴 –cn→ ℂ ) = ( ( 𝐿 [,] 𝑈 ) –cn→ ℂ )
32 31 eleq2i ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐻 ) ∈ ( 𝐴 –cn→ ℂ ) ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐻 ) ∈ ( ( 𝐿 [,] 𝑈 ) –cn→ ℂ ) )
33 9 32 sylib ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐻 ) ∈ ( ( 𝐿 [,] 𝑈 ) –cn→ ℂ ) )
34 cnicciblnc ⊢ ( ( 𝐿 ∈ ℝ ∧ 𝑈 ∈ ℝ ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐻 ) ∈ ( ( 𝐿 [,] 𝑈 ) –cn→ ℂ ) ) → ( 𝑥 ∈ 𝐴 ↦ 𝐻 ) ∈ 𝐿1 )
35 29 30 33 34 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐻 ) ∈ 𝐿1 )
36 7 28 35 iblmulc2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ ( 𝐺 · 𝐻 ) ) ∈ 𝐿1 )
37 31 eleq2i ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ∈ ( 𝐴 –cn→ ℂ ) ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ∈ ( ( 𝐿 [,] 𝑈 ) –cn→ ℂ ) )
38 6 37 sylib ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ∈ ( ( 𝐿 [,] 𝑈 ) –cn→ ℂ ) )
39 cniccbdd ⊢ ( ( 𝐿 ∈ ℝ ∧ 𝑈 ∈ ℝ ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ∈ ( ( 𝐿 [,] 𝑈 ) –cn→ ℂ ) ) → ∃ 𝑞 ∈ ℝ ∀ 𝑟 ∈ ( 𝐿 [,] 𝑈 ) ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ‘ 𝑟 ) ) ≤ 𝑞 )
40 3 4 38 39 syl3anc ⊢ ( 𝜑 → ∃ 𝑞 ∈ ℝ ∀ 𝑟 ∈ ( 𝐿 [,] 𝑈 ) ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ‘ 𝑟 ) ) ≤ 𝑞 )
41 40 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ∃ 𝑞 ∈ ℝ ∀ 𝑟 ∈ ( 𝐿 [,] 𝑈 ) ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ‘ 𝑟 ) ) ≤ 𝑞 )
42 5 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐹 ∈ ℂ )
43 dmmptg ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐹 ∈ ℂ → dom ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) = 𝐴 )
44 42 43 syl ⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) = 𝐴 )
45 44 1 eqtrdi ⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) = ( 𝐿 [,] 𝑈 ) )
46 45 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑟 ∈ dom ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ‘ 𝑟 ) ) ≤ 𝑞 ↔ ∀ 𝑟 ∈ ( 𝐿 [,] 𝑈 ) ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ‘ 𝑟 ) ) ≤ 𝑞 ) )
47 46 rexbidv ⊢ ( 𝜑 → ( ∃ 𝑞 ∈ ℝ ∀ 𝑟 ∈ dom ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ‘ 𝑟 ) ) ≤ 𝑞 ↔ ∃ 𝑞 ∈ ℝ ∀ 𝑟 ∈ ( 𝐿 [,] 𝑈 ) ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ‘ 𝑟 ) ) ≤ 𝑞 ) )
48 47 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( ∃ 𝑞 ∈ ℝ ∀ 𝑟 ∈ dom ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ‘ 𝑟 ) ) ≤ 𝑞 ↔ ∃ 𝑞 ∈ ℝ ∀ 𝑟 ∈ ( 𝐿 [,] 𝑈 ) ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ‘ 𝑟 ) ) ≤ 𝑞 ) )
49 41 48 mpbird ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ∃ 𝑞 ∈ ℝ ∀ 𝑟 ∈ dom ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ‘ 𝑟 ) ) ≤ 𝑞 )
50 bddmulibl ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ ( 𝐺 · 𝐻 ) ) ∈ 𝐿1 ∧ ∃ 𝑞 ∈ ℝ ∀ 𝑟 ∈ dom ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ‘ 𝑟 ) ) ≤ 𝑞 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( 𝐺 · 𝐻 ) ) ) ∈ 𝐿1 )
51 27 36 49 50 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( 𝐺 · 𝐻 ) ) ) ∈ 𝐿1 )
52 24 51 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 · ( 𝐺 · 𝐻 ) ) ) ∈ 𝐿1 )
53 12 2 16 52 itgfsum ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝐵 ( 𝐹 · ( 𝐺 · 𝐻 ) ) ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝐵 ( 𝐹 · ( 𝐺 · 𝐻 ) ) d 𝑥 = Σ 𝑘 ∈ 𝐵 ∫ 𝐴 ( 𝐹 · ( 𝐺 · 𝐻 ) ) d 𝑥 ) )
54 53 simprd ⊢ ( 𝜑 → ∫ 𝐴 Σ 𝑘 ∈ 𝐵 ( 𝐹 · ( 𝐺 · 𝐻 ) ) d 𝑥 = Σ 𝑘 ∈ 𝐵 ∫ 𝐴 ( 𝐹 · ( 𝐺 · 𝐻 ) ) d 𝑥 )