Metamath Proof Explorer


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 )