Metamath Proof Explorer


Theorem fsumxp

Description: Combine two sums into a single sum over the cartesian product. (Contributed by Mario Carneiro, 23-Apr-2014)

Ref Expression
Hypotheses fsumxp.1 ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → 𝐷 = 𝐶 )
fsumxp.2 ( 𝜑𝐴 ∈ Fin )
fsumxp.3 ( 𝜑𝐵 ∈ Fin )
fsumxp.4 ( ( 𝜑 ∧ ( 𝑗𝐴𝑘𝐵 ) ) → 𝐶 ∈ ℂ )
Assertion fsumxp ( 𝜑 → Σ 𝑗𝐴 Σ 𝑘𝐵 𝐶 = Σ 𝑧 ∈ ( 𝐴 × 𝐵 ) 𝐷 )

Proof

Step Hyp Ref Expression
1 fsumxp.1 ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → 𝐷 = 𝐶 )
2 fsumxp.2 ( 𝜑𝐴 ∈ Fin )
3 fsumxp.3 ( 𝜑𝐵 ∈ Fin )
4 fsumxp.4 ( ( 𝜑 ∧ ( 𝑗𝐴𝑘𝐵 ) ) → 𝐶 ∈ ℂ )
5 3 adantr ( ( 𝜑𝑗𝐴 ) → 𝐵 ∈ Fin )
6 1 2 5 4 fsum2d ( 𝜑 → Σ 𝑗𝐴 Σ 𝑘𝐵 𝐶 = Σ 𝑧 𝑗𝐴 ( { 𝑗 } × 𝐵 ) 𝐷 )
7 iunxpconst 𝑗𝐴 ( { 𝑗 } × 𝐵 ) = ( 𝐴 × 𝐵 )
8 7 sumeq1i Σ 𝑧 𝑗𝐴 ( { 𝑗 } × 𝐵 ) 𝐷 = Σ 𝑧 ∈ ( 𝐴 × 𝐵 ) 𝐷
9 6 8 eqtrdi ( 𝜑 → Σ 𝑗𝐴 Σ 𝑘𝐵 𝐶 = Σ 𝑧 ∈ ( 𝐴 × 𝐵 ) 𝐷 )