Metamath Proof Explorer

Theorem gsumzcl2

Description: Closure of a finite group sum. This theorem has a weaker hypothesis than gsumzcl , because it is not required that F is a function (actually, the hypothesis always holds for any proper class F ). (Contributed by Mario Carneiro, 24-Apr-2016) (Revised by AV, 1-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 𝐹 ) )
gsumzcl2.w ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ∈ Fin )
Assertion gsumzcl2 ( 𝜑 → ( 𝐺 Σ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 gsumzcl2.w ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ∈ Fin )
9 2 fvexi ⊢ 0 ∈ V
10 9 a1i ⊢ ( 𝜑 → 0 ∈ V )
11 ssidd ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ ( 𝐹 supp 0 ) )
12 6 5 10 11 gsumcllem ⊢ ( ( 𝜑 ∧ ( 𝐹 supp 0 ) = ∅ ) → 𝐹 = ( 𝑘 ∈ 𝐴 ↦ 0 ) )
13 12 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝐹 supp 0 ) = ∅ ) → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 0 ) ) )
14 2 gsumz ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉 ) → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 0 ) ) = 0 )
15 4 5 14 syl2anc ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 0 ) ) = 0 )
16 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 supp 0 ) = ∅ ) → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 0 ) ) = 0 )
17 13 16 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐹 supp 0 ) = ∅ ) → ( 𝐺 Σg 𝐹 ) = 0 )
18 1 2 mndidcl ⊢ ( 𝐺 ∈ Mnd → 0 ∈ 𝐵 )
19 4 18 syl ⊢ ( 𝜑 → 0 ∈ 𝐵 )
20 19 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 supp 0 ) = ∅ ) → 0 ∈ 𝐵 )
21 17 20 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝐹 supp 0 ) = ∅ ) → ( 𝐺 Σg 𝐹 ) ∈ 𝐵 )
22 21 ex ⊢ ( 𝜑 → ( ( 𝐹 supp 0 ) = ∅ → ( 𝐺 Σg 𝐹 ) ∈ 𝐵 ) )
23 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
24 4 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → 𝐺 ∈ Mnd )
25 5 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → 𝐴 ∈ 𝑉 )
26 6 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
27 7 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
28 simprl ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ )
29 f1of1 ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) → 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ ( 𝐹 supp 0 ) )
30 29 ad2antll ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ ( 𝐹 supp 0 ) )
31 suppssdm ⊢ ( 𝐹 supp 0 ) ⊆ dom 𝐹
32 31 6 fssdm ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ 𝐴 )
33 32 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐹 supp 0 ) ⊆ 𝐴 )
34 f1ss ⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ ( 𝐹 supp 0 ) ∧ ( 𝐹 supp 0 ) ⊆ 𝐴 ) → 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ 𝐴 )
35 30 33 34 syl2anc ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ 𝐴 )
36 ssid ⊢ ( 𝐹 supp 0 ) ⊆ ( 𝐹 supp 0 )
37 f1ofo ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) → 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –onto→ ( 𝐹 supp 0 ) )
38 forn ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –onto→ ( 𝐹 supp 0 ) → ran 𝑓 = ( 𝐹 supp 0 ) )
39 37 38 syl ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) → ran 𝑓 = ( 𝐹 supp 0 ) )
40 39 ad2antll ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ran 𝑓 = ( 𝐹 supp 0 ) )
41 36 40 sseqtrrid ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐹 supp 0 ) ⊆ ran 𝑓 )
42 eqid ⊢ ( ( 𝐹 ∘ 𝑓 ) supp 0 ) = ( ( 𝐹 ∘ 𝑓 ) supp 0 )
43 1 2 23 3 24 25 26 27 28 35 41 42 gsumval3 ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) )
44 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
45 28 44 eleqtrdi ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ( ℤ≥ ‘ 1 ) )
46 f1f ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ 𝐴 → 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ⟶ 𝐴 )
47 35 46 syl ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ⟶ 𝐴 )
48 fco ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ⟶ 𝐴 ) → ( 𝐹 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ⟶ 𝐵 )
49 26 47 48 syl2anc ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐹 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ⟶ 𝐵 )
50 49 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ) → ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑘 ) ∈ 𝐵 )
51 1 23 mndcl ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑘 ( +g ‘ 𝐺 ) 𝑥 ) ∈ 𝐵 )
52 51 3expb ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) → ( 𝑘 ( +g ‘ 𝐺 ) 𝑥 ) ∈ 𝐵 )
53 24 52 sylan ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) ∧ ( 𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) → ( 𝑘 ( +g ‘ 𝐺 ) 𝑥 ) ∈ 𝐵 )
54 45 50 53 seqcl ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ∈ 𝐵 )
55 43 54 eqeltrd ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐺 Σg 𝐹 ) ∈ 𝐵 )
56 55 expr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ) → ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) → ( 𝐺 Σg 𝐹 ) ∈ 𝐵 ) )
57 56 exlimdv ⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ) → ( ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) → ( 𝐺 Σg 𝐹 ) ∈ 𝐵 ) )
58 57 expimpd ⊢ ( 𝜑 → ( ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) → ( 𝐺 Σg 𝐹 ) ∈ 𝐵 ) )
59 fz1f1o ⊢ ( ( 𝐹 supp 0 ) ∈ Fin → ( ( 𝐹 supp 0 ) = ∅ ∨ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) )
60 8 59 syl ⊢ ( 𝜑 → ( ( 𝐹 supp 0 ) = ∅ ∨ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) )
61 22 58 60 mpjaod ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) ∈ 𝐵 )