gsumzf1o

Description: Re-index a finite group sum using a bijection. (Contributed by Mario Carneiro, 24-Apr-2016) (Revised by AV, 2-Jun-2019)

	Ref	Expression
Hypotheses	gsumzcl.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	gsumzcl.0	⊢ 0 = ( 0_g ‘ 𝐺 )
	gsumzcl.z	⊢ 𝑍 = ( Cntz ‘ 𝐺 )
	gsumzcl.g	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
	gsumzcl.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	gsumzcl.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	gsumzcl.c	⊢ ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
	gsumzcl.w	⊢ ( 𝜑 → 𝐹 finSupp 0 )
	gsumzf1o.h	⊢ ( 𝜑 → 𝐻 : 𝐶 –1-1-onto→ 𝐴 )
Assertion	gsumzf1o	⊢ ( 𝜑 → ( 𝐺 Σ_g 𝐹 ) = ( 𝐺 Σ_g ( 𝐹 ∘ 𝐻 ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsumzcl.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		gsumzcl.0	⊢ 0 = ( 0_g ‘ 𝐺 )
3		gsumzcl.z	⊢ 𝑍 = ( Cntz ‘ 𝐺 )
4		gsumzcl.g	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
5		gsumzcl.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6		gsumzcl.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
7		gsumzcl.c	⊢ ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
8		gsumzcl.w	⊢ ( 𝜑 → 𝐹 finSupp 0 )
9		gsumzf1o.h	⊢ ( 𝜑 → 𝐻 : 𝐶 –1-1-onto→ 𝐴 )
10	2	gsumz	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉 ) → ( 𝐺 Σ_g ( 𝑘 ∈ 𝐴 ↦ 0 ) ) = 0 )
11	4 5 10	syl2anc	⊢ ( 𝜑 → ( 𝐺 Σ_g ( 𝑘 ∈ 𝐴 ↦ 0 ) ) = 0 )
12		f1of1	⊢ ( 𝐻 : 𝐶 –1-1-onto→ 𝐴 → 𝐻 : 𝐶 –1-1→ 𝐴 )
13	9 12	syl	⊢ ( 𝜑 → 𝐻 : 𝐶 –1-1→ 𝐴 )
14		f1dmex	⊢ ( ( 𝐻 : 𝐶 –1-1→ 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝐶 ∈ V )
15	13 5 14	syl2anc	⊢ ( 𝜑 → 𝐶 ∈ V )
16	2	gsumz	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐶 ∈ V ) → ( 𝐺 Σ_g ( 𝑥 ∈ 𝐶 ↦ 0 ) ) = 0 )
17	4 15 16	syl2anc	⊢ ( 𝜑 → ( 𝐺 Σ_g ( 𝑥 ∈ 𝐶 ↦ 0 ) ) = 0 )
18	11 17	eqtr4d	⊢ ( 𝜑 → ( 𝐺 Σ_g ( 𝑘 ∈ 𝐴 ↦ 0 ) ) = ( 𝐺 Σ_g ( 𝑥 ∈ 𝐶 ↦ 0 ) ) )
19	18	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 supp 0 ) = ∅ ) → ( 𝐺 Σ_g ( 𝑘 ∈ 𝐴 ↦ 0 ) ) = ( 𝐺 Σ_g ( 𝑥 ∈ 𝐶 ↦ 0 ) ) )
20	2	fvexi	⊢ 0 ∈ V
21	20	a1i	⊢ ( 𝜑 → 0 ∈ V )
22		ssidd	⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ ( 𝐹 supp 0 ) )
23	6 5 21 22	gsumcllem	⊢ ( ( 𝜑 ∧ ( 𝐹 supp 0 ) = ∅ ) → 𝐹 = ( 𝑘 ∈ 𝐴 ↦ 0 ) )
24	23	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝐹 supp 0 ) = ∅ ) → ( 𝐺 Σ_g 𝐹 ) = ( 𝐺 Σ_g ( 𝑘 ∈ 𝐴 ↦ 0 ) ) )
25		f1of	⊢ ( 𝐻 : 𝐶 –1-1-onto→ 𝐴 → 𝐻 : 𝐶 ⟶ 𝐴 )
26	9 25	syl	⊢ ( 𝜑 → 𝐻 : 𝐶 ⟶ 𝐴 )
27	26	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 supp 0 ) = ∅ ) → 𝐻 : 𝐶 ⟶ 𝐴 )
28	27	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ ( 𝐹 supp 0 ) = ∅ ) ∧ 𝑥 ∈ 𝐶 ) → ( 𝐻 ‘ 𝑥 ) ∈ 𝐴 )
29	27	feqmptd	⊢ ( ( 𝜑 ∧ ( 𝐹 supp 0 ) = ∅ ) → 𝐻 = ( 𝑥 ∈ 𝐶 ↦ ( 𝐻 ‘ 𝑥 ) ) )
30		eqidd	⊢ ( 𝑘 = ( 𝐻 ‘ 𝑥 ) → 0 = 0 )
31	28 29 23 30	fmptco	⊢ ( ( 𝜑 ∧ ( 𝐹 supp 0 ) = ∅ ) → ( 𝐹 ∘ 𝐻 ) = ( 𝑥 ∈ 𝐶 ↦ 0 ) )
32	31	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝐹 supp 0 ) = ∅ ) → ( 𝐺 Σ_g ( 𝐹 ∘ 𝐻 ) ) = ( 𝐺 Σ_g ( 𝑥 ∈ 𝐶 ↦ 0 ) ) )
33	19 24 32	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝐹 supp 0 ) = ∅ ) → ( 𝐺 Σ_g 𝐹 ) = ( 𝐺 Σ_g ( 𝐹 ∘ 𝐻 ) ) )
34	33	ex	⊢ ( 𝜑 → ( ( 𝐹 supp 0 ) = ∅ → ( 𝐺 Σ_g 𝐹 ) = ( 𝐺 Σ_g ( 𝐹 ∘ 𝐻 ) ) ) )
35	9	adantr	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → 𝐻 : 𝐶 –1-1-onto→ 𝐴 )
36		f1ococnv2	⊢ ( 𝐻 : 𝐶 –1-1-onto→ 𝐴 → ( 𝐻 ∘ ^◡ 𝐻 ) = ( I ↾ 𝐴 ) )
37	35 36	syl	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐻 ∘ ^◡ 𝐻 ) = ( I ↾ 𝐴 ) )
38	37	coeq1d	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ( 𝐻 ∘ ^◡ 𝐻 ) ∘ 𝑓 ) = ( ( I ↾ 𝐴 ) ∘ 𝑓 ) )
39		f1of1	⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) → 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ ( 𝐹 supp 0 ) )
40	39	ad2antll	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ ( 𝐹 supp 0 ) )
41		suppssdm	⊢ ( 𝐹 supp 0 ) ⊆ dom 𝐹
42	41 6	fssdm	⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ 𝐴 )
43	42	adantr	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐹 supp 0 ) ⊆ 𝐴 )
44		f1ss	⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ ( 𝐹 supp 0 ) ∧ ( 𝐹 supp 0 ) ⊆ 𝐴 ) → 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ 𝐴 )
45	40 43 44	syl2anc	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ 𝐴 )
46		f1f	⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ 𝐴 → 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ⟶ 𝐴 )
47		fcoi2	⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ⟶ 𝐴 → ( ( I ↾ 𝐴 ) ∘ 𝑓 ) = 𝑓 )
48	45 46 47	3syl	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ( I ↾ 𝐴 ) ∘ 𝑓 ) = 𝑓 )
49	38 48	eqtrd	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ( 𝐻 ∘ ^◡ 𝐻 ) ∘ 𝑓 ) = 𝑓 )
50		coass	⊢ ( ( 𝐻 ∘ ^◡ 𝐻 ) ∘ 𝑓 ) = ( 𝐻 ∘ ( ^◡ 𝐻 ∘ 𝑓 ) )
51	49 50	eqtr3di	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → 𝑓 = ( 𝐻 ∘ ( ^◡ 𝐻 ∘ 𝑓 ) ) )
52	51	coeq2d	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐹 ∘ 𝑓 ) = ( 𝐹 ∘ ( 𝐻 ∘ ( ^◡ 𝐻 ∘ 𝑓 ) ) ) )
53		coass	⊢ ( ( 𝐹 ∘ 𝐻 ) ∘ ( ^◡ 𝐻 ∘ 𝑓 ) ) = ( 𝐹 ∘ ( 𝐻 ∘ ( ^◡ 𝐻 ∘ 𝑓 ) ) )
54	52 53	eqtr4di	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐹 ∘ 𝑓 ) = ( ( 𝐹 ∘ 𝐻 ) ∘ ( ^◡ 𝐻 ∘ 𝑓 ) ) )
55	54	seqeq3d	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → seq 1 ( ( +_g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) = seq 1 ( ( +_g ‘ 𝐺 ) , ( ( 𝐹 ∘ 𝐻 ) ∘ ( ^◡ 𝐻 ∘ 𝑓 ) ) ) )
56	55	fveq1d	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( seq 1 ( ( +_g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) = ( seq 1 ( ( +_g ‘ 𝐺 ) , ( ( 𝐹 ∘ 𝐻 ) ∘ ( ^◡ 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) )
57		eqid	⊢ ( +_g ‘ 𝐺 ) = ( +_g ‘ 𝐺 )
58	4	adantr	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → 𝐺 ∈ Mnd )
59	5	adantr	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → 𝐴 ∈ 𝑉 )
60	6	adantr	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
61	7	adantr	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
62		simprl	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ )
63		ssid	⊢ ( 𝐹 supp 0 ) ⊆ ( 𝐹 supp 0 )
64		f1ofo	⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) → 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –onto→ ( 𝐹 supp 0 ) )
65		forn	⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –onto→ ( 𝐹 supp 0 ) → ran 𝑓 = ( 𝐹 supp 0 ) )
66	64 65	syl	⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) → ran 𝑓 = ( 𝐹 supp 0 ) )
67	66	ad2antll	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ran 𝑓 = ( 𝐹 supp 0 ) )
68	63 67	sseqtrrid	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐹 supp 0 ) ⊆ ran 𝑓 )
69		eqid	⊢ ( ( 𝐹 ∘ 𝑓 ) supp 0 ) = ( ( 𝐹 ∘ 𝑓 ) supp 0 )
70	1 2 57 3 58 59 60 61 62 45 68 69	gsumval3	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐺 Σ_g 𝐹 ) = ( seq 1 ( ( +_g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) )
71	15	adantr	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → 𝐶 ∈ V )
72		fco	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐻 : 𝐶 ⟶ 𝐴 ) → ( 𝐹 ∘ 𝐻 ) : 𝐶 ⟶ 𝐵 )
73	6 26 72	syl2anc	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐻 ) : 𝐶 ⟶ 𝐵 )
74	73	adantr	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐹 ∘ 𝐻 ) : 𝐶 ⟶ 𝐵 )
75		rncoss	⊢ ran ( 𝐹 ∘ 𝐻 ) ⊆ ran 𝐹
76	3	cntzidss	⊢ ( ( ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) ∧ ran ( 𝐹 ∘ 𝐻 ) ⊆ ran 𝐹 ) → ran ( 𝐹 ∘ 𝐻 ) ⊆ ( 𝑍 ‘ ran ( 𝐹 ∘ 𝐻 ) ) )
77	7 75 76	sylancl	⊢ ( 𝜑 → ran ( 𝐹 ∘ 𝐻 ) ⊆ ( 𝑍 ‘ ran ( 𝐹 ∘ 𝐻 ) ) )
78	77	adantr	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ran ( 𝐹 ∘ 𝐻 ) ⊆ ( 𝑍 ‘ ran ( 𝐹 ∘ 𝐻 ) ) )
79		f1ocnv	⊢ ( 𝐻 : 𝐶 –1-1-onto→ 𝐴 → ^◡ 𝐻 : 𝐴 –1-1-onto→ 𝐶 )
80		f1of1	⊢ ( ^◡ 𝐻 : 𝐴 –1-1-onto→ 𝐶 → ^◡ 𝐻 : 𝐴 –1-1→ 𝐶 )
81	9 79 80	3syl	⊢ ( 𝜑 → ^◡ 𝐻 : 𝐴 –1-1→ 𝐶 )
82	81	adantr	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ^◡ 𝐻 : 𝐴 –1-1→ 𝐶 )
83		f1co	⊢ ( ( ^◡ 𝐻 : 𝐴 –1-1→ 𝐶 ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ 𝐴 ) → ( ^◡ 𝐻 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ 𝐶 )
84	82 45 83	syl2anc	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ^◡ 𝐻 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ 𝐶 )
85		ssidd	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐹 supp 0 ) ⊆ ( 𝐹 supp 0 ) )
86	6 5	fexd	⊢ ( 𝜑 → 𝐹 ∈ V )
87		suppimacnv	⊢ ( ( 𝐹 ∈ V ∧ 0 ∈ V ) → ( 𝐹 supp 0 ) = ( ^◡ 𝐹 “ ( V ∖ { 0 } ) ) )
88	86 20 87	sylancl	⊢ ( 𝜑 → ( 𝐹 supp 0 ) = ( ^◡ 𝐹 “ ( V ∖ { 0 } ) ) )
89	88	eqcomd	⊢ ( 𝜑 → ( ^◡ 𝐹 “ ( V ∖ { 0 } ) ) = ( 𝐹 supp 0 ) )
90	89	adantr	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ^◡ 𝐹 “ ( V ∖ { 0 } ) ) = ( 𝐹 supp 0 ) )
91	85 90 67	3sstr4d	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ^◡ 𝐹 “ ( V ∖ { 0 } ) ) ⊆ ran 𝑓 )
92		imass2	⊢ ( ( ^◡ 𝐹 “ ( V ∖ { 0 } ) ) ⊆ ran 𝑓 → ( ^◡ 𝐻 “ ( ^◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ⊆ ( ^◡ 𝐻 “ ran 𝑓 ) )
93	91 92	syl	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ^◡ 𝐻 “ ( ^◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ⊆ ( ^◡ 𝐻 “ ran 𝑓 ) )
94		cnvco	⊢ ^◡ ( 𝐹 ∘ 𝐻 ) = ( ^◡ 𝐻 ∘ ^◡ 𝐹 )
95	94	imaeq1i	⊢ ( ^◡ ( 𝐹 ∘ 𝐻 ) “ ( V ∖ { 0 } ) ) = ( ( ^◡ 𝐻 ∘ ^◡ 𝐹 ) “ ( V ∖ { 0 } ) )
96		imaco	⊢ ( ( ^◡ 𝐻 ∘ ^◡ 𝐹 ) “ ( V ∖ { 0 } ) ) = ( ^◡ 𝐻 “ ( ^◡ 𝐹 “ ( V ∖ { 0 } ) ) )
97	95 96	eqtri	⊢ ( ^◡ ( 𝐹 ∘ 𝐻 ) “ ( V ∖ { 0 } ) ) = ( ^◡ 𝐻 “ ( ^◡ 𝐹 “ ( V ∖ { 0 } ) ) )
98		rnco2	⊢ ran ( ^◡ 𝐻 ∘ 𝑓 ) = ( ^◡ 𝐻 “ ran 𝑓 )
99	93 97 98	3sstr4g	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ^◡ ( 𝐹 ∘ 𝐻 ) “ ( V ∖ { 0 } ) ) ⊆ ran ( ^◡ 𝐻 ∘ 𝑓 ) )
100		f1oexrnex	⊢ ( ( 𝐻 : 𝐶 –1-1-onto→ 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝐻 ∈ V )
101	9 5 100	syl2anc	⊢ ( 𝜑 → 𝐻 ∈ V )
102		coexg	⊢ ( ( 𝐹 ∈ V ∧ 𝐻 ∈ V ) → ( 𝐹 ∘ 𝐻 ) ∈ V )
103	86 101 102	syl2anc	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐻 ) ∈ V )
104		suppimacnv	⊢ ( ( ( 𝐹 ∘ 𝐻 ) ∈ V ∧ 0 ∈ V ) → ( ( 𝐹 ∘ 𝐻 ) supp 0 ) = ( ^◡ ( 𝐹 ∘ 𝐻 ) “ ( V ∖ { 0 } ) ) )
105	103 20 104	sylancl	⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐻 ) supp 0 ) = ( ^◡ ( 𝐹 ∘ 𝐻 ) “ ( V ∖ { 0 } ) ) )
106	105	sseq1d	⊢ ( 𝜑 → ( ( ( 𝐹 ∘ 𝐻 ) supp 0 ) ⊆ ran ( ^◡ 𝐻 ∘ 𝑓 ) ↔ ( ^◡ ( 𝐹 ∘ 𝐻 ) “ ( V ∖ { 0 } ) ) ⊆ ran ( ^◡ 𝐻 ∘ 𝑓 ) ) )
107	106	adantr	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ( ( 𝐹 ∘ 𝐻 ) supp 0 ) ⊆ ran ( ^◡ 𝐻 ∘ 𝑓 ) ↔ ( ^◡ ( 𝐹 ∘ 𝐻 ) “ ( V ∖ { 0 } ) ) ⊆ ran ( ^◡ 𝐻 ∘ 𝑓 ) ) )
108	99 107	mpbird	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ( 𝐹 ∘ 𝐻 ) supp 0 ) ⊆ ran ( ^◡ 𝐻 ∘ 𝑓 ) )
109		eqid	⊢ ( ( ( 𝐹 ∘ 𝐻 ) ∘ ( ^◡ 𝐻 ∘ 𝑓 ) ) supp 0 ) = ( ( ( 𝐹 ∘ 𝐻 ) ∘ ( ^◡ 𝐻 ∘ 𝑓 ) ) supp 0 )
110	1 2 57 3 58 71 74 78 62 84 108 109	gsumval3	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐺 Σ_g ( 𝐹 ∘ 𝐻 ) ) = ( seq 1 ( ( +_g ‘ 𝐺 ) , ( ( 𝐹 ∘ 𝐻 ) ∘ ( ^◡ 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) )
111	56 70 110	3eqtr4d	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐺 Σ_g 𝐹 ) = ( 𝐺 Σ_g ( 𝐹 ∘ 𝐻 ) ) )
112	111	expr	⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ) → ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) → ( 𝐺 Σ_g 𝐹 ) = ( 𝐺 Σ_g ( 𝐹 ∘ 𝐻 ) ) ) )
113	112	exlimdv	⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ) → ( ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) → ( 𝐺 Σ_g 𝐹 ) = ( 𝐺 Σ_g ( 𝐹 ∘ 𝐻 ) ) ) )
114	113	expimpd	⊢ ( 𝜑 → ( ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) → ( 𝐺 Σ_g 𝐹 ) = ( 𝐺 Σ_g ( 𝐹 ∘ 𝐻 ) ) ) )
115		fsuppimp	⊢ ( 𝐹 finSupp 0 → ( Fun 𝐹 ∧ ( 𝐹 supp 0 ) ∈ Fin ) )
116	115	simprd	⊢ ( 𝐹 finSupp 0 → ( 𝐹 supp 0 ) ∈ Fin )
117		fz1f1o	⊢ ( ( 𝐹 supp 0 ) ∈ Fin → ( ( 𝐹 supp 0 ) = ∅ ∨ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) )
118	8 116 117	3syl	⊢ ( 𝜑 → ( ( 𝐹 supp 0 ) = ∅ ∨ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) )
119	34 114 118	mpjaod	⊢ ( 𝜑 → ( 𝐺 Σ_g 𝐹 ) = ( 𝐺 Σ_g ( 𝐹 ∘ 𝐻 ) ) )

Metamath Proof Explorer

Theorem gsumzf1o

Proof