gsumzres - Metamath Proof Explorer

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

Theorem gsumzres 18310

Description: Extend a finite group sum by padding outside with zeroes. (Contributed by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 31-May-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 𝐹))
gsumzres.s	⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝑊)
gsumzres.w	⊢ (𝜑 → 𝐹 finSupp 0 )

**Assertion**
Ref	Expression
gsumzres	⊢ (𝜑 → (𝐺 Σ_g (𝐹 ↾ 𝑊)) = (𝐺 Σ_g 𝐹))

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

Step	Hyp	Ref	Expression
1		gsumzcl.g	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ Mnd)
2		gsumzcl.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
3		inex1g 4801	. . . . . . . 8 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝑊) ∈ V)
4	2, 3	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝐴 ∩ 𝑊) ∈ V)
5		gsumzcl.0	. . . . . . . 8 ⊢ 0 = (0_g‘𝐺)
6	5	gsumz 17374	. . . . . . 7 ⊢ ((𝐺 ∈ Mnd ∧ (𝐴 ∩ 𝑊) ∈ V) → (𝐺 Σ_g (𝑘 ∈ (𝐴 ∩ 𝑊) ↦ 0 )) = 0 )
7	1, 4, 6	syl2anc 693	. . . . . 6 ⊢ (𝜑 → (𝐺 Σ_g (𝑘 ∈ (𝐴 ∩ 𝑊) ↦ 0 )) = 0 )
8	5	gsumz 17374	. . . . . . 7 ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σ_g (𝑘 ∈ 𝐴 ↦ 0 )) = 0 )
9	1, 2, 8	syl2anc 693	. . . . . 6 ⊢ (𝜑 → (𝐺 Σ_g (𝑘 ∈ 𝐴 ↦ 0 )) = 0 )
10	7, 9	eqtr4d 2659	. . . . 5 ⊢ (𝜑 → (𝐺 Σ_g (𝑘 ∈ (𝐴 ∩ 𝑊) ↦ 0 )) = (𝐺 Σ_g (𝑘 ∈ 𝐴 ↦ 0 )))
11	10	adantr 481	. . . 4 ⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → (𝐺 Σ_g (𝑘 ∈ (𝐴 ∩ 𝑊) ↦ 0 )) = (𝐺 Σ_g (𝑘 ∈ 𝐴 ↦ 0 )))
12		resres 5409	. . . . . . . 8 ⊢ ((𝐹 ↾ 𝐴) ↾ 𝑊) = (𝐹 ↾ (𝐴 ∩ 𝑊))
13		gsumzcl.f	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
14		ffn 6045	. . . . . . . . . 10 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
15		fnresdm 6000	. . . . . . . . . 10 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)
16	13, 14, 15	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 ↾ 𝐴) = 𝐹)
17	16	reseq1d 5395	. . . . . . . 8 ⊢ (𝜑 → ((𝐹 ↾ 𝐴) ↾ 𝑊) = (𝐹 ↾ 𝑊))
18	12, 17	syl5eqr 2670	. . . . . . 7 ⊢ (𝜑 → (𝐹 ↾ (𝐴 ∩ 𝑊)) = (𝐹 ↾ 𝑊))
19	18	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → (𝐹 ↾ (𝐴 ∩ 𝑊)) = (𝐹 ↾ 𝑊))
20		fvex 6201	. . . . . . . . . . 11 ⊢ (0_g‘𝐺) ∈ V
21	5, 20	eqeltri 2697	. . . . . . . . . 10 ⊢ 0 ∈ V
22	21	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ V)
23		ssid 3624	. . . . . . . . . 10 ⊢ (𝐹 supp 0 ) ⊆ (𝐹 supp 0 )
24	23	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ (𝐹 supp 0 ))
25	13, 2, 22, 24	gsumcllem 18309	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → 𝐹 = (𝑘 ∈ 𝐴 ↦ 0 ))
26	25	reseq1d 5395	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → (𝐹 ↾ (𝐴 ∩ 𝑊)) = ((𝑘 ∈ 𝐴 ↦ 0 ) ↾ (𝐴 ∩ 𝑊)))
27		inss1 3833	. . . . . . . 8 ⊢ (𝐴 ∩ 𝑊) ⊆ 𝐴
28		resmpt 5449	. . . . . . . 8 ⊢ ((𝐴 ∩ 𝑊) ⊆ 𝐴 → ((𝑘 ∈ 𝐴 ↦ 0 ) ↾ (𝐴 ∩ 𝑊)) = (𝑘 ∈ (𝐴 ∩ 𝑊) ↦ 0 ))
29	27, 28	ax-mp 5	. . . . . . 7 ⊢ ((𝑘 ∈ 𝐴 ↦ 0 ) ↾ (𝐴 ∩ 𝑊)) = (𝑘 ∈ (𝐴 ∩ 𝑊) ↦ 0 )
30	26, 29	syl6eq 2672	. . . . . 6 ⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → (𝐹 ↾ (𝐴 ∩ 𝑊)) = (𝑘 ∈ (𝐴 ∩ 𝑊) ↦ 0 ))
31	19, 30	eqtr3d 2658	. . . . 5 ⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → (𝐹 ↾ 𝑊) = (𝑘 ∈ (𝐴 ∩ 𝑊) ↦ 0 ))
32	31	oveq2d 6666	. . . 4 ⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → (𝐺 Σ_g (𝐹 ↾ 𝑊)) = (𝐺 Σ_g (𝑘 ∈ (𝐴 ∩ 𝑊) ↦ 0 )))
33	25	oveq2d 6666	. . . 4 ⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → (𝐺 Σ_g 𝐹) = (𝐺 Σ_g (𝑘 ∈ 𝐴 ↦ 0 )))
34	11, 32, 33	3eqtr4d 2666	. . 3 ⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → (𝐺 Σ_g (𝐹 ↾ 𝑊)) = (𝐺 Σ_g 𝐹))
35	34	ex 450	. 2 ⊢ (𝜑 → ((𝐹 supp 0 ) = ∅ → (𝐺 Σ_g (𝐹 ↾ 𝑊)) = (𝐺 Σ_g 𝐹)))
36		f1ofo 6144	. . . . . . . . . . . 12 ⊢ (𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) → 𝑓:(1...(#‘(𝐹 supp 0 )))–onto→(𝐹 supp 0 ))
37		forn 6118	. . . . . . . . . . . 12 ⊢ (𝑓:(1...(#‘(𝐹 supp 0 )))–onto→(𝐹 supp 0 ) → ran 𝑓 = (𝐹 supp 0 ))
38	36, 37	syl 17	. . . . . . . . . . 11 ⊢ (𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) → ran 𝑓 = (𝐹 supp 0 ))
39	38	ad2antll 765	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → ran 𝑓 = (𝐹 supp 0 ))
40		gsumzres.s	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝑊)
41	40	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐹 supp 0 ) ⊆ 𝑊)
42	39, 41	eqsstrd 3639	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → ran 𝑓 ⊆ 𝑊)
43		cores 5638	. . . . . . . . 9 ⊢ (ran 𝑓 ⊆ 𝑊 → ((𝐹 ↾ 𝑊) ∘ 𝑓) = (𝐹 ∘ 𝑓))
44	42, 43	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → ((𝐹 ↾ 𝑊) ∘ 𝑓) = (𝐹 ∘ 𝑓))
45	44	seqeq3d 12809	. . . . . . 7 ⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → seq1((+_g‘𝐺), ((𝐹 ↾ 𝑊) ∘ 𝑓)) = seq1((+_g‘𝐺), (𝐹 ∘ 𝑓)))
46	45	fveq1d 6193	. . . . . 6 ⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (seq1((+_g‘𝐺), ((𝐹 ↾ 𝑊) ∘ 𝑓))‘(#‘(𝐹 supp 0 ))) = (seq1((+_g‘𝐺), (𝐹 ∘ 𝑓))‘(#‘(𝐹 supp 0 ))))
47		gsumzcl.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐺)
48		eqid 2622	. . . . . . 7 ⊢ (+_g‘𝐺) = (+_g‘𝐺)
49		gsumzcl.z	. . . . . . 7 ⊢ 𝑍 = (Cntz‘𝐺)
50	1	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → 𝐺 ∈ Mnd)
51	4	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐴 ∩ 𝑊) ∈ V)
52	13	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → 𝐹:𝐴⟶𝐵)
53		fssres 6070	. . . . . . . . 9 ⊢ ((𝐹:𝐴⟶𝐵 ∧ (𝐴 ∩ 𝑊) ⊆ 𝐴) → (𝐹 ↾ (𝐴 ∩ 𝑊)):(𝐴 ∩ 𝑊)⟶𝐵)
54	52, 27, 53	sylancl 694	. . . . . . . 8 ⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐹 ↾ (𝐴 ∩ 𝑊)):(𝐴 ∩ 𝑊)⟶𝐵)
55	18	feq1d 6030	. . . . . . . . 9 ⊢ (𝜑 → ((𝐹 ↾ (𝐴 ∩ 𝑊)):(𝐴 ∩ 𝑊)⟶𝐵 ↔ (𝐹 ↾ 𝑊):(𝐴 ∩ 𝑊)⟶𝐵))
56	55	biimpa 501	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐹 ↾ (𝐴 ∩ 𝑊)):(𝐴 ∩ 𝑊)⟶𝐵) → (𝐹 ↾ 𝑊):(𝐴 ∩ 𝑊)⟶𝐵)
57	54, 56	syldan 487	. . . . . . 7 ⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐹 ↾ 𝑊):(𝐴 ∩ 𝑊)⟶𝐵)
58		gsumzcl.c	. . . . . . . . 9 ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
59		resss 5422	. . . . . . . . . 10 ⊢ (𝐹 ↾ 𝑊) ⊆ 𝐹
60		rnss 5354	. . . . . . . . . 10 ⊢ ((𝐹 ↾ 𝑊) ⊆ 𝐹 → ran (𝐹 ↾ 𝑊) ⊆ ran 𝐹)
61	59, 60	ax-mp 5	. . . . . . . . 9 ⊢ ran (𝐹 ↾ 𝑊) ⊆ ran 𝐹
62	49	cntzidss 17770	. . . . . . . . 9 ⊢ ((ran 𝐹 ⊆ (𝑍‘ran 𝐹) ∧ ran (𝐹 ↾ 𝑊) ⊆ ran 𝐹) → ran (𝐹 ↾ 𝑊) ⊆ (𝑍‘ran (𝐹 ↾ 𝑊)))
63	58, 61, 62	sylancl 694	. . . . . . . 8 ⊢ (𝜑 → ran (𝐹 ↾ 𝑊) ⊆ (𝑍‘ran (𝐹 ↾ 𝑊)))
64	63	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → ran (𝐹 ↾ 𝑊) ⊆ (𝑍‘ran (𝐹 ↾ 𝑊)))
65		simprl 794	. . . . . . 7 ⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (#‘(𝐹 supp 0 )) ∈ ℕ)
66		f1of1 6136	. . . . . . . . 9 ⊢ (𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) → 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1→(𝐹 supp 0 ))
67	66	ad2antll 765	. . . . . . . 8 ⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1→(𝐹 supp 0 ))
68		suppssdm 7308	. . . . . . . . . . 11 ⊢ (𝐹 supp 0 ) ⊆ dom 𝐹
69		fdm 6051	. . . . . . . . . . . 12 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)
70	13, 69	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝐹 = 𝐴)
71	68, 70	syl5sseq 3653	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝐴)
72	71, 40	ssind 3837	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ (𝐴 ∩ 𝑊))
73	72	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐹 supp 0 ) ⊆ (𝐴 ∩ 𝑊))
74		f1ss 6106	. . . . . . . 8 ⊢ ((𝑓:(1...(#‘(𝐹 supp 0 )))–1-1→(𝐹 supp 0 ) ∧ (𝐹 supp 0 ) ⊆ (𝐴 ∩ 𝑊)) → 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1→(𝐴 ∩ 𝑊))
75	67, 73, 74	syl2anc 693	. . . . . . 7 ⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1→(𝐴 ∩ 𝑊))
76		fex 6490	. . . . . . . . . . . . 13 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → 𝐹 ∈ V)
77	13, 2, 76	syl2anc 693	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ∈ V)
78		ressuppss 7314	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ V ∧ 0 ∈ V) → ((𝐹 ↾ 𝑊) supp 0 ) ⊆ (𝐹 supp 0 ))
79	77, 21, 78	sylancl 694	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐹 ↾ 𝑊) supp 0 ) ⊆ (𝐹 supp 0 ))
80		sseq2 3627	. . . . . . . . . . 11 ⊢ (ran 𝑓 = (𝐹 supp 0 ) → (((𝐹 ↾ 𝑊) supp 0 ) ⊆ ran 𝑓 ↔ ((𝐹 ↾ 𝑊) supp 0 ) ⊆ (𝐹 supp 0 )))
81	79, 80	syl5ibr 236	. . . . . . . . . 10 ⊢ (ran 𝑓 = (𝐹 supp 0 ) → (𝜑 → ((𝐹 ↾ 𝑊) supp 0 ) ⊆ ran 𝑓))
82	36, 37, 81	3syl 18	. . . . . . . . 9 ⊢ (𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) → (𝜑 → ((𝐹 ↾ 𝑊) supp 0 ) ⊆ ran 𝑓))
83	82	adantl 482	. . . . . . . 8 ⊢ (((#‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 )) → (𝜑 → ((𝐹 ↾ 𝑊) supp 0 ) ⊆ ran 𝑓))
84	83	impcom 446	. . . . . . 7 ⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → ((𝐹 ↾ 𝑊) supp 0 ) ⊆ ran 𝑓)
85		eqid 2622	. . . . . . 7 ⊢ (((𝐹 ↾ 𝑊) ∘ 𝑓) supp 0 ) = (((𝐹 ↾ 𝑊) ∘ 𝑓) supp 0 )
86	47, 5, 48, 49, 50, 51, 57, 64, 65, 75, 84, 85	gsumval3 18308	. . . . . 6 ⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐺 Σ_g (𝐹 ↾ 𝑊)) = (seq1((+_g‘𝐺), ((𝐹 ↾ 𝑊) ∘ 𝑓))‘(#‘(𝐹 supp 0 ))))
87	2	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → 𝐴 ∈ 𝑉)
88	58	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
89	71	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐹 supp 0 ) ⊆ 𝐴)
90		f1ss 6106	. . . . . . . 8 ⊢ ((𝑓:(1...(#‘(𝐹 supp 0 )))–1-1→(𝐹 supp 0 ) ∧ (𝐹 supp 0 ) ⊆ 𝐴) → 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1→𝐴)
91	67, 89, 90	syl2anc 693	. . . . . . 7 ⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1→𝐴)
92	23, 39	syl5sseqr 3654	. . . . . . 7 ⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐹 supp 0 ) ⊆ ran 𝑓)
93		eqid 2622	. . . . . . 7 ⊢ ((𝐹 ∘ 𝑓) supp 0 ) = ((𝐹 ∘ 𝑓) supp 0 )
94	47, 5, 48, 49, 50, 87, 52, 88, 65, 91, 92, 93	gsumval3 18308	. . . . . 6 ⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐺 Σ_g 𝐹) = (seq1((+_g‘𝐺), (𝐹 ∘ 𝑓))‘(#‘(𝐹 supp 0 ))))
95	46, 86, 94	3eqtr4d 2666	. . . . 5 ⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧ 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐺 Σ_g (𝐹 ↾ 𝑊)) = (𝐺 Σ_g 𝐹))
96	95	expr 643	. . . 4 ⊢ ((𝜑 ∧ (#‘(𝐹 supp 0 )) ∈ ℕ) → (𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) → (𝐺 Σ_g (𝐹 ↾ 𝑊)) = (𝐺 Σ_g 𝐹)))
97	96	exlimdv 1861	. . 3 ⊢ ((𝜑 ∧ (#‘(𝐹 supp 0 )) ∈ ℕ) → (∃𝑓 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) → (𝐺 Σ_g (𝐹 ↾ 𝑊)) = (𝐺 Σ_g 𝐹)))
98	97	expimpd 629	. 2 ⊢ (𝜑 → (((#‘(𝐹 supp 0 )) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 )) → (𝐺 Σ_g (𝐹 ↾ 𝑊)) = (𝐺 Σ_g 𝐹)))
99		gsumzres.w	. . 3 ⊢ (𝜑 → 𝐹 finSupp 0 )
100		fsuppimp 8281	. . . 4 ⊢ (𝐹 finSupp 0 → (Fun 𝐹 ∧ (𝐹 supp 0 ) ∈ Fin))
101	100	simprd 479	. . 3 ⊢ (𝐹 finSupp 0 → (𝐹 supp 0 ) ∈ Fin)
102		fz1f1o 14441	. . 3 ⊢ ((𝐹 supp 0 ) ∈ Fin → ((𝐹 supp 0 ) = ∅ ∨ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))))
103	99, 101, 102	3syl 18	. 2 ⊢ (𝜑 → ((𝐹 supp 0 ) = ∅ ∨ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))))
104	35, 98, 103	mpjaod 396	1 ⊢ (𝜑 → (𝐺 Σ_g (𝐹 ↾ 𝑊)) = (𝐺 Σ_g 𝐹))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∨ wo 383 ∧ wa 384 = wceq 1483 ∃wex 1704 ∈ wcel 1990 Vcvv 3200 ∩ cin 3573 ⊆ wss 3574 ∅c0 3915 class class class wbr 4653 ↦ cmpt 4729 dom cdm 5114 ran crn 5115 ↾ cres 5116 ∘ ccom 5118 Fun wfun 5882 Fn wfn 5883 ⟶wf 5884 –1-1→wf1 5885 –onto→wfo 5886 –1-1-onto→wf1o 5887 ‘cfv 5888 (class class class)co 6650 supp csupp 7295 Fincfn 7955 finSupp cfsupp 8275 1c1 9937 ℕcn 11020 ...cfz 12326 seqcseq 12801 #chash 13117 Basecbs 15857 +_gcplusg 15941 0_gc0g 16100 Σ_g cgsu 16101 Mndcmnd 17294 Cntzccntz 17748

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-supp 7296 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fsupp 8276 df-oi 8415 df-card 8765 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-n0 11293 df-z 11378 df-uz 11688 df-fz 12327 df-fzo 12466 df-seq 12802 df-hash 13118 df-0g 16102 df-gsum 16103 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-cntz 17750

This theorem is referenced by: gsumres 18314 gsumzsplit 18327 gsumpt 18361 dmdprdsplitlem 18436 dpjidcl 18457 mplcoe5 19468

W3C validator