Metamath Proof Explorer


Theorem 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 = ( 0g𝐺 )
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 = ( 0g𝐺 )
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 ffvelrnda ( ( ( 𝜑 ∧ ( 𝐹 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 ( 𝐹𝐻 ) ) )