Metamath Proof Explorer

Theorem gsumconst

Description: Sum of a constant series. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by Mario Carneiro, 24-Apr-2016)

Ref Expression
Hypotheses gsumconst.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsumconst.m ⊢ · = ( .g ‘ 𝐺 )
Assertion gsumconst ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) = ( ( ♯ ‘ 𝐴 ) · 𝑋 ) )

Proof

Step Hyp Ref Expression
1 gsumconst.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsumconst.m ⊢ · = ( .g ‘ 𝐺 )
3 simpl3 ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ 𝐴 = ∅ ) → 𝑋 ∈ 𝐵 )
4 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
5 1 4 2 mulg0 ⊢ ( 𝑋 ∈ 𝐵 → ( 0 · 𝑋 ) = ( 0g ‘ 𝐺 ) )
6 3 5 syl ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ 𝐴 = ∅ ) → ( 0 · 𝑋 ) = ( 0g ‘ 𝐺 ) )
7 fveq2 ⊢ ( 𝐴 = ∅ → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ ∅ ) )
8 7 adantl ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ 𝐴 = ∅ ) → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ ∅ ) )
9 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
10 8 9 eqtrdi ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ 𝐴 = ∅ ) → ( ♯ ‘ 𝐴 ) = 0 )
11 10 oveq1d ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ 𝐴 = ∅ ) → ( ( ♯ ‘ 𝐴 ) · 𝑋 ) = ( 0 · 𝑋 ) )
12 mpteq1 ⊢ ( 𝐴 = ∅ → ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) = ( 𝑘 ∈ ∅ ↦ 𝑋 ) )
13 12 adantl ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ 𝐴 = ∅ ) → ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) = ( 𝑘 ∈ ∅ ↦ 𝑋 ) )
14 mpt0 ⊢ ( 𝑘 ∈ ∅ ↦ 𝑋 ) = ∅
15 13 14 eqtrdi ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ 𝐴 = ∅ ) → ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) = ∅ )
16 15 oveq2d ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ 𝐴 = ∅ ) → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) = ( 𝐺 Σg ∅ ) )
17 4 gsum0 ⊢ ( 𝐺 Σg ∅ ) = ( 0g ‘ 𝐺 )
18 16 17 eqtrdi ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ 𝐴 = ∅ ) → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) = ( 0g ‘ 𝐺 ) )
19 6 11 18 3eqtr4rd ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ 𝐴 = ∅ ) → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) = ( ( ♯ ‘ 𝐴 ) · 𝑋 ) )
20 19 ex ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) → ( 𝐴 = ∅ → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) = ( ( ♯ ‘ 𝐴 ) · 𝑋 ) ) )
21 simprl ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( ♯ ‘ 𝐴 ) ∈ ℕ )
22 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
23 21 22 eleqtrdi ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) )
24 simpr ⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
25 simpl3 ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → 𝑋 ∈ 𝐵 )
26 25 adantr ⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → 𝑋 ∈ 𝐵 )
27 eqid ⊢ ( 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ↦ 𝑋 ) = ( 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ↦ 𝑋 )
28 27 fvmpt2 ⊢ ( ( 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ↦ 𝑋 ) ‘ 𝑥 ) = 𝑋 )
29 24 26 28 syl2anc ⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ↦ 𝑋 ) ‘ 𝑥 ) = 𝑋 )
30 f1of ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
31 30 ad2antll ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
32 31 ffvelrnda ⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝐴 )
33 31 feqmptd ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → 𝑓 = ( 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ↦ ( 𝑓 ‘ 𝑥 ) ) )
34 eqidd ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) = ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) )
35 eqidd ⊢ ( 𝑘 = ( 𝑓 ‘ 𝑥 ) → 𝑋 = 𝑋 )
36 32 33 34 35 fmptco ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ∘ 𝑓 ) = ( 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ↦ 𝑋 ) )
37 36 fveq1d ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ∘ 𝑓 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ↦ 𝑋 ) ‘ 𝑥 ) )
38 37 adantr ⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ∘ 𝑓 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ↦ 𝑋 ) ‘ 𝑥 ) )
39 elfznn ⊢ ( 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → 𝑥 ∈ ℕ )
40 fvconst2g ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑥 ∈ ℕ ) → ( ( ℕ × { 𝑋 } ) ‘ 𝑥 ) = 𝑋 )
41 25 39 40 syl2an ⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ℕ × { 𝑋 } ) ‘ 𝑥 ) = 𝑋 )
42 29 38 41 3eqtr4d ⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ∘ 𝑓 ) ‘ 𝑥 ) = ( ( ℕ × { 𝑋 } ) ‘ 𝑥 ) )
43 23 42 seqfveq ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( seq 1 ( ( +g ‘ 𝐺 ) , ( ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ ( ♯ ‘ 𝐴 ) ) )
44 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
45 eqid ⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
46 simpl1 ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → 𝐺 ∈ Mnd )
47 simpl2 ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → 𝐴 ∈ Fin )
48 25 adantr ⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
49 48 fmpttd ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) : 𝐴 ⟶ 𝐵 )
50 eqidd ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( 𝑋 ( +g ‘ 𝐺 ) 𝑋 ) = ( 𝑋 ( +g ‘ 𝐺 ) 𝑋 ) )
51 1 44 45 elcntzsn ⊢ ( 𝑋 ∈ 𝐵 → ( 𝑋 ∈ ( ( Cntz ‘ 𝐺 ) ‘ { 𝑋 } ) ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝑋 ( +g ‘ 𝐺 ) 𝑋 ) = ( 𝑋 ( +g ‘ 𝐺 ) 𝑋 ) ) ) )
52 25 51 syl ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( 𝑋 ∈ ( ( Cntz ‘ 𝐺 ) ‘ { 𝑋 } ) ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝑋 ( +g ‘ 𝐺 ) 𝑋 ) = ( 𝑋 ( +g ‘ 𝐺 ) 𝑋 ) ) ) )
53 25 50 52 mpbir2and ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → 𝑋 ∈ ( ( Cntz ‘ 𝐺 ) ‘ { 𝑋 } ) )
54 53 snssd ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → { 𝑋 } ⊆ ( ( Cntz ‘ 𝐺 ) ‘ { 𝑋 } ) )
55 snidg ⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ { 𝑋 } )
56 25 55 syl ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → 𝑋 ∈ { 𝑋 } )
57 56 adantr ⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) → 𝑋 ∈ { 𝑋 } )
58 57 fmpttd ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) : 𝐴 ⟶ { 𝑋 } )
59 58 frnd ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ran ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ⊆ { 𝑋 } )
60 45 cntzidss ⊢ ( ( { 𝑋 } ⊆ ( ( Cntz ‘ 𝐺 ) ‘ { 𝑋 } ) ∧ ran ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ⊆ { 𝑋 } ) → ran ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) )
61 54 59 60 syl2anc ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ran ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) )
62 f1of1 ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1→ 𝐴 )
63 62 ad2antll ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1→ 𝐴 )
64 suppssdm ⊢ ( ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) supp ( 0g ‘ 𝐺 ) ) ⊆ dom ( 𝑘 ∈ 𝐴 ↦ 𝑋 )
65 eqid ⊢ ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) = ( 𝑘 ∈ 𝐴 ↦ 𝑋 )
66 65 dmmptss ⊢ dom ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ⊆ 𝐴
67 66 a1i ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → dom ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ⊆ 𝐴 )
68 64 67 sstrid ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) supp ( 0g ‘ 𝐺 ) ) ⊆ 𝐴 )
69 f1ofo ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –onto→ 𝐴 )
70 forn ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –onto→ 𝐴 → ran 𝑓 = 𝐴 )
71 69 70 syl ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → ran 𝑓 = 𝐴 )
72 71 ad2antll ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ran 𝑓 = 𝐴 )
73 68 72 sseqtrrd ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) supp ( 0g ‘ 𝐺 ) ) ⊆ ran 𝑓 )
74 eqid ⊢ ( ( ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ∘ 𝑓 ) supp ( 0g ‘ 𝐺 ) ) = ( ( ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ∘ 𝑓 ) supp ( 0g ‘ 𝐺 ) )
75 1 4 44 45 46 47 49 61 21 63 73 74 gsumval3 ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) )
76 eqid ⊢ seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) = seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) )
77 1 44 2 76 mulgnn ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( ( ♯ ‘ 𝐴 ) · 𝑋 ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ ( ♯ ‘ 𝐴 ) ) )
78 21 25 77 syl2anc ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( ( ♯ ‘ 𝐴 ) · 𝑋 ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ ( ♯ ‘ 𝐴 ) ) )
79 43 75 78 3eqtr4d ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) = ( ( ♯ ‘ 𝐴 ) · 𝑋 ) )
80 79 expr ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) → ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) = ( ( ♯ ‘ 𝐴 ) · 𝑋 ) ) )
81 80 exlimdv ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) → ( ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) = ( ( ♯ ‘ 𝐴 ) · 𝑋 ) ) )
82 81 expimpd ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) → ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) = ( ( ♯ ‘ 𝐴 ) · 𝑋 ) ) )
83 fz1f1o ⊢ ( 𝐴 ∈ Fin → ( 𝐴 = ∅ ∨ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) )
84 83 3ad2ant2 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) → ( 𝐴 = ∅ ∨ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) )
85 20 82 84 mpjaod ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) = ( ( ♯ ‘ 𝐴 ) · 𝑋 ) )