Metamath Proof Explorer

Theorem gsumzmhm

Description: Apply a group homomorphism to a group sum. (Contributed by Mario Carneiro, 24-Apr-2016) (Revised by AV, 6-Jun-2019)

Ref Expression
Hypotheses gsumzmhm.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsumzmhm.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
gsumzmhm.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
gsumzmhm.h ⊢ ( 𝜑 → 𝐻 ∈ Mnd )
gsumzmhm.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
gsumzmhm.k ⊢ ( 𝜑 → 𝐾 ∈ ( 𝐺 MndHom 𝐻 ) )
gsumzmhm.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
gsumzmhm.c ⊢ ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
gsumzmhm.0 ⊢ 0 = ( 0g ‘ 𝐺 )
gsumzmhm.w ⊢ ( 𝜑 → 𝐹 finSupp 0 )
Assertion gsumzmhm ( 𝜑 → ( 𝐻 Σg ( 𝐾 ∘ 𝐹 ) ) = ( 𝐾 ‘ ( 𝐺 Σg 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 gsumzmhm.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsumzmhm.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
3 gsumzmhm.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
4 gsumzmhm.h ⊢ ( 𝜑 → 𝐻 ∈ Mnd )
5 gsumzmhm.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6 gsumzmhm.k ⊢ ( 𝜑 → 𝐾 ∈ ( 𝐺 MndHom 𝐻 ) )
7 gsumzmhm.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
8 gsumzmhm.c ⊢ ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
9 gsumzmhm.0 ⊢ 0 = ( 0g ‘ 𝐺 )
10 gsumzmhm.w ⊢ ( 𝜑 → 𝐹 finSupp 0 )
11 eqid ⊢ ( 0g ‘ 𝐻 ) = ( 0g ‘ 𝐻 )
12 11 gsumz ⊢ ( ( 𝐻 ∈ Mnd ∧ 𝐴 ∈ 𝑉 ) → ( 𝐻 Σg ( 𝑘 ∈ 𝐴 ↦ ( 0g ‘ 𝐻 ) ) ) = ( 0g ‘ 𝐻 ) )
13 4 5 12 syl2anc ⊢ ( 𝜑 → ( 𝐻 Σg ( 𝑘 ∈ 𝐴 ↦ ( 0g ‘ 𝐻 ) ) ) = ( 0g ‘ 𝐻 ) )
14 13 adantr ⊢ ( ( 𝜑 ∧ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) = ∅ ) → ( 𝐻 Σg ( 𝑘 ∈ 𝐴 ↦ ( 0g ‘ 𝐻 ) ) ) = ( 0g ‘ 𝐻 ) )
15 9 11 mhm0 ⊢ ( 𝐾 ∈ ( 𝐺 MndHom 𝐻 ) → ( 𝐾 ‘ 0 ) = ( 0g ‘ 𝐻 ) )
16 6 15 syl ⊢ ( 𝜑 → ( 𝐾 ‘ 0 ) = ( 0g ‘ 𝐻 ) )
17 16 adantr ⊢ ( ( 𝜑 ∧ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) = ∅ ) → ( 𝐾 ‘ 0 ) = ( 0g ‘ 𝐻 ) )
18 14 17 eqtr4d ⊢ ( ( 𝜑 ∧ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) = ∅ ) → ( 𝐻 Σg ( 𝑘 ∈ 𝐴 ↦ ( 0g ‘ 𝐻 ) ) ) = ( 𝐾 ‘ 0 ) )
19 1 9 mndidcl ⊢ ( 𝐺 ∈ Mnd → 0 ∈ 𝐵 )
20 3 19 syl ⊢ ( 𝜑 → 0 ∈ 𝐵 )
21 20 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) = ∅ ) ∧ 𝑘 ∈ 𝐴 ) → 0 ∈ 𝐵 )
22 9 fvexi ⊢ 0 ∈ V
23 22 a1i ⊢ ( 𝜑 → 0 ∈ V )
24 fex ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → 𝐹 ∈ V )
25 7 5 24 syl2anc ⊢ ( 𝜑 → 𝐹 ∈ V )
26 suppimacnv ⊢ ( ( 𝐹 ∈ V ∧ 0 ∈ V ) → ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) )
27 25 23 26 syl2anc ⊢ ( 𝜑 → ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) )
28 ssid ⊢ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ⊆ ( ◡ 𝐹 “ ( V ∖ { 0 } ) )
29 27 28 eqsstrdi ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) )
30 7 5 23 29 gsumcllem ⊢ ( ( 𝜑 ∧ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) = ∅ ) → 𝐹 = ( 𝑘 ∈ 𝐴 ↦ 0 ) )
31 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
32 1 31 mhmf ⊢ ( 𝐾 ∈ ( 𝐺 MndHom 𝐻 ) → 𝐾 : 𝐵 ⟶ ( Base ‘ 𝐻 ) )
33 6 32 syl ⊢ ( 𝜑 → 𝐾 : 𝐵 ⟶ ( Base ‘ 𝐻 ) )
34 33 feqmptd ⊢ ( 𝜑 → 𝐾 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐾 ‘ 𝑥 ) ) )
35 34 adantr ⊢ ( ( 𝜑 ∧ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) = ∅ ) → 𝐾 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐾 ‘ 𝑥 ) ) )
36 fveq2 ⊢ ( 𝑥 = 0 → ( 𝐾 ‘ 𝑥 ) = ( 𝐾 ‘ 0 ) )
37 21 30 35 36 fmptco ⊢ ( ( 𝜑 ∧ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) = ∅ ) → ( 𝐾 ∘ 𝐹 ) = ( 𝑘 ∈ 𝐴 ↦ ( 𝐾 ‘ 0 ) ) )
38 16 mpteq2dv ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ ( 𝐾 ‘ 0 ) ) = ( 𝑘 ∈ 𝐴 ↦ ( 0g ‘ 𝐻 ) ) )
39 38 adantr ⊢ ( ( 𝜑 ∧ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) = ∅ ) → ( 𝑘 ∈ 𝐴 ↦ ( 𝐾 ‘ 0 ) ) = ( 𝑘 ∈ 𝐴 ↦ ( 0g ‘ 𝐻 ) ) )
40 37 39 eqtrd ⊢ ( ( 𝜑 ∧ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) = ∅ ) → ( 𝐾 ∘ 𝐹 ) = ( 𝑘 ∈ 𝐴 ↦ ( 0g ‘ 𝐻 ) ) )
41 40 oveq2d ⊢ ( ( 𝜑 ∧ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) = ∅ ) → ( 𝐻 Σg ( 𝐾 ∘ 𝐹 ) ) = ( 𝐻 Σg ( 𝑘 ∈ 𝐴 ↦ ( 0g ‘ 𝐻 ) ) ) )
42 30 oveq2d ⊢ ( ( 𝜑 ∧ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) = ∅ ) → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 0 ) ) )
43 9 gsumz ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉 ) → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 0 ) ) = 0 )
44 3 5 43 syl2anc ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 0 ) ) = 0 )
45 44 adantr ⊢ ( ( 𝜑 ∧ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) = ∅ ) → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 0 ) ) = 0 )
46 42 45 eqtrd ⊢ ( ( 𝜑 ∧ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) = ∅ ) → ( 𝐺 Σg 𝐹 ) = 0 )
47 46 fveq2d ⊢ ( ( 𝜑 ∧ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) = ∅ ) → ( 𝐾 ‘ ( 𝐺 Σg 𝐹 ) ) = ( 𝐾 ‘ 0 ) )
48 18 41 47 3eqtr4d ⊢ ( ( 𝜑 ∧ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) = ∅ ) → ( 𝐻 Σg ( 𝐾 ∘ 𝐹 ) ) = ( 𝐾 ‘ ( 𝐺 Σg 𝐹 ) ) )
49 48 ex ⊢ ( 𝜑 → ( ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) = ∅ → ( 𝐻 Σg ( 𝐾 ∘ 𝐹 ) ) = ( 𝐾 ‘ ( 𝐺 Σg 𝐹 ) ) ) )
50 3 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → 𝐺 ∈ Mnd )
51 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
52 1 51 mndcl ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐵 )
53 52 3expb ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐵 )
54 50 53 sylan ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐵 )
55 f1of1 ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) → 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) )
56 55 ad2antll ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) )
57 cnvimass ⊢ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ⊆ dom 𝐹
58 7 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
59 57 58 fssdm ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ⊆ 𝐴 )
60 f1ss ⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ∧ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ⊆ 𝐴 ) → 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1→ 𝐴 )
61 56 59 60 syl2anc ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1→ 𝐴 )
62 f1f ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1→ 𝐴 → 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ⟶ 𝐴 )
63 61 62 syl ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ⟶ 𝐴 )
64 fco ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ⟶ 𝐴 ) → ( 𝐹 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ⟶ 𝐵 )
65 7 63 64 syl2an2r ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( 𝐹 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ⟶ 𝐵 )
66 65 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ) → ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑥 ) ∈ 𝐵 )
67 simprl ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ )
68 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
69 67 68 eleqtrdi ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ( ℤ≥ ‘ 1 ) )
70 6 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → 𝐾 ∈ ( 𝐺 MndHom 𝐻 ) )
71 eqid ⊢ ( +g ‘ 𝐻 ) = ( +g ‘ 𝐻 )
72 1 51 71 mhmlin ⊢ ( ( 𝐾 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝐾 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = ( ( 𝐾 ‘ 𝑥 ) ( +g ‘ 𝐻 ) ( 𝐾 ‘ 𝑦 ) ) )
73 72 3expb ⊢ ( ( 𝐾 ∈ ( 𝐺 MndHom 𝐻 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐾 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = ( ( 𝐾 ‘ 𝑥 ) ( +g ‘ 𝐻 ) ( 𝐾 ‘ 𝑦 ) ) )
74 70 73 sylan ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐾 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = ( ( 𝐾 ‘ 𝑥 ) ( +g ‘ 𝐻 ) ( 𝐾 ‘ 𝑦 ) ) )
75 coass ⊢ ( ( 𝐾 ∘ 𝐹 ) ∘ 𝑓 ) = ( 𝐾 ∘ ( 𝐹 ∘ 𝑓 ) )
76 75 fveq1i ⊢ ( ( ( 𝐾 ∘ 𝐹 ) ∘ 𝑓 ) ‘ 𝑥 ) = ( ( 𝐾 ∘ ( 𝐹 ∘ 𝑓 ) ) ‘ 𝑥 )
77 fvco3 ⊢ ( ( ( 𝐹 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ⟶ 𝐵 ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ) → ( ( 𝐾 ∘ ( 𝐹 ∘ 𝑓 ) ) ‘ 𝑥 ) = ( 𝐾 ‘ ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑥 ) ) )
78 65 77 sylan ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ) → ( ( 𝐾 ∘ ( 𝐹 ∘ 𝑓 ) ) ‘ 𝑥 ) = ( 𝐾 ‘ ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑥 ) ) )
79 76 78 syl5req ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ) → ( 𝐾 ‘ ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑥 ) ) = ( ( ( 𝐾 ∘ 𝐹 ) ∘ 𝑓 ) ‘ 𝑥 ) )
80 54 66 69 74 79 seqhomo ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( 𝐾 ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ) = ( seq 1 ( ( +g ‘ 𝐻 ) , ( ( 𝐾 ∘ 𝐹 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) )
81 5 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → 𝐴 ∈ 𝑉 )
82 8 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
83 29 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( 𝐹 supp 0 ) ⊆ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) )
84 f1ofo ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) → 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) )
85 forn ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) → ran 𝑓 = ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) )
86 84 85 syl ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) → ran 𝑓 = ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) )
87 86 ad2antll ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ran 𝑓 = ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) )
88 83 87 sseqtrrd ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( 𝐹 supp 0 ) ⊆ ran 𝑓 )
89 eqid ⊢ ( ( 𝐹 ∘ 𝑓 ) supp 0 ) = ( ( 𝐹 ∘ 𝑓 ) supp 0 )
90 1 9 51 2 50 81 58 82 67 61 88 89 gsumval3 ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) )
91 90 fveq2d ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( 𝐾 ‘ ( 𝐺 Σg 𝐹 ) ) = ( 𝐾 ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ) )
92 eqid ⊢ ( Cntz ‘ 𝐻 ) = ( Cntz ‘ 𝐻 )
93 4 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → 𝐻 ∈ Mnd )
94 fco ⊢ ( ( 𝐾 : 𝐵 ⟶ ( Base ‘ 𝐻 ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐾 ∘ 𝐹 ) : 𝐴 ⟶ ( Base ‘ 𝐻 ) )
95 33 58 94 syl2an2r ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( 𝐾 ∘ 𝐹 ) : 𝐴 ⟶ ( Base ‘ 𝐻 ) )
96 2 92 cntzmhm2 ⊢ ( ( 𝐾 ∈ ( 𝐺 MndHom 𝐻 ) ∧ ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) ) → ( 𝐾 “ ran 𝐹 ) ⊆ ( ( Cntz ‘ 𝐻 ) ‘ ( 𝐾 “ ran 𝐹 ) ) )
97 6 82 96 syl2an2r ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( 𝐾 “ ran 𝐹 ) ⊆ ( ( Cntz ‘ 𝐻 ) ‘ ( 𝐾 “ ran 𝐹 ) ) )
98 rnco2 ⊢ ran ( 𝐾 ∘ 𝐹 ) = ( 𝐾 “ ran 𝐹 )
99 98 fveq2i ⊢ ( ( Cntz ‘ 𝐻 ) ‘ ran ( 𝐾 ∘ 𝐹 ) ) = ( ( Cntz ‘ 𝐻 ) ‘ ( 𝐾 “ ran 𝐹 ) )
100 97 98 99 3sstr4g ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ran ( 𝐾 ∘ 𝐹 ) ⊆ ( ( Cntz ‘ 𝐻 ) ‘ ran ( 𝐾 ∘ 𝐹 ) ) )
101 eldifi ⊢ ( 𝑥 ∈ ( 𝐴 ∖ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) → 𝑥 ∈ 𝐴 )
102 fvco3 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑥 ) = ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) )
103 58 101 102 syl2an ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑥 ) = ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) )
104 22 a1i ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → 0 ∈ V )
105 58 83 81 104 suppssr ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( 𝐹 ‘ 𝑥 ) = 0 )
106 105 fveq2d ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐾 ‘ 0 ) )
107 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( 𝐾 ‘ 0 ) = ( 0g ‘ 𝐻 ) )
108 103 106 107 3eqtrd ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑥 ) = ( 0g ‘ 𝐻 ) )
109 95 108 suppss ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( ( 𝐾 ∘ 𝐹 ) supp ( 0g ‘ 𝐻 ) ) ⊆ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) )
110 109 87 sseqtrrd ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( ( 𝐾 ∘ 𝐹 ) supp ( 0g ‘ 𝐻 ) ) ⊆ ran 𝑓 )
111 eqid ⊢ ( ( ( 𝐾 ∘ 𝐹 ) ∘ 𝑓 ) supp ( 0g ‘ 𝐻 ) ) = ( ( ( 𝐾 ∘ 𝐹 ) ∘ 𝑓 ) supp ( 0g ‘ 𝐻 ) )
112 31 11 71 92 93 81 95 100 67 61 110 111 gsumval3 ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( 𝐻 Σg ( 𝐾 ∘ 𝐹 ) ) = ( seq 1 ( ( +g ‘ 𝐻 ) , ( ( 𝐾 ∘ 𝐹 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) )
113 80 91 112 3eqtr4rd ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) → ( 𝐻 Σg ( 𝐾 ∘ 𝐹 ) ) = ( 𝐾 ‘ ( 𝐺 Σg 𝐹 ) ) )
114 113 expr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ) → ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) → ( 𝐻 Σg ( 𝐾 ∘ 𝐹 ) ) = ( 𝐾 ‘ ( 𝐺 Σg 𝐹 ) ) ) )
115 114 exlimdv ⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ) → ( ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) → ( 𝐻 Σg ( 𝐾 ∘ 𝐹 ) ) = ( 𝐾 ‘ ( 𝐺 Σg 𝐹 ) ) ) )
116 115 expimpd ⊢ ( 𝜑 → ( ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) → ( 𝐻 Σg ( 𝐾 ∘ 𝐹 ) ) = ( 𝐾 ‘ ( 𝐺 Σg 𝐹 ) ) ) )
117 10 fsuppimpd ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ∈ Fin )
118 27 117 eqeltrrd ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ∈ Fin )
119 fz1f1o ⊢ ( ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ∈ Fin → ( ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) = ∅ ∨ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) )
120 118 119 syl ⊢ ( 𝜑 → ( ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) = ∅ ∨ ( ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ) )
121 49 116 120 mpjaod ⊢ ( 𝜑 → ( 𝐻 Σg ( 𝐾 ∘ 𝐹 ) ) = ( 𝐾 ‘ ( 𝐺 Σg 𝐹 ) ) )