Metamath Proof Explorer

Theorem gsummptfzcl

Description: Closure of a finite group sum over a finite set of sequential integers as map. (Contributed by AV, 14-Dec-2018)

Ref Expression
Hypotheses gsummptfzcl.b ⊢ B = Base G
gsummptfzcl.g ⊢ φ → G ∈ Mnd
gsummptfzcl.n ⊢ φ → N ∈ ℤ ≥ M
gsummptfzcl.i ⊢ φ → I = M … N
gsummptfzcl.e ⊢ φ → ∀ i ∈ I X ∈ B
Assertion gsummptfzcl ⊢ φ → ∑ G i ∈ I X ∈ B

Proof

Step Hyp Ref Expression
1 gsummptfzcl.b ⊢ B = Base G
2 gsummptfzcl.g ⊢ φ → G ∈ Mnd
3 gsummptfzcl.n ⊢ φ → N ∈ ℤ ≥ M
4 gsummptfzcl.i ⊢ φ → I = M … N
5 gsummptfzcl.e ⊢ φ → ∀ i ∈ I X ∈ B
6 eqid ⊢ + G = + G
7 eqid ⊢ i ∈ I ⟼ X = i ∈ I ⟼ X
8 7 fmpt ⊢ ∀ i ∈ I X ∈ B ↔ i ∈ I ⟼ X : I ⟶ B
9 4 feq2d ⊢ φ → i ∈ I ⟼ X : I ⟶ B ↔ i ∈ I ⟼ X : M … N ⟶ B
10 8 9 bitrid ⊢ φ → ∀ i ∈ I X ∈ B ↔ i ∈ I ⟼ X : M … N ⟶ B
11 5 10 mpbid ⊢ φ → i ∈ I ⟼ X : M … N ⟶ B
12 1 6 2 3 11 gsumval2 ⊢ φ → ∑ G i ∈ I X = seq M + G i ∈ I ⟼ X ⁡ N
13 5 adantr ⊢ φ ∧ x ∈ M … N → ∀ i ∈ I X ∈ B
14 13 8 sylib ⊢ φ ∧ x ∈ M … N → i ∈ I ⟼ X : I ⟶ B
15 4 eqcomd ⊢ φ → M … N = I
16 15 eleq2d ⊢ φ → x ∈ M … N ↔ x ∈ I
17 16 biimpa ⊢ φ ∧ x ∈ M … N → x ∈ I
18 14 17 ffvelcdmd ⊢ φ ∧ x ∈ M … N → i ∈ I ⟼ X ⁡ x ∈ B
19 2 adantr ⊢ φ ∧ x ∈ B ∧ y ∈ B → G ∈ Mnd
20 simprl ⊢ φ ∧ x ∈ B ∧ y ∈ B → x ∈ B
21 simprr ⊢ φ ∧ x ∈ B ∧ y ∈ B → y ∈ B
22 1 6 mndcl ⊢ G ∈ Mnd ∧ x ∈ B ∧ y ∈ B → x + G y ∈ B
23 19 20 21 22 syl3anc ⊢ φ ∧ x ∈ B ∧ y ∈ B → x + G y ∈ B
24 3 18 23 seqcl ⊢ φ → seq M + G i ∈ I ⟼ X ⁡ N ∈ B
25 12 24 eqeltrd ⊢ φ → ∑ G i ∈ I X ∈ B