Theorem gsumz

Description: Value of a group sum over the zero element. (Contributed by Mario Carneiro, 7-Dec-2014)

	Ref	Expression
Hypothesis	gsumz.z	⊢ 0 = ( 0g ‘ 𝐺 )
Assertion	gsumz	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉 ) → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 0 ) ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		gsumz.z	⊢ 0 = ( 0g ‘ 𝐺 )
2		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
3		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
4		eqid	⊢ { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑦 ) } = { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑦 ) }
5		simpl	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉 ) → 𝐺 ∈ Mnd )
6		simpr	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 )
7	1	fvexi	⊢ 0 ∈ V
8	7	snid	⊢ 0 ∈ { 0 }
9	2 1 3 4	gsumvallem2	⊢ ( 𝐺 ∈ Mnd → { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑦 ) } = { 0 } )
10	8 9	eleqtrrid	⊢ ( 𝐺 ∈ Mnd → 0 ∈ { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑦 ) } )
11	10	ad2antrr	⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑘 ∈ 𝐴 ) → 0 ∈ { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑦 ) } )
12	11	fmpttd	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉 ) → ( 𝑘 ∈ 𝐴 ↦ 0 ) : 𝐴 ⟶ { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑦 ) } )
13	2 1 3 4 5 6 12	gsumval1	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉 ) → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 0 ) ) = 0 )