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

Metamath Proof Explorer

Theorem gsumval1

Description: Value of the group sum operation when every element being summed is an identity of G . (Contributed by Mario Carneiro, 7-Dec-2014)

Ref Expression
Hypotheses gsumval1.b ⊢ B = Base G
gsumval1.z ⊢ 0 ˙ = 0 G
gsumval1.p ⊢ + ˙ = + G
gsumval1.o ⊢ O = x ∈ B | ∀ y ∈ B x + ˙ y = y ∧ y + ˙ x = y
gsumval1.g ⊢ φ → G ∈ V
gsumval1.a ⊢ φ → A ∈ W
gsumval1.f ⊢ φ → F : A ⟶ O
Assertion gsumval1 ⊢ φ → ∑ G F = 0 ˙

Proof

Step Hyp Ref Expression
1 gsumval1.b ⊢ B = Base G
2 gsumval1.z ⊢ 0 ˙ = 0 G
3 gsumval1.p ⊢ + ˙ = + G
4 gsumval1.o ⊢ O = x ∈ B | ∀ y ∈ B x + ˙ y = y ∧ y + ˙ x = y
5 gsumval1.g ⊢ φ → G ∈ V
6 gsumval1.a ⊢ φ → A ∈ W
7 gsumval1.f ⊢ φ → F : A ⟶ O
8 eqidd ⊢ φ → F -1 V ∖ O = F -1 V ∖ O
9 4 ssrab3 ⊢ O ⊆ B
10 fss ⊢ F : A ⟶ O ∧ O ⊆ B → F : A ⟶ B
11 7 9 10 sylancl ⊢ φ → F : A ⟶ B
12 1 2 3 4 8 5 6 11 gsumval ⊢ φ → ∑ G F = if ran ⁡ F ⊆ O 0 ˙ if A ∈ ran ⁡ … ι z | ∃ m ∃ n ∈ ℤ ≥ m A = m … n ∧ z = seq m + ˙ F ⁡ n ι z | ∃ f f : 1 … F -1 V ∖ O ⟶ 1-1 onto F -1 V ∖ O ∧ z = seq 1 + ˙ F ∘ f ⁡ F -1 V ∖ O
13 frn ⊢ F : A ⟶ O → ran ⁡ F ⊆ O
14 iftrue ⊢ ran ⁡ F ⊆ O → if ran ⁡ F ⊆ O 0 ˙ if A ∈ ran ⁡ … ι z | ∃ m ∃ n ∈ ℤ ≥ m A = m … n ∧ z = seq m + ˙ F ⁡ n ι z | ∃ f f : 1 … F -1 V ∖ O ⟶ 1-1 onto F -1 V ∖ O ∧ z = seq 1 + ˙ F ∘ f ⁡ F -1 V ∖ O = 0 ˙
15 7 13 14 3syl ⊢ φ → if ran ⁡ F ⊆ O 0 ˙ if A ∈ ran ⁡ … ι z | ∃ m ∃ n ∈ ℤ ≥ m A = m … n ∧ z = seq m + ˙ F ⁡ n ι z | ∃ f f : 1 … F -1 V ∖ O ⟶ 1-1 onto F -1 V ∖ O ∧ z = seq 1 + ˙ F ∘ f ⁡ F -1 V ∖ O = 0 ˙
16 12 15 eqtrd ⊢ φ → ∑ G F = 0 ˙