Metamath Proof Explorer

Theorem gsumzres

Description: Extend a finite group sum by padding outside with zeroes. (Contributed by Mario Carneiro, 24-Apr-2016) (Revised by AV, 31-May-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 𝐹 ) )
gsumzres.s ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ 𝑊 )
gsumzres.w ⊢ ( 𝜑 → 𝐹 finSupp 0 )
Assertion gsumzres ( 𝜑 → ( 𝐺 Σ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 gsumzres.s ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ 𝑊 )
9 gsumzres.w ⊢ ( 𝜑 → 𝐹 finSupp 0 )
10 inex1g ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∩ 𝑊 ) ∈ V )
11 5 10 syl ⊢ ( 𝜑 → ( 𝐴 ∩ 𝑊 ) ∈ V )
12 2 gsumz ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝐴 ∩ 𝑊 ) ∈ V ) → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 ∩ 𝑊 ) ↦ 0 ) ) = 0 )
13 4 11 12 syl2anc ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 ∩ 𝑊 ) ↦ 0 ) ) = 0 )
14 2 gsumz ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉 ) → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 0 ) ) = 0 )
15 4 5 14 syl2anc ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 0 ) ) = 0 )
16 13 15 eqtr4d ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 ∩ 𝑊 ) ↦ 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 0 ) ) )
17 16 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 supp 0 ) = ∅ ) → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 ∩ 𝑊 ) ↦ 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 0 ) ) )
18 resres ⊢ ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑊 ) = ( 𝐹 ↾ ( 𝐴 ∩ 𝑊 ) )
19 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
20 fnresdm ⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ 𝐴 ) = 𝐹 )
21 6 19 20 3syl ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) = 𝐹 )
22 21 reseq1d ⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑊 ) = ( 𝐹 ↾ 𝑊 ) )
23 18 22 eqtr3id ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 ∩ 𝑊 ) ) = ( 𝐹 ↾ 𝑊 ) )
24 23 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 supp 0 ) = ∅ ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝑊 ) ) = ( 𝐹 ↾ 𝑊 ) )
25 2 fvexi ⊢ 0 ∈ V
26 25 a1i ⊢ ( 𝜑 → 0 ∈ V )
27 ssid ⊢ ( 𝐹 supp 0 ) ⊆ ( 𝐹 supp 0 )
28 27 a1i ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ ( 𝐹 supp 0 ) )
29 6 5 26 28 gsumcllem ⊢ ( ( 𝜑 ∧ ( 𝐹 supp 0 ) = ∅ ) → 𝐹 = ( 𝑘 ∈ 𝐴 ↦ 0 ) )
30 29 reseq1d ⊢ ( ( 𝜑 ∧ ( 𝐹 supp 0 ) = ∅ ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝑊 ) ) = ( ( 𝑘 ∈ 𝐴 ↦ 0 ) ↾ ( 𝐴 ∩ 𝑊 ) ) )
31 inss1 ⊢ ( 𝐴 ∩ 𝑊 ) ⊆ 𝐴
32 resmpt ⊢ ( ( 𝐴 ∩ 𝑊 ) ⊆ 𝐴 → ( ( 𝑘 ∈ 𝐴 ↦ 0 ) ↾ ( 𝐴 ∩ 𝑊 ) ) = ( 𝑘 ∈ ( 𝐴 ∩ 𝑊 ) ↦ 0 ) )
33 31 32 ax-mp ⊢ ( ( 𝑘 ∈ 𝐴 ↦ 0 ) ↾ ( 𝐴 ∩ 𝑊 ) ) = ( 𝑘 ∈ ( 𝐴 ∩ 𝑊 ) ↦ 0 )
34 30 33 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝐹 supp 0 ) = ∅ ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝑊 ) ) = ( 𝑘 ∈ ( 𝐴 ∩ 𝑊 ) ↦ 0 ) )
35 24 34 eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝐹 supp 0 ) = ∅ ) → ( 𝐹 ↾ 𝑊 ) = ( 𝑘 ∈ ( 𝐴 ∩ 𝑊 ) ↦ 0 ) )
36 35 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝐹 supp 0 ) = ∅ ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑊 ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 ∩ 𝑊 ) ↦ 0 ) ) )
37 29 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝐹 supp 0 ) = ∅ ) → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 0 ) ) )
38 17 36 37 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝐹 supp 0 ) = ∅ ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑊 ) ) = ( 𝐺 Σg 𝐹 ) )
39 38 ex ⊢ ( 𝜑 → ( ( 𝐹 supp 0 ) = ∅ → ( 𝐺 Σg ( 𝐹 ↾ 𝑊 ) ) = ( 𝐺 Σg 𝐹 ) ) )
40 f1ofo ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) → 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –onto→ ( 𝐹 supp 0 ) )
41 forn ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –onto→ ( 𝐹 supp 0 ) → ran 𝑓 = ( 𝐹 supp 0 ) )
42 40 41 syl ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) → ran 𝑓 = ( 𝐹 supp 0 ) )
43 42 ad2antll ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ran 𝑓 = ( 𝐹 supp 0 ) )
44 8 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐹 supp 0 ) ⊆ 𝑊 )
45 43 44 eqsstrd ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ran 𝑓 ⊆ 𝑊 )
46 cores ⊢ ( ran 𝑓 ⊆ 𝑊 → ( ( 𝐹 ↾ 𝑊 ) ∘ 𝑓 ) = ( 𝐹 ∘ 𝑓 ) )
47 45 46 syl ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ( 𝐹 ↾ 𝑊 ) ∘ 𝑓 ) = ( 𝐹 ∘ 𝑓 ) )
48 47 seqeq3d ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → seq 1 ( ( +g ‘ 𝐺 ) , ( ( 𝐹 ↾ 𝑊 ) ∘ 𝑓 ) ) = seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) )
49 48 fveq1d ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( seq 1 ( ( +g ‘ 𝐺 ) , ( ( 𝐹 ↾ 𝑊 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) )
50 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
51 4 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → 𝐺 ∈ Mnd )
52 11 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐴 ∩ 𝑊 ) ∈ V )
53 6 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
54 fssres ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝐴 ∩ 𝑊 ) ⊆ 𝐴 ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝑊 ) ) : ( 𝐴 ∩ 𝑊 ) ⟶ 𝐵 )
55 53 31 54 sylancl ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝑊 ) ) : ( 𝐴 ∩ 𝑊 ) ⟶ 𝐵 )
56 23 feq1d ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐴 ∩ 𝑊 ) ) : ( 𝐴 ∩ 𝑊 ) ⟶ 𝐵 ↔ ( 𝐹 ↾ 𝑊 ) : ( 𝐴 ∩ 𝑊 ) ⟶ 𝐵 ) )
57 56 biimpa ⊢ ( ( 𝜑 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝑊 ) ) : ( 𝐴 ∩ 𝑊 ) ⟶ 𝐵 ) → ( 𝐹 ↾ 𝑊 ) : ( 𝐴 ∩ 𝑊 ) ⟶ 𝐵 )
58 55 57 syldan ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐹 ↾ 𝑊 ) : ( 𝐴 ∩ 𝑊 ) ⟶ 𝐵 )
59 resss ⊢ ( 𝐹 ↾ 𝑊 ) ⊆ 𝐹
60 59 rnssi ⊢ ran ( 𝐹 ↾ 𝑊 ) ⊆ ran 𝐹
61 3 cntzidss ⊢ ( ( ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) ∧ ran ( 𝐹 ↾ 𝑊 ) ⊆ ran 𝐹 ) → ran ( 𝐹 ↾ 𝑊 ) ⊆ ( 𝑍 ‘ ran ( 𝐹 ↾ 𝑊 ) ) )
62 7 60 61 sylancl ⊢ ( 𝜑 → ran ( 𝐹 ↾ 𝑊 ) ⊆ ( 𝑍 ‘ ran ( 𝐹 ↾ 𝑊 ) ) )
63 62 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ran ( 𝐹 ↾ 𝑊 ) ⊆ ( 𝑍 ‘ ran ( 𝐹 ↾ 𝑊 ) ) )
64 simprl ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ )
65 f1of1 ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) → 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ ( 𝐹 supp 0 ) )
66 65 ad2antll ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ ( 𝐹 supp 0 ) )
67 suppssdm ⊢ ( 𝐹 supp 0 ) ⊆ dom 𝐹
68 67 6 fssdm ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ 𝐴 )
69 68 8 ssind ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ ( 𝐴 ∩ 𝑊 ) )
70 69 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐹 supp 0 ) ⊆ ( 𝐴 ∩ 𝑊 ) )
71 f1ss ⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ ( 𝐹 supp 0 ) ∧ ( 𝐹 supp 0 ) ⊆ ( 𝐴 ∩ 𝑊 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ ( 𝐴 ∩ 𝑊 ) )
72 66 70 71 syl2anc ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ ( 𝐴 ∩ 𝑊 ) )
73 6 5 fexd ⊢ ( 𝜑 → 𝐹 ∈ V )
74 ressuppss ⊢ ( ( 𝐹 ∈ V ∧ 0 ∈ V ) → ( ( 𝐹 ↾ 𝑊 ) supp 0 ) ⊆ ( 𝐹 supp 0 ) )
75 73 25 74 sylancl ⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝑊 ) supp 0 ) ⊆ ( 𝐹 supp 0 ) )
76 sseq2 ⊢ ( ran 𝑓 = ( 𝐹 supp 0 ) → ( ( ( 𝐹 ↾ 𝑊 ) supp 0 ) ⊆ ran 𝑓 ↔ ( ( 𝐹 ↾ 𝑊 ) supp 0 ) ⊆ ( 𝐹 supp 0 ) ) )
77 75 76 imbitrrid ⊢ ( ran 𝑓 = ( 𝐹 supp 0 ) → ( 𝜑 → ( ( 𝐹 ↾ 𝑊 ) supp 0 ) ⊆ ran 𝑓 ) )
78 40 41 77 3syl ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) → ( 𝜑 → ( ( 𝐹 ↾ 𝑊 ) supp 0 ) ⊆ ran 𝑓 ) )
79 78 adantl ⊢ ( ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) → ( 𝜑 → ( ( 𝐹 ↾ 𝑊 ) supp 0 ) ⊆ ran 𝑓 ) )
80 79 impcom ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ( 𝐹 ↾ 𝑊 ) supp 0 ) ⊆ ran 𝑓 )
81 eqid ⊢ ( ( ( 𝐹 ↾ 𝑊 ) ∘ 𝑓 ) supp 0 ) = ( ( ( 𝐹 ↾ 𝑊 ) ∘ 𝑓 ) supp 0 )
82 1 2 50 3 51 52 58 63 64 72 80 81 gsumval3 ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑊 ) ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( ( 𝐹 ↾ 𝑊 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) )
83 5 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → 𝐴 ∈ 𝑉 )
84 7 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
85 68 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐹 supp 0 ) ⊆ 𝐴 )
86 f1ss ⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ ( 𝐹 supp 0 ) ∧ ( 𝐹 supp 0 ) ⊆ 𝐴 ) → 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ 𝐴 )
87 66 85 86 syl2anc ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ 𝐴 )
88 27 43 sseqtrrid ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐹 supp 0 ) ⊆ ran 𝑓 )
89 eqid ⊢ ( ( 𝐹 ∘ 𝑓 ) supp 0 ) = ( ( 𝐹 ∘ 𝑓 ) supp 0 )
90 1 2 50 3 51 83 53 84 64 87 88 89 gsumval3 ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) )
91 49 82 90 3eqtr4d ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑊 ) ) = ( 𝐺 Σg 𝐹 ) )
92 91 expr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ) → ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑊 ) ) = ( 𝐺 Σg 𝐹 ) ) )
93 92 exlimdv ⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ) → ( ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑊 ) ) = ( 𝐺 Σg 𝐹 ) ) )
94 93 expimpd ⊢ ( 𝜑 → ( ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑊 ) ) = ( 𝐺 Σg 𝐹 ) ) )
95 fsuppimp ⊢ ( 𝐹 finSupp 0 → ( Fun 𝐹 ∧ ( 𝐹 supp 0 ) ∈ Fin ) )
96 95 simprd ⊢ ( 𝐹 finSupp 0 → ( 𝐹 supp 0 ) ∈ Fin )
97 fz1f1o ⊢ ( ( 𝐹 supp 0 ) ∈ Fin → ( ( 𝐹 supp 0 ) = ∅ ∨ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) )
98 9 96 97 3syl ⊢ ( 𝜑 → ( ( 𝐹 supp 0 ) = ∅ ∨ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) )
99 39 94 98 mpjaod ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ 𝑊 ) ) = ( 𝐺 Σg 𝐹 ) )