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 ( 𝑘𝐴𝑋 ) ) = ( ( ♯ ‘ 𝐴 ) · 𝑋 ) )