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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsummptfzcl.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
gsummptfzcl.n ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
gsummptfzcl.i ⊢ ( 𝜑 → 𝐼 = ( 𝑀 ... 𝑁 ) )
gsummptfzcl.e ⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝐼 𝑋 ∈ 𝐵 )
Assertion gsummptfzcl ( 𝜑 → ( 𝐺 Σg ( 𝑖 ∈ 𝐼 ↦ 𝑋 ) ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 gsummptfzcl.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsummptfzcl.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
3 gsummptfzcl.n ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
4 gsummptfzcl.i ⊢ ( 𝜑 → 𝐼 = ( 𝑀 ... 𝑁 ) )
5 gsummptfzcl.e ⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝐼 𝑋 ∈ 𝐵 )
6 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
7 eqid ⊢ ( 𝑖 ∈ 𝐼 ↦ 𝑋 ) = ( 𝑖 ∈ 𝐼 ↦ 𝑋 )
8 7 fmpt ⊢ ( ∀ 𝑖 ∈ 𝐼 𝑋 ∈ 𝐵 ↔ ( 𝑖 ∈ 𝐼 ↦ 𝑋 ) : 𝐼 ⟶ 𝐵 )
9 4 feq2d ⊢ ( 𝜑 → ( ( 𝑖 ∈ 𝐼 ↦ 𝑋 ) : 𝐼 ⟶ 𝐵 ↔ ( 𝑖 ∈ 𝐼 ↦ 𝑋 ) : ( 𝑀 ... 𝑁 ) ⟶ 𝐵 ) )
10 8 9 bitrid ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ 𝐼 𝑋 ∈ 𝐵 ↔ ( 𝑖 ∈ 𝐼 ↦ 𝑋 ) : ( 𝑀 ... 𝑁 ) ⟶ 𝐵 ) )
11 5 10 mpbid ⊢ ( 𝜑 → ( 𝑖 ∈ 𝐼 ↦ 𝑋 ) : ( 𝑀 ... 𝑁 ) ⟶ 𝐵 )
12 1 6 2 3 11 gsumval2 ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑖 ∈ 𝐼 ↦ 𝑋 ) ) = ( seq 𝑀 ( ( +g ‘ 𝐺 ) , ( 𝑖 ∈ 𝐼 ↦ 𝑋 ) ) ‘ 𝑁 ) )
13 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ∀ 𝑖 ∈ 𝐼 𝑋 ∈ 𝐵 )
14 13 8 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑖 ∈ 𝐼 ↦ 𝑋 ) : 𝐼 ⟶ 𝐵 )
15 4 eqcomd ⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) = 𝐼 )
16 15 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝑥 ∈ 𝐼 ) )
17 16 biimpa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑥 ∈ 𝐼 )
18 14 17 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑖 ∈ 𝐼 ↦ 𝑋 ) ‘ 𝑥 ) ∈ 𝐵 )
19 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐺 ∈ Mnd )
20 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
21 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
22 1 6 mndcl ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐵 )
23 19 20 21 22 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐵 )
24 3 18 23 seqcl ⊢ ( 𝜑 → ( seq 𝑀 ( ( +g ‘ 𝐺 ) , ( 𝑖 ∈ 𝐼 ↦ 𝑋 ) ) ‘ 𝑁 ) ∈ 𝐵 )
25 12 24 eqeltrd ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑖 ∈ 𝐼 ↦ 𝑋 ) ) ∈ 𝐵 )