gsumxp2

Description: Write a group sum over a cartesian product as a double sum in two ways. This corresponds to the first equation in Lang p. 6. (Contributed by AV, 27-Dec-2023)

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

Proof

Step	Hyp	Ref	Expression
1		gsumxp2.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		gsumxp2.z	⊢ 0 = ( 0_g ‘ 𝐺 )
3		gsumxp2.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4		gsumxp2.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5		gsumxp2.r	⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
6		gsumxp2.f	⊢ ( 𝜑 → 𝐹 : ( 𝐴 × 𝐶 ) ⟶ 𝐵 )
7		gsumxp2.w	⊢ ( 𝜑 → 𝐹 finSupp 0 )
8	6	fovcdmda	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ) → ( 𝑗 𝐹 𝑘 ) ∈ 𝐵 )
9	7	fsuppimpd	⊢ ( 𝜑 → ( 𝐹 supp 0 ) ∈ Fin )
10		simpl	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ) → 𝜑 )
11		opelxpi	⊢ ( ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) → ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐴 × 𝐶 ) )
12	11	ad2antlr	⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ) ∧ ¬ ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐹 supp 0 ) ) → ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐴 × 𝐶 ) )
13		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ) ∧ ¬ ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐹 supp 0 ) ) → ¬ ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐹 supp 0 ) )
14	12 13	eldifd	⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ) ∧ ¬ ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐹 supp 0 ) ) → ⟨ 𝑗 , 𝑘 ⟩ ∈ ( ( 𝐴 × 𝐶 ) ∖ ( 𝐹 supp 0 ) ) )
15		ssidd	⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ ( 𝐹 supp 0 ) )
16	4 5	xpexd	⊢ ( 𝜑 → ( 𝐴 × 𝐶 ) ∈ V )
17	2	fvexi	⊢ 0 ∈ V
18	17	a1i	⊢ ( 𝜑 → 0 ∈ V )
19	6 15 16 18	suppssr	⊢ ( ( 𝜑 ∧ ⟨ 𝑗 , 𝑘 ⟩ ∈ ( ( 𝐴 × 𝐶 ) ∖ ( 𝐹 supp 0 ) ) ) → ( 𝐹 ‘ ⟨ 𝑗 , 𝑘 ⟩ ) = 0 )
20	10 14 19	syl2an2r	⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ) ∧ ¬ ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐹 supp 0 ) ) → ( 𝐹 ‘ ⟨ 𝑗 , 𝑘 ⟩ ) = 0 )
21	20	ex	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ) → ( ¬ ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐹 supp 0 ) → ( 𝐹 ‘ ⟨ 𝑗 , 𝑘 ⟩ ) = 0 ) )
22		df-br	⊢ ( 𝑗 ( 𝐹 supp 0 ) 𝑘 ↔ ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐹 supp 0 ) )
23	22	notbii	⊢ ( ¬ 𝑗 ( 𝐹 supp 0 ) 𝑘 ↔ ¬ ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐹 supp 0 ) )
24		df-ov	⊢ ( 𝑗 𝐹 𝑘 ) = ( 𝐹 ‘ ⟨ 𝑗 , 𝑘 ⟩ )
25	24	eqeq1i	⊢ ( ( 𝑗 𝐹 𝑘 ) = 0 ↔ ( 𝐹 ‘ ⟨ 𝑗 , 𝑘 ⟩ ) = 0 )
26	21 23 25	3imtr4g	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ) → ( ¬ 𝑗 ( 𝐹 supp 0 ) 𝑘 → ( 𝑗 𝐹 𝑘 ) = 0 ) )
27	26	impr	⊢ ( ( 𝜑 ∧ ( ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ∧ ¬ 𝑗 ( 𝐹 supp 0 ) 𝑘 ) ) → ( 𝑗 𝐹 𝑘 ) = 0 )
28	1 2 3 4 5 8 9 27	gsumcom3	⊢ ( 𝜑 → ( 𝐺 Σ_g ( 𝑗 ∈ 𝐴 ↦ ( 𝐺 Σ_g ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) = ( 𝐺 Σ_g ( 𝑘 ∈ 𝐶 ↦ ( 𝐺 Σ_g ( 𝑗 ∈ 𝐴 ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) )
29	28	eqcomd	⊢ ( 𝜑 → ( 𝐺 Σ_g ( 𝑘 ∈ 𝐶 ↦ ( 𝐺 Σ_g ( 𝑗 ∈ 𝐴 ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) = ( 𝐺 Σ_g ( 𝑗 ∈ 𝐴 ↦ ( 𝐺 Σ_g ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) )

Metamath Proof Explorer

Theorem gsumxp2

Proof