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

Metamath Proof Explorer

Theorem gsumval

Description: Expand out the substitutions in df-gsum . (Contributed by Mario Carneiro, 7-Dec-2014)

Ref Expression
Hypotheses gsumval.b ⊢ B = Base G
gsumval.z ⊢ 0 ˙ = 0 G
gsumval.p ⊢ + ˙ = + G
gsumval.o ⊢ O = s ∈ B | ∀ t ∈ B s + ˙ t = t ∧ t + ˙ s = t
gsumval.w ⊢ φ → W = F -1 V ∖ O
gsumval.g ⊢ φ → G ∈ V
gsumval.a ⊢ φ → A ∈ X
gsumval.f ⊢ φ → F : A ⟶ B
Assertion gsumval ⊢ φ → ∑ G F = if ran ⁡ F ⊆ O 0 ˙ if A ∈ ran ⁡ … ι x | ∃ m ∃ n ∈ ℤ ≥ m A = m … n ∧ x = seq m + ˙ F ⁡ n ι x | ∃ f f : 1 … W ⟶ 1-1 onto W ∧ x = seq 1 + ˙ F ∘ f ⁡ W

Proof

Step Hyp Ref Expression
1 gsumval.b ⊢ B = Base G
2 gsumval.z ⊢ 0 ˙ = 0 G
3 gsumval.p ⊢ + ˙ = + G
4 gsumval.o ⊢ O = s ∈ B | ∀ t ∈ B s + ˙ t = t ∧ t + ˙ s = t
5 gsumval.w ⊢ φ → W = F -1 V ∖ O
6 gsumval.g ⊢ φ → G ∈ V
7 gsumval.a ⊢ φ → A ∈ X
8 gsumval.f ⊢ φ → F : A ⟶ B
9 1 fvexi ⊢ B ∈ V
10 9 a1i ⊢ φ → B ∈ V
11 fex2 ⊢ F : A ⟶ B ∧ A ∈ X ∧ B ∈ V → F ∈ V
12 8 7 10 11 syl3anc ⊢ φ → F ∈ V
13 8 fdmd ⊢ φ → dom ⁡ F = A
14 1 2 3 4 5 6 12 13 gsumvalx ⊢ φ → ∑ G F = if ran ⁡ F ⊆ O 0 ˙ if A ∈ ran ⁡ … ι x | ∃ m ∃ n ∈ ℤ ≥ m A = m … n ∧ x = seq m + ˙ F ⁡ n ι x | ∃ f f : 1 … W ⟶ 1-1 onto W ∧ x = seq 1 + ˙ F ∘ f ⁡ W