This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gsumxp

Description: Write a group sum over a cartesian product as a double sum. (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by AV, 9-Jun-2019)

Ref Expression
Hypotheses gsumxp.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsumxp.z ⊢ 0 = ( 0g ‘ 𝐺 )
gsumxp.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
gsumxp.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
gsumxp.r ⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
gsumxp.f ⊢ ( 𝜑 → 𝐹 : ( 𝐴 × 𝐶 ) ⟶ 𝐵 )
gsumxp.w ⊢ ( 𝜑 → 𝐹 finSupp 0 )
Assertion gsumxp ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝑗 ∈ 𝐴 ↦ ( 𝐺 Σg ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 gsumxp.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsumxp.z ⊢ 0 = ( 0g ‘ 𝐺 )
3 gsumxp.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4 gsumxp.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5 gsumxp.r ⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
6 gsumxp.f ⊢ ( 𝜑 → 𝐹 : ( 𝐴 × 𝐶 ) ⟶ 𝐵 )
7 gsumxp.w ⊢ ( 𝜑 → 𝐹 finSupp 0 )
8 4 5 xpexd ⊢ ( 𝜑 → ( 𝐴 × 𝐶 ) ∈ V )
9 relxp ⊢ Rel ( 𝐴 × 𝐶 )
10 9 a1i ⊢ ( 𝜑 → Rel ( 𝐴 × 𝐶 ) )
11 dmxpss ⊢ dom ( 𝐴 × 𝐶 ) ⊆ 𝐴
12 11 a1i ⊢ ( 𝜑 → dom ( 𝐴 × 𝐶 ) ⊆ 𝐴 )
13 1 2 3 8 10 4 12 6 7 gsum2d ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝑗 ∈ 𝐴 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( ( 𝐴 × 𝐶 ) “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) )
14 df-ima ⊢ ( ( 𝐴 × 𝐶 ) “ { 𝑗 } ) = ran ( ( 𝐴 × 𝐶 ) ↾ { 𝑗 } )
15 df-res ⊢ ( ( 𝐴 × 𝐶 ) ↾ { 𝑗 } ) = ( ( 𝐴 × 𝐶 ) ∩ ( { 𝑗 } × V ) )
16 inxp ⊢ ( ( 𝐴 × 𝐶 ) ∩ ( { 𝑗 } × V ) ) = ( ( 𝐴 ∩ { 𝑗 } ) × ( 𝐶 ∩ V ) )
17 15 16 eqtri ⊢ ( ( 𝐴 × 𝐶 ) ↾ { 𝑗 } ) = ( ( 𝐴 ∩ { 𝑗 } ) × ( 𝐶 ∩ V ) )
18 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝑗 ∈ 𝐴 )
19 18 snssd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → { 𝑗 } ⊆ 𝐴 )
20 sseqin2 ⊢ ( { 𝑗 } ⊆ 𝐴 ↔ ( 𝐴 ∩ { 𝑗 } ) = { 𝑗 } )
21 19 20 sylib ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝐴 ∩ { 𝑗 } ) = { 𝑗 } )
22 inv1 ⊢ ( 𝐶 ∩ V ) = 𝐶
23 22 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝐶 ∩ V ) = 𝐶 )
24 21 23 xpeq12d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝐴 ∩ { 𝑗 } ) × ( 𝐶 ∩ V ) ) = ( { 𝑗 } × 𝐶 ) )
25 17 24 eqtrid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝐴 × 𝐶 ) ↾ { 𝑗 } ) = ( { 𝑗 } × 𝐶 ) )
26 25 rneqd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ran ( ( 𝐴 × 𝐶 ) ↾ { 𝑗 } ) = ran ( { 𝑗 } × 𝐶 ) )
27 vex ⊢ 𝑗 ∈ V
28 27 snnz ⊢ { 𝑗 } ≠ ∅
29 rnxp ⊢ ( { 𝑗 } ≠ ∅ → ran ( { 𝑗 } × 𝐶 ) = 𝐶 )
30 28 29 ax-mp ⊢ ran ( { 𝑗 } × 𝐶 ) = 𝐶
31 26 30 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ran ( ( 𝐴 × 𝐶 ) ↾ { 𝑗 } ) = 𝐶 )
32 14 31 eqtrid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝐴 × 𝐶 ) “ { 𝑗 } ) = 𝐶 )
33 32 mpteq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝑘 ∈ ( ( 𝐴 × 𝐶 ) “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) = ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) )
34 33 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝐺 Σg ( 𝑘 ∈ ( ( 𝐴 × 𝐶 ) “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ) )
35 34 mpteq2dva ⊢ ( 𝜑 → ( 𝑗 ∈ 𝐴 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( ( 𝐴 × 𝐶 ) “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) = ( 𝑗 ∈ 𝐴 ↦ ( 𝐺 Σg ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) )
36 35 oveq2d ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑗 ∈ 𝐴 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( ( 𝐴 × 𝐶 ) “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) = ( 𝐺 Σg ( 𝑗 ∈ 𝐴 ↦ ( 𝐺 Σg ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) )
37 13 36 eqtrd ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝑗 ∈ 𝐴 ↦ ( 𝐺 Σg ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) )