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

Metamath Proof Explorer

Theorem gsumzmhm

Proof