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

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 )