gsumzf1o - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > gsumzf1o		Structured version Visualization version GIF version

Theorem gsumzf1o 18434

Description: Re-index a finite group sum using a bijection. (Contributed by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 2-Jun-2019.)

**Hypotheses**
Ref	Expression
gsumzcl.b	⊢ 𝐵 = (Base‘𝐺)
gsumzcl.0	⊢ 0 = (0_g‘𝐺)
gsumzcl.z	⊢ 𝑍 = (Cntz‘𝐺)
gsumzcl.g	⊢ (𝜑 → 𝐺 ∈ Mnd)
gsumzcl.a	⊢ (𝜑 → 𝐴 ∈ 𝑉)
gsumzcl.f	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
gsumzcl.c	⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
gsumzcl.w	⊢ (𝜑 → 𝐹 finSupp 0 )
gsumzf1o.h	⊢ (𝜑 → 𝐻:𝐶–1-1-onto→𝐴)

**Assertion**
Ref	Expression
gsumzf1o	⊢ (𝜑 → (𝐺 Σ_g 𝐹) = (𝐺 Σ_g (𝐹 ∘ 𝐻)))

Proof of Theorem gsumzf1o Dummy variables 𝑓 𝑘 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		gsumzcl.g	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ Mnd)
2		gsumzcl.a	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
3		gsumzcl.0	. . . . . . . 8 ⊢ 0 = (0_g‘𝐺)
4	3	gsumz 17496	. . . . . . 7 ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σ_g (𝑘 ∈ 𝐴 ↦ 0 )) = 0 )
5	1, 2, 4	syl2anc 696	. . . . . 6 ⊢ (𝜑 → (𝐺 Σ_g (𝑘 ∈ 𝐴 ↦ 0 )) = 0 )
6		gsumzf1o.h	. . . . . . . . 9 ⊢ (𝜑 → 𝐻:𝐶–1-1-onto→𝐴)
7		f1of1 6249	. . . . . . . . 9 ⊢ (𝐻:𝐶–1-1-onto→𝐴 → 𝐻:𝐶–1-1→𝐴)
8	6, 7	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐻:𝐶–1-1→𝐴)
9		f1dmex 7253	. . . . . . . 8 ⊢ ((𝐻:𝐶–1-1→𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐶 ∈ V)
10	8, 2, 9	syl2anc 696	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ V)
11	3	gsumz 17496	. . . . . . 7 ⊢ ((𝐺 ∈ Mnd ∧ 𝐶 ∈ V) → (𝐺 Σ_g (𝑥 ∈ 𝐶 ↦ 0 )) = 0 )
12	1, 10, 11	syl2anc 696	. . . . . 6 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ 𝐶 ↦ 0 )) = 0 )
13	5, 12	eqtr4d 2761	. . . . 5 ⊢ (𝜑 → (𝐺 Σ_g (𝑘 ∈ 𝐴 ↦ 0 )) = (𝐺 Σ_g (𝑥 ∈ 𝐶 ↦ 0 )))
14	13	adantr 472	. . . 4 ⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → (𝐺 Σ_g (𝑘 ∈ 𝐴 ↦ 0 )) = (𝐺 Σ_g (𝑥 ∈ 𝐶 ↦ 0 )))
15		gsumzcl.f	. . . . . 6 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
16		fvex 6314	. . . . . . . 8 ⊢ (0_g‘𝐺) ∈ V
17	3, 16	eqeltri 2799	. . . . . . 7 ⊢ 0 ∈ V
18	17	a1i 11	. . . . . 6 ⊢ (𝜑 → 0 ∈ V)
19		ssid 3730	. . . . . . 7 ⊢ (𝐹 supp 0 ) ⊆ (𝐹 supp 0 )
20	19	a1i 11	. . . . . 6 ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ (𝐹 supp 0 ))
21	15, 2, 18, 20	gsumcllem 18430	. . . . 5 ⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → 𝐹 = (𝑘 ∈ 𝐴 ↦ 0 ))
22	21	oveq2d 6781	. . . 4 ⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → (𝐺 Σ_g 𝐹) = (𝐺 Σ_g (𝑘 ∈ 𝐴 ↦ 0 )))
23		f1of 6250	. . . . . . . . 9 ⊢ (𝐻:𝐶–1-1-onto→𝐴 → 𝐻:𝐶⟶𝐴)
24	6, 23	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐻:𝐶⟶𝐴)
25	24	adantr 472	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → 𝐻:𝐶⟶𝐴)
26	25	ffvelrnda 6474	. . . . . 6 ⊢ (((𝜑 ∧ (𝐹 supp 0 ) = ∅) ∧ 𝑥 ∈ 𝐶) → (𝐻‘𝑥) ∈ 𝐴)
27	25	feqmptd 6363	. . . . . 6 ⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → 𝐻 = (𝑥 ∈ 𝐶 ↦ (𝐻‘𝑥)))
28		eqidd 2725	. . . . . 6 ⊢ (𝑘 = (𝐻‘𝑥) → 0 = 0 )
29	26, 27, 21, 28	fmptco 6511	. . . . 5 ⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → (𝐹 ∘ 𝐻) = (𝑥 ∈ 𝐶 ↦ 0 ))
30	29	oveq2d 6781	. . . 4 ⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → (𝐺 Σ_g (𝐹 ∘ 𝐻)) = (𝐺 Σ_g (𝑥 ∈ 𝐶 ↦ 0 )))
31	14, 22, 30	3eqtr4d 2768	. . 3 ⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → (𝐺 Σ_g 𝐹) = (𝐺 Σ_g (𝐹 ∘ 𝐻)))
32	31	ex 449	. 2 ⊢ (𝜑 → ((𝐹 supp 0 ) = ∅ → (𝐺 Σ_g 𝐹) = (𝐺 Σ_g (𝐹 ∘ 𝐻))))
33		coass 5767	. . . . . . . . . . 11 ⊢ ((𝐻 ∘ ^◡𝐻) ∘ 𝑓) = (𝐻 ∘ (^◡𝐻 ∘ 𝑓))
34	6	adantr 472	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → 𝐻:𝐶–1-1-onto→𝐴)
35		f1ococnv2 6276	. . . . . . . . . . . . . 14 ⊢ (𝐻:𝐶–1-1-onto→𝐴 → (𝐻 ∘ ^◡𝐻) = ( I ↾ 𝐴))
36	34, 35	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐻 ∘ ^◡𝐻) = ( I ↾ 𝐴))
37	36	coeq1d 5391	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → ((𝐻 ∘ ^◡𝐻) ∘ 𝑓) = (( I ↾ 𝐴) ∘ 𝑓))
38		f1of1 6249	. . . . . . . . . . . . . . 15 ⊢ (𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) → 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1→(𝐹 supp 0 ))
39	38	ad2antll 767	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1→(𝐹 supp 0 ))
40		suppssdm 7428	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 supp 0 ) ⊆ dom 𝐹
41		fdm 6164	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)
42	15, 41	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom 𝐹 = 𝐴)
43	40, 42	syl5sseq 3759	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝐴)
44	43	adantr 472	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐹 supp 0 ) ⊆ 𝐴)
45		f1ss 6219	. . . . . . . . . . . . . 14 ⊢ ((𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1→(𝐹 supp 0 ) ∧ (𝐹 supp 0 ) ⊆ 𝐴) → 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1→𝐴)
46	39, 44, 45	syl2anc 696	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1→𝐴)
47		f1f 6214	. . . . . . . . . . . . 13 ⊢ (𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1→𝐴 → 𝑓:(1...(♯‘(𝐹 supp 0 )))⟶𝐴)
48		fcoi2 6192	. . . . . . . . . . . . 13 ⊢ (𝑓:(1...(♯‘(𝐹 supp 0 )))⟶𝐴 → (( I ↾ 𝐴) ∘ 𝑓) = 𝑓)
49	46, 47, 48	3syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (( I ↾ 𝐴) ∘ 𝑓) = 𝑓)
50	37, 49	eqtrd 2758	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → ((𝐻 ∘ ^◡𝐻) ∘ 𝑓) = 𝑓)
51	33, 50	syl5reqr 2773	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → 𝑓 = (𝐻 ∘ (^◡𝐻 ∘ 𝑓)))
52	51	coeq2d 5392	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐹 ∘ 𝑓) = (𝐹 ∘ (𝐻 ∘ (^◡𝐻 ∘ 𝑓))))
53		coass 5767	. . . . . . . . 9 ⊢ ((𝐹 ∘ 𝐻) ∘ (^◡𝐻 ∘ 𝑓)) = (𝐹 ∘ (𝐻 ∘ (^◡𝐻 ∘ 𝑓)))
54	52, 53	syl6eqr 2776	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐹 ∘ 𝑓) = ((𝐹 ∘ 𝐻) ∘ (^◡𝐻 ∘ 𝑓)))
55	54	seqeq3d 12924	. . . . . . 7 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → seq1((+_g‘𝐺), (𝐹 ∘ 𝑓)) = seq1((+_g‘𝐺), ((𝐹 ∘ 𝐻) ∘ (^◡𝐻 ∘ 𝑓))))
56	55	fveq1d 6306	. . . . . 6 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (seq1((+_g‘𝐺), (𝐹 ∘ 𝑓))‘(♯‘(𝐹 supp 0 ))) = (seq1((+_g‘𝐺), ((𝐹 ∘ 𝐻) ∘ (^◡𝐻 ∘ 𝑓)))‘(♯‘(𝐹 supp 0 ))))
57		gsumzcl.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐺)
58		eqid 2724	. . . . . . 7 ⊢ (+_g‘𝐺) = (+_g‘𝐺)
59		gsumzcl.z	. . . . . . 7 ⊢ 𝑍 = (Cntz‘𝐺)
60	1	adantr 472	. . . . . . 7 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → 𝐺 ∈ Mnd)
61	2	adantr 472	. . . . . . 7 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → 𝐴 ∈ 𝑉)
62	15	adantr 472	. . . . . . 7 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → 𝐹:𝐴⟶𝐵)
63		gsumzcl.c	. . . . . . . 8 ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
64	63	adantr 472	. . . . . . 7 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
65		simprl 811	. . . . . . 7 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (♯‘(𝐹 supp 0 )) ∈ ℕ)
66		f1ofo 6257	. . . . . . . . . 10 ⊢ (𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) → 𝑓:(1...(♯‘(𝐹 supp 0 )))–onto→(𝐹 supp 0 ))
67		forn 6231	. . . . . . . . . 10 ⊢ (𝑓:(1...(♯‘(𝐹 supp 0 )))–onto→(𝐹 supp 0 ) → ran 𝑓 = (𝐹 supp 0 ))
68	66, 67	syl 17	. . . . . . . . 9 ⊢ (𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) → ran 𝑓 = (𝐹 supp 0 ))
69	68	ad2antll 767	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → ran 𝑓 = (𝐹 supp 0 ))
70	19, 69	syl5sseqr 3760	. . . . . . 7 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐹 supp 0 ) ⊆ ran 𝑓)
71		eqid 2724	. . . . . . 7 ⊢ ((𝐹 ∘ 𝑓) supp 0 ) = ((𝐹 ∘ 𝑓) supp 0 )
72	57, 3, 58, 59, 60, 61, 62, 64, 65, 46, 70, 71	gsumval3 18429	. . . . . 6 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐺 Σ_g 𝐹) = (seq1((+_g‘𝐺), (𝐹 ∘ 𝑓))‘(♯‘(𝐹 supp 0 ))))
73	10	adantr 472	. . . . . . 7 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → 𝐶 ∈ V)
74		fco 6171	. . . . . . . . 9 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐻:𝐶⟶𝐴) → (𝐹 ∘ 𝐻):𝐶⟶𝐵)
75	15, 24, 74	syl2anc 696	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ∘ 𝐻):𝐶⟶𝐵)
76	75	adantr 472	. . . . . . 7 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐹 ∘ 𝐻):𝐶⟶𝐵)
77		rncoss 5493	. . . . . . . . 9 ⊢ ran (𝐹 ∘ 𝐻) ⊆ ran 𝐹
78	59	cntzidss 17891	. . . . . . . . 9 ⊢ ((ran 𝐹 ⊆ (𝑍‘ran 𝐹) ∧ ran (𝐹 ∘ 𝐻) ⊆ ran 𝐹) → ran (𝐹 ∘ 𝐻) ⊆ (𝑍‘ran (𝐹 ∘ 𝐻)))
79	63, 77, 78	sylancl 697	. . . . . . . 8 ⊢ (𝜑 → ran (𝐹 ∘ 𝐻) ⊆ (𝑍‘ran (𝐹 ∘ 𝐻)))
80	79	adantr 472	. . . . . . 7 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → ran (𝐹 ∘ 𝐻) ⊆ (𝑍‘ran (𝐹 ∘ 𝐻)))
81		f1ocnv 6262	. . . . . . . . . 10 ⊢ (𝐻:𝐶–1-1-onto→𝐴 → ^◡𝐻:𝐴–1-1-onto→𝐶)
82		f1of1 6249	. . . . . . . . . 10 ⊢ (^◡𝐻:𝐴–1-1-onto→𝐶 → ^◡𝐻:𝐴–1-1→𝐶)
83	6, 81, 82	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → ^◡𝐻:𝐴–1-1→𝐶)
84	83	adantr 472	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → ^◡𝐻:𝐴–1-1→𝐶)
85		f1co 6223	. . . . . . . 8 ⊢ ((^◡𝐻:𝐴–1-1→𝐶 ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1→𝐴) → (^◡𝐻 ∘ 𝑓):(1...(♯‘(𝐹 supp 0 )))–1-1→𝐶)
86	84, 46, 85	syl2anc 696	. . . . . . 7 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (^◡𝐻 ∘ 𝑓):(1...(♯‘(𝐹 supp 0 )))–1-1→𝐶)
87	19	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐹 supp 0 ) ⊆ (𝐹 supp 0 ))
88		fex 6605	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → 𝐹 ∈ V)
89	15, 2, 88	syl2anc 696	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 ∈ V)
90		suppimacnv 7426	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ V ∧ 0 ∈ V) → (𝐹 supp 0 ) = (^◡𝐹 “ (V ∖ { 0 })))
91	89, 17, 90	sylancl 697	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹 supp 0 ) = (^◡𝐹 “ (V ∖ { 0 })))
92	91	eqcomd 2730	. . . . . . . . . . . 12 ⊢ (𝜑 → (^◡𝐹 “ (V ∖ { 0 })) = (𝐹 supp 0 ))
93	92	adantr 472	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (^◡𝐹 “ (V ∖ { 0 })) = (𝐹 supp 0 ))
94	87, 93, 69	3sstr4d 3754	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (^◡𝐹 “ (V ∖ { 0 })) ⊆ ran 𝑓)
95		imass2 5611	. . . . . . . . . 10 ⊢ ((^◡𝐹 “ (V ∖ { 0 })) ⊆ ran 𝑓 → (^◡𝐻 “ (^◡𝐹 “ (V ∖ { 0 }))) ⊆ (^◡𝐻 “ ran 𝑓))
96	94, 95	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (^◡𝐻 “ (^◡𝐹 “ (V ∖ { 0 }))) ⊆ (^◡𝐻 “ ran 𝑓))
97		cnvco 5415	. . . . . . . . . . 11 ⊢ ^◡(𝐹 ∘ 𝐻) = (^◡𝐻 ∘ ^◡𝐹)
98	97	imaeq1i 5573	. . . . . . . . . 10 ⊢ (^◡(𝐹 ∘ 𝐻) “ (V ∖ { 0 })) = ((^◡𝐻 ∘ ^◡𝐹) “ (V ∖ { 0 }))
99		imaco 5753	. . . . . . . . . 10 ⊢ ((^◡𝐻 ∘ ^◡𝐹) “ (V ∖ { 0 })) = (^◡𝐻 “ (^◡𝐹 “ (V ∖ { 0 })))
100	98, 99	eqtri 2746	. . . . . . . . 9 ⊢ (^◡(𝐹 ∘ 𝐻) “ (V ∖ { 0 })) = (^◡𝐻 “ (^◡𝐹 “ (V ∖ { 0 })))
101		rnco2 5755	. . . . . . . . 9 ⊢ ran (^◡𝐻 ∘ 𝑓) = (^◡𝐻 “ ran 𝑓)
102	96, 100, 101	3sstr4g 3752	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (^◡(𝐹 ∘ 𝐻) “ (V ∖ { 0 })) ⊆ ran (^◡𝐻 ∘ 𝑓))
103		f1oexrnex 7232	. . . . . . . . . . . . 13 ⊢ ((𝐻:𝐶–1-1-onto→𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐻 ∈ V)
104	6, 2, 103	syl2anc 696	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐻 ∈ V)
105		coexg 7234	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ V ∧ 𝐻 ∈ V) → (𝐹 ∘ 𝐻) ∈ V)
106	89, 104, 105	syl2anc 696	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹 ∘ 𝐻) ∈ V)
107		suppimacnv 7426	. . . . . . . . . . 11 ⊢ (((𝐹 ∘ 𝐻) ∈ V ∧ 0 ∈ V) → ((𝐹 ∘ 𝐻) supp 0 ) = (^◡(𝐹 ∘ 𝐻) “ (V ∖ { 0 })))
108	106, 17, 107	sylancl 697	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐹 ∘ 𝐻) supp 0 ) = (^◡(𝐹 ∘ 𝐻) “ (V ∖ { 0 })))
109	108	sseq1d 3738	. . . . . . . . 9 ⊢ (𝜑 → (((𝐹 ∘ 𝐻) supp 0 ) ⊆ ran (^◡𝐻 ∘ 𝑓) ↔ (^◡(𝐹 ∘ 𝐻) “ (V ∖ { 0 })) ⊆ ran (^◡𝐻 ∘ 𝑓)))
110	109	adantr 472	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (((𝐹 ∘ 𝐻) supp 0 ) ⊆ ran (^◡𝐻 ∘ 𝑓) ↔ (^◡(𝐹 ∘ 𝐻) “ (V ∖ { 0 })) ⊆ ran (^◡𝐻 ∘ 𝑓)))
111	102, 110	mpbird 247	. . . . . . 7 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → ((𝐹 ∘ 𝐻) supp 0 ) ⊆ ran (^◡𝐻 ∘ 𝑓))
112		eqid 2724	. . . . . . 7 ⊢ (((𝐹 ∘ 𝐻) ∘ (^◡𝐻 ∘ 𝑓)) supp 0 ) = (((𝐹 ∘ 𝐻) ∘ (^◡𝐻 ∘ 𝑓)) supp 0 )
113	57, 3, 58, 59, 60, 73, 76, 80, 65, 86, 111, 112	gsumval3 18429	. . . . . 6 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐺 Σ_g (𝐹 ∘ 𝐻)) = (seq1((+_g‘𝐺), ((𝐹 ∘ 𝐻) ∘ (^◡𝐻 ∘ 𝑓)))‘(♯‘(𝐹 supp 0 ))))
114	56, 72, 113	3eqtr4d 2768	. . . . 5 ⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐺 Σ_g 𝐹) = (𝐺 Σ_g (𝐹 ∘ 𝐻)))
115	114	expr 644	. . . 4 ⊢ ((𝜑 ∧ (♯‘(𝐹 supp 0 )) ∈ ℕ) → (𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) → (𝐺 Σ_g 𝐹) = (𝐺 Σ_g (𝐹 ∘ 𝐻))))
116	115	exlimdv 1974	. . 3 ⊢ ((𝜑 ∧ (♯‘(𝐹 supp 0 )) ∈ ℕ) → (∃𝑓 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) → (𝐺 Σ_g 𝐹) = (𝐺 Σ_g (𝐹 ∘ 𝐻))))
117	116	expimpd 630	. 2 ⊢ (𝜑 → (((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 )) → (𝐺 Σ_g 𝐹) = (𝐺 Σ_g (𝐹 ∘ 𝐻))))
118		gsumzcl.w	. . 3 ⊢ (𝜑 → 𝐹 finSupp 0 )
119		fsuppimp 8397	. . . 4 ⊢ (𝐹 finSupp 0 → (Fun 𝐹 ∧ (𝐹 supp 0 ) ∈ Fin))
120	119	simprd 482	. . 3 ⊢ (𝐹 finSupp 0 → (𝐹 supp 0 ) ∈ Fin)
121		fz1f1o 14561	. . 3 ⊢ ((𝐹 supp 0 ) ∈ Fin → ((𝐹 supp 0 ) = ∅ ∨ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))))
122	118, 120, 121	3syl 18	. 2 ⊢ (𝜑 → ((𝐹 supp 0 ) = ∅ ∨ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))))
123	32, 117, 122	mpjaod 395	1 ⊢ (𝜑 → (𝐺 Σ_g 𝐹) = (𝐺 Σ_g (𝐹 ∘ 𝐻)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∨ wo 382 ∧ wa 383 = wceq 1596 ∃wex 1817 ∈ wcel 2103 Vcvv 3304 ∖ cdif 3677 ⊆ wss 3680 ∅c0 4023 {csn 4285 class class class wbr 4760 ↦ cmpt 4837 I cid 5127 ^◡ccnv 5217 dom cdm 5218 ran crn 5219 ↾ cres 5220 “ cima 5221 ∘ ccom 5222 Fun wfun 5995 ⟶wf 5997 –1-1→wf1 5998 –onto→wfo 5999 –1-1-onto→wf1o 6000 ‘cfv 6001 (class class class)co 6765 supp csupp 7415 Fincfn 8072 finSupp cfsupp 8391 1c1 10050 ℕcn 11133 ...cfz 12440 seqcseq 12916 ♯chash 13232 Basecbs 15980 +_gcplusg 16064 0_gc0g 16223 Σ_g cgsu 16224 Mndcmnd 17416 Cntzccntz 17869

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1835 ax-4 1850 ax-5 1952 ax-6 2018 ax-7 2054 ax-8 2105 ax-9 2112 ax-10 2132 ax-11 2147 ax-12 2160 ax-13 2355 ax-ext 2704 ax-rep 4879 ax-sep 4889 ax-nul 4897 ax-pow 4948 ax-pr 5011 ax-un 7066 ax-cnex 10105 ax-resscn 10106 ax-1cn 10107 ax-icn 10108 ax-addcl 10109 ax-addrcl 10110 ax-mulcl 10111 ax-mulrcl 10112 ax-mulcom 10113 ax-addass 10114 ax-mulass 10115 ax-distr 10116 ax-i2m1 10117 ax-1ne0 10118 ax-1rid 10119 ax-rnegex 10120 ax-rrecex 10121 ax-cnre 10122 ax-pre-lttri 10123 ax-pre-lttrn 10124 ax-pre-ltadd 10125 ax-pre-mulgt0 10126

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1599 df-ex 1818 df-nf 1823 df-sb 2011 df-eu 2575 df-mo 2576 df-clab 2711 df-cleq 2717 df-clel 2720 df-nfc 2855 df-ne 2897 df-nel 3000 df-ral 3019 df-rex 3020 df-reu 3021 df-rmo 3022 df-rab 3023 df-v 3306 df-sbc 3542 df-csb 3640 df-dif 3683 df-un 3685 df-in 3687 df-ss 3694 df-pss 3696 df-nul 4024 df-if 4195 df-pw 4268 df-sn 4286 df-pr 4288 df-tp 4290 df-op 4292 df-uni 4545 df-int 4584 df-iun 4630 df-br 4761 df-opab 4821 df-mpt 4838 df-tr 4861 df-id 5128 df-eprel 5133 df-po 5139 df-so 5140 df-fr 5177 df-se 5178 df-we 5179 df-xp 5224 df-rel 5225 df-cnv 5226 df-co 5227 df-dm 5228 df-rn 5229 df-res 5230 df-ima 5231 df-pred 5793 df-ord 5839 df-on 5840 df-lim 5841 df-suc 5842 df-iota 5964 df-fun 6003 df-fn 6004 df-f 6005 df-f1 6006 df-fo 6007 df-f1o 6008 df-fv 6009 df-isom 6010 df-riota 6726 df-ov 6768 df-oprab 6769 df-mpt2 6770 df-om 7183 df-1st 7285 df-2nd 7286 df-supp 7416 df-wrecs 7527 df-recs 7588 df-rdg 7626 df-1o 7680 df-oadd 7684 df-er 7862 df-en 8073 df-dom 8074 df-sdom 8075 df-fin 8076 df-fsupp 8392 df-oi 8531 df-card 8878 df-pnf 10189 df-mnf 10190 df-xr 10191 df-ltxr 10192 df-le 10193 df-sub 10381 df-neg 10382 df-nn 11134 df-n0 11406 df-z 11491 df-uz 11801 df-fz 12441 df-fzo 12581 df-seq 12917 df-hash 13233 df-0g 16225 df-gsum 16226 df-mgm 17364 df-sgrp 17406 df-mnd 17417 df-cntz 17871

This theorem is referenced by: gsumf1o 18438 smadiadetlem3 20597

W3C validator