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	ffvelcdmda	⊢ ( ( ( ( 𝐺 ∈ 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 ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) = ( ( ♯ ‘ 𝐴 ) · 𝑋 ) )