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	syl5eq	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝐴 × 𝐶 ) ↾ { 𝑗 } ) = ( { 𝑗 } × 𝐶 ) )
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	syl5eq	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝐴 × 𝐶 ) “ { 𝑗 } ) = 𝐶 )
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 ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) )