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 coass ⊢ ( ( 𝐻 ∘ ◡ 𝐻 ) ∘ 𝑓 ) = ( 𝐻 ∘ ( ◡ 𝐻 ∘ 𝑓 ) )
36 9 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → 𝐻 : 𝐶 –1-1-onto→ 𝐴 )
37 f1ococnv2 ⊢ ( 𝐻 : 𝐶 –1-1-onto→ 𝐴 → ( 𝐻 ∘ ◡ 𝐻 ) = ( I ↾ 𝐴 ) )
38 36 37 syl ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐻 ∘ ◡ 𝐻 ) = ( I ↾ 𝐴 ) )
39 38 coeq1d ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ( 𝐻 ∘ ◡ 𝐻 ) ∘ 𝑓 ) = ( ( I ↾ 𝐴 ) ∘ 𝑓 ) )
40 f1of1 ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) → 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ ( 𝐹 supp 0 ) )
41 40 ad2antll ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ ( 𝐹 supp 0 ) )
42 suppssdm ⊢ ( 𝐹 supp 0 ) ⊆ dom 𝐹
43 42 6 fssdm ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ 𝐴 )
44 43 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐹 supp 0 ) ⊆ 𝐴 )
45 f1ss ⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ ( 𝐹 supp 0 ) ∧ ( 𝐹 supp 0 ) ⊆ 𝐴 ) → 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ 𝐴 )
46 41 44 45 syl2anc ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ 𝐴 )
47 f1f ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ 𝐴 → 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ⟶ 𝐴 )
48 fcoi2 ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ⟶ 𝐴 → ( ( I ↾ 𝐴 ) ∘ 𝑓 ) = 𝑓 )
49 46 47 48 3syl ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ( I ↾ 𝐴 ) ∘ 𝑓 ) = 𝑓 )
50 39 49 eqtrd ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ( 𝐻 ∘ ◡ 𝐻 ) ∘ 𝑓 ) = 𝑓 )
51 35 50 syl5reqr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 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 syl6eqr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 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 46 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 46 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 fex ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → 𝐹 ∈ V )
87 6 5 86 syl2anc ⊢ ( 𝜑 → 𝐹 ∈ V )
88 suppimacnv ⊢ ( ( 𝐹 ∈ V ∧ 0 ∈ V ) → ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) )
89 87 20 88 sylancl ⊢ ( 𝜑 → ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) )
90 89 eqcomd ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) = ( 𝐹 supp 0 ) )
91 90 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) = ( 𝐹 supp 0 ) )
92 85 91 67 3sstr4d ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ⊆ ran 𝑓 )
93 imass2 ⊢ ( ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ⊆ ran 𝑓 → ( ◡ 𝐻 “ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ⊆ ( ◡ 𝐻 “ ran 𝑓 ) )
94 92 93 syl ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ◡ 𝐻 “ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ⊆ ( ◡ 𝐻 “ ran 𝑓 ) )
95 cnvco ⊢ ◡ ( 𝐹 ∘ 𝐻 ) = ( ◡ 𝐻 ∘ ◡ 𝐹 )
96 95 imaeq1i ⊢ ( ◡ ( 𝐹 ∘ 𝐻 ) “ ( V ∖ { 0 } ) ) = ( ( ◡ 𝐻 ∘ ◡ 𝐹 ) “ ( V ∖ { 0 } ) )
97 imaco ⊢ ( ( ◡ 𝐻 ∘ ◡ 𝐹 ) “ ( V ∖ { 0 } ) ) = ( ◡ 𝐻 “ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) )
98 96 97 eqtri ⊢ ( ◡ ( 𝐹 ∘ 𝐻 ) “ ( V ∖ { 0 } ) ) = ( ◡ 𝐻 “ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) )
99 rnco2 ⊢ ran ( ◡ 𝐻 ∘ 𝑓 ) = ( ◡ 𝐻 “ ran 𝑓 )
100 94 98 99 3sstr4g ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ◡ ( 𝐹 ∘ 𝐻 ) “ ( V ∖ { 0 } ) ) ⊆ ran ( ◡ 𝐻 ∘ 𝑓 ) )
101 f1oexrnex ⊢ ( ( 𝐻 : 𝐶 –1-1-onto→ 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝐻 ∈ V )
102 9 5 101 syl2anc ⊢ ( 𝜑 → 𝐻 ∈ V )
103 coexg ⊢ ( ( 𝐹 ∈ V ∧ 𝐻 ∈ V ) → ( 𝐹 ∘ 𝐻 ) ∈ V )
104 87 102 103 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∘ 𝐻 ) ∈ V )
105 suppimacnv ⊢ ( ( ( 𝐹 ∘ 𝐻 ) ∈ V ∧ 0 ∈ V ) → ( ( 𝐹 ∘ 𝐻 ) supp 0 ) = ( ◡ ( 𝐹 ∘ 𝐻 ) “ ( V ∖ { 0 } ) ) )
106 104 20 105 sylancl ⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐻 ) supp 0 ) = ( ◡ ( 𝐹 ∘ 𝐻 ) “ ( V ∖ { 0 } ) ) )
107 106 sseq1d ⊢ ( 𝜑 → ( ( ( 𝐹 ∘ 𝐻 ) supp 0 ) ⊆ ran ( ◡ 𝐻 ∘ 𝑓 ) ↔ ( ◡ ( 𝐹 ∘ 𝐻 ) “ ( V ∖ { 0 } ) ) ⊆ ran ( ◡ 𝐻 ∘ 𝑓 ) ) )
108 107 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ( ( 𝐹 ∘ 𝐻 ) supp 0 ) ⊆ ran ( ◡ 𝐻 ∘ 𝑓 ) ↔ ( ◡ ( 𝐹 ∘ 𝐻 ) “ ( V ∖ { 0 } ) ) ⊆ ran ( ◡ 𝐻 ∘ 𝑓 ) ) )
109 100 108 mpbird ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ( 𝐹 ∘ 𝐻 ) supp 0 ) ⊆ ran ( ◡ 𝐻 ∘ 𝑓 ) )
110 eqid ⊢ ( ( ( 𝐹 ∘ 𝐻 ) ∘ ( ◡ 𝐻 ∘ 𝑓 ) ) supp 0 ) = ( ( ( 𝐹 ∘ 𝐻 ) ∘ ( ◡ 𝐻 ∘ 𝑓 ) ) supp 0 )
111 1 2 57 3 58 71 74 78 62 84 109 110 gsumval3 ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐺 Σg ( 𝐹 ∘ 𝐻 ) ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( ( 𝐹 ∘ 𝐻 ) ∘ ( ◡ 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) )
112 56 70 111 3eqtr4d ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝐹 ∘ 𝐻 ) ) )
113 112 expr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ) → ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝐹 ∘ 𝐻 ) ) ) )
114 113 exlimdv ⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ) → ( ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝐹 ∘ 𝐻 ) ) ) )
115 114 expimpd ⊢ ( 𝜑 → ( ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝐹 ∘ 𝐻 ) ) ) )
116 fsuppimp ⊢ ( 𝐹 finSupp 0 → ( Fun 𝐹 ∧ ( 𝐹 supp 0 ) ∈ Fin ) )
117 116 simprd ⊢ ( 𝐹 finSupp 0 → ( 𝐹 supp 0 ) ∈ Fin )
118 fz1f1o ⊢ ( ( 𝐹 supp 0 ) ∈ Fin → ( ( 𝐹 supp 0 ) = ∅ ∨ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) )
119 8 117 118 3syl ⊢ ( 𝜑 → ( ( 𝐹 supp 0 ) = ∅ ∨ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) )
120 34 115 119 mpjaod ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝐹 ∘ 𝐻 ) ) )