Metamath Proof Explorer


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

Proof

Step Hyp Ref Expression
1 3factsumint2.1 ( ( 𝜑𝑥𝐴 ) → 𝐹 ∈ ℂ )
2 3factsumint2.2 ( ( 𝜑𝑘𝐵 ) → 𝐺 ∈ ℂ )
3 3factsumint2.3 ( ( 𝜑 ∧ ( 𝑥𝐴𝑘𝐵 ) ) → 𝐻 ∈ ℂ )
4 1 adantlr ( ( ( 𝜑𝑘𝐵 ) ∧ 𝑥𝐴 ) → 𝐹 ∈ ℂ )
5 2 adantr ( ( ( 𝜑𝑘𝐵 ) ∧ 𝑥𝐴 ) → 𝐺 ∈ ℂ )
6 ancom ( ( 𝑥𝐴𝑘𝐵 ) ↔ ( 𝑘𝐵𝑥𝐴 ) )
7 6 anbi2i ( ( 𝜑 ∧ ( 𝑥𝐴𝑘𝐵 ) ) ↔ ( 𝜑 ∧ ( 𝑘𝐵𝑥𝐴 ) ) )
8 anass ( ( ( 𝜑𝑘𝐵 ) ∧ 𝑥𝐴 ) ↔ ( 𝜑 ∧ ( 𝑘𝐵𝑥𝐴 ) ) )
9 8 bicomi ( ( 𝜑 ∧ ( 𝑘𝐵𝑥𝐴 ) ) ↔ ( ( 𝜑𝑘𝐵 ) ∧ 𝑥𝐴 ) )
10 7 9 bitri ( ( 𝜑 ∧ ( 𝑥𝐴𝑘𝐵 ) ) ↔ ( ( 𝜑𝑘𝐵 ) ∧ 𝑥𝐴 ) )
11 10 imbi1i ( ( ( 𝜑 ∧ ( 𝑥𝐴𝑘𝐵 ) ) → 𝐻 ∈ ℂ ) ↔ ( ( ( 𝜑𝑘𝐵 ) ∧ 𝑥𝐴 ) → 𝐻 ∈ ℂ ) )
12 3 11 mpbi ( ( ( 𝜑𝑘𝐵 ) ∧ 𝑥𝐴 ) → 𝐻 ∈ ℂ )
13 4 5 12 mul12d ( ( ( 𝜑𝑘𝐵 ) ∧ 𝑥𝐴 ) → ( 𝐹 · ( 𝐺 · 𝐻 ) ) = ( 𝐺 · ( 𝐹 · 𝐻 ) ) )
14 13 itgeq2dv ( ( 𝜑𝑘𝐵 ) → ∫ 𝐴 ( 𝐹 · ( 𝐺 · 𝐻 ) ) d 𝑥 = ∫ 𝐴 ( 𝐺 · ( 𝐹 · 𝐻 ) ) d 𝑥 )
15 14 sumeq2dv ( 𝜑 → Σ 𝑘𝐵𝐴 ( 𝐹 · ( 𝐺 · 𝐻 ) ) d 𝑥 = Σ 𝑘𝐵𝐴 ( 𝐺 · ( 𝐹 · 𝐻 ) ) d 𝑥 )