seqcoll2

Description: The function F contains a sparse set of nonzero values to be summed. The function G is an order isomorphism from the set of nonzero values of F to a 1-based finite sequence, and H collects these nonzero values together. Under these conditions, the sum over the values in H yields the same result as the sum over the original set F . (Contributed by Mario Carneiro, 13-Dec-2014)

	Ref	Expression
Hypotheses	seqcoll2.1	$⊢ (φ \land k \in S) \to Z \underset{˙}{+} k = k$
	seqcoll2.1b	$⊢ (φ \land k \in S) \to k \underset{˙}{+} Z = k$
	seqcoll2.c	$⊢ (φ \land (k \in S \land n \in S)) \to k \underset{˙}{+} n \in S$
	seqcoll2.a	$⊢ φ \to Z \in S$
	seqcoll2.2	$⊢ φ \to G {Isom}_{<, <} ((1 \dots \|A\|), A)$
	seqcoll2.3	$⊢ φ \to A \neq \emptyset$
	seqcoll2.5	$⊢ φ \to A \subseteq (M \dots N)$
	seqcoll2.6	$⊢ (φ \land k \in (M \dots N)) \to F (k) \in S$
	seqcoll2.7	$⊢ (φ \land k \in ((M \dots N) ∖ A)) \to F (k) = Z$
	seqcoll2.8	$⊢ (φ \land n \in (1 \dots \|A\|)) \to H (n) = F (G (n))$
Assertion	seqcoll2	$⊢ φ \to seq M (\underset{˙}{+}, F) (N) = seq 1 (\underset{˙}{+}, H) (\|A\|)$

Proof

Step	Hyp	Ref	Expression
1		seqcoll2.1	$⊢ (φ \land k \in S) \to Z \underset{˙}{+} k = k$
2		seqcoll2.1b	$⊢ (φ \land k \in S) \to k \underset{˙}{+} Z = k$
3		seqcoll2.c	$⊢ (φ \land (k \in S \land n \in S)) \to k \underset{˙}{+} n \in S$
4		seqcoll2.a	$⊢ φ \to Z \in S$
5		seqcoll2.2	$⊢ φ \to G {Isom}_{<, <} ((1 \dots \|A\|), A)$
6		seqcoll2.3	$⊢ φ \to A \neq \emptyset$
7		seqcoll2.5	$⊢ φ \to A \subseteq (M \dots N)$
8		seqcoll2.6	$⊢ (φ \land k \in (M \dots N)) \to F (k) \in S$
9		seqcoll2.7	$⊢ (φ \land k \in ((M \dots N) ∖ A)) \to F (k) = Z$
10		seqcoll2.8	$⊢ (φ \land n \in (1 \dots \|A\|)) \to H (n) = F (G (n))$
11		fzssuz	$⊢ (M \dots N) \subseteq ℤ_{\geq M}$
12		isof1o	$⊢ G {Isom}_{<, <} ((1 \dots \|A\|), A) \to G : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A$
13	5 12	syl	$⊢ φ \to G : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A$
14		f1of	$⊢ G : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to G : (1 \dots \|A\|) ⟶ A$
15	13 14	syl	$⊢ φ \to G : (1 \dots \|A\|) ⟶ A$
16		fzfi	$⊢ (M \dots N) \in Fin$
17		ssfi	$⊢ ((M \dots N) \in Fin \land A \subseteq (M \dots N)) \to A \in Fin$
18	16 7 17	sylancr	$⊢ φ \to A \in Fin$
19		hasheq0	$⊢ A \in Fin \to (\|A\| = 0 \leftrightarrow A = \emptyset)$
20	18 19	syl	$⊢ φ \to (\|A\| = 0 \leftrightarrow A = \emptyset)$
21	20	necon3bbid	$⊢ φ \to (\neg \|A\| = 0 \leftrightarrow A \neq \emptyset)$
22	6 21	mpbird	$⊢ φ \to \neg \|A\| = 0$
23		hashcl	$⊢ A \in Fin \to \|A\| \in ℕ_{0}$
24	18 23	syl	$⊢ φ \to \|A\| \in ℕ_{0}$
25		elnn0	$⊢ \|A\| \in ℕ_{0} \leftrightarrow (\|A\| \in ℕ \lor \|A\| = 0)$
26	24 25	sylib	$⊢ φ \to (\|A\| \in ℕ \lor \|A\| = 0)$
27	26	ord	$⊢ φ \to (\neg \|A\| \in ℕ \to \|A\| = 0)$
28	22 27	mt3d	$⊢ φ \to \|A\| \in ℕ$
29		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
30	28 29	eleqtrdi	$⊢ φ \to \|A\| \in ℤ_{\geq 1}$
31		eluzfz2	$⊢ \|A\| \in ℤ_{\geq 1} \to \|A\| \in (1 \dots \|A\|)$
32	30 31	syl	$⊢ φ \to \|A\| \in (1 \dots \|A\|)$
33	15 32	ffvelcdmd	$⊢ φ \to G (\|A\|) \in A$
34	7 33	sseldd	$⊢ φ \to G (\|A\|) \in (M \dots N)$
35	11 34	sselid	$⊢ φ \to G (\|A\|) \in ℤ_{\geq M}$
36		elfzuz3	$⊢ G (\|A\|) \in (M \dots N) \to N \in ℤ_{\geq G (\|A\|)}$
37	34 36	syl	$⊢ φ \to N \in ℤ_{\geq G (\|A\|)}$
38		fzss2	$⊢ N \in ℤ_{\geq G (\|A\|)} \to (M \dots G (\|A\|)) \subseteq (M \dots N)$
39	37 38	syl	$⊢ φ \to (M \dots G (\|A\|)) \subseteq (M \dots N)$
40	39	sselda	$⊢ (φ \land k \in (M \dots G (\|A\|))) \to k \in (M \dots N)$
41	40 8	syldan	$⊢ (φ \land k \in (M \dots G (\|A\|))) \to F (k) \in S$
42	35 41 3	seqcl	$⊢ φ \to seq M (\underset{˙}{+}, F) (G (\|A\|)) \in S$
43		peano2uz	$⊢ G (\|A\|) \in ℤ_{\geq M} \to G (\|A\|) + 1 \in ℤ_{\geq M}$
44	35 43	syl	$⊢ φ \to G (\|A\|) + 1 \in ℤ_{\geq M}$
45		fzss1	$⊢ G (\|A\|) + 1 \in ℤ_{\geq M} \to (G (\|A\|) + 1 \dots N) \subseteq (M \dots N)$
46	44 45	syl	$⊢ φ \to (G (\|A\|) + 1 \dots N) \subseteq (M \dots N)$
47	46	sselda	$⊢ (φ \land k \in (G (\|A\|) + 1 \dots N)) \to k \in (M \dots N)$
48		eluzelre	$⊢ G (\|A\|) \in ℤ_{\geq M} \to G (\|A\|) \in ℝ$
49	35 48	syl	$⊢ φ \to G (\|A\|) \in ℝ$
50	49	adantr	$⊢ (φ \land k \in (G (\|A\|) + 1 \dots N)) \to G (\|A\|) \in ℝ$
51		peano2re	$⊢ G (\|A\|) \in ℝ \to G (\|A\|) + 1 \in ℝ$
52	50 51	syl	$⊢ (φ \land k \in (G (\|A\|) + 1 \dots N)) \to G (\|A\|) + 1 \in ℝ$
53		elfzelz	$⊢ k \in (G (\|A\|) + 1 \dots N) \to k \in ℤ$
54	53	zred	$⊢ k \in (G (\|A\|) + 1 \dots N) \to k \in ℝ$
55	54	adantl	$⊢ (φ \land k \in (G (\|A\|) + 1 \dots N)) \to k \in ℝ$
56	50	ltp1d	$⊢ (φ \land k \in (G (\|A\|) + 1 \dots N)) \to G (\|A\|) < G (\|A\|) + 1$
57		elfzle1	$⊢ k \in (G (\|A\|) + 1 \dots N) \to G (\|A\|) + 1 \leq k$
58	57	adantl	$⊢ (φ \land k \in (G (\|A\|) + 1 \dots N)) \to G (\|A\|) + 1 \leq k$
59	50 52 55 56 58	ltletrd	$⊢ (φ \land k \in (G (\|A\|) + 1 \dots N)) \to G (\|A\|) < k$
60	13	adantr	$⊢ (φ \land (k \in (G (\|A\|) + 1 \dots N) \land k \in A)) \to G : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A$
61		f1ocnv	$⊢ G : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to G^{-1} : A \underset{1-1 onto}{⟶} (1 \dots \|A\|)$
62	60 61	syl	$⊢ (φ \land (k \in (G (\|A\|) + 1 \dots N) \land k \in A)) \to G^{-1} : A \underset{1-1 onto}{⟶} (1 \dots \|A\|)$
63		f1of	$⊢ G^{-1} : A \underset{1-1 onto}{⟶} (1 \dots \|A\|) \to G^{-1} : A ⟶ (1 \dots \|A\|)$
64	62 63	syl	$⊢ (φ \land (k \in (G (\|A\|) + 1 \dots N) \land k \in A)) \to G^{-1} : A ⟶ (1 \dots \|A\|)$
65		simprr	$⊢ (φ \land (k \in (G (\|A\|) + 1 \dots N) \land k \in A)) \to k \in A$
66	64 65	ffvelcdmd	$⊢ (φ \land (k \in (G (\|A\|) + 1 \dots N) \land k \in A)) \to G^{-1} (k) \in (1 \dots \|A\|)$
67	66	elfzelzd	$⊢ (φ \land (k \in (G (\|A\|) + 1 \dots N) \land k \in A)) \to G^{-1} (k) \in ℤ$
68	67	zred	$⊢ (φ \land (k \in (G (\|A\|) + 1 \dots N) \land k \in A)) \to G^{-1} (k) \in ℝ$
69	24	adantr	$⊢ (φ \land (k \in (G (\|A\|) + 1 \dots N) \land k \in A)) \to \|A\| \in ℕ_{0}$
70	69	nn0red	$⊢ (φ \land (k \in (G (\|A\|) + 1 \dots N) \land k \in A)) \to \|A\| \in ℝ$
71		elfzle2	$⊢ G^{-1} (k) \in (1 \dots \|A\|) \to G^{-1} (k) \leq \|A\|$
72	66 71	syl	$⊢ (φ \land (k \in (G (\|A\|) + 1 \dots N) \land k \in A)) \to G^{-1} (k) \leq \|A\|$
73	68 70 72	lensymd	$⊢ (φ \land (k \in (G (\|A\|) + 1 \dots N) \land k \in A)) \to \neg \|A\| < G^{-1} (k)$
74	5	adantr	$⊢ (φ \land (k \in (G (\|A\|) + 1 \dots N) \land k \in A)) \to G {Isom}_{<, <} ((1 \dots \|A\|), A)$
75	32	adantr	$⊢ (φ \land (k \in (G (\|A\|) + 1 \dots N) \land k \in A)) \to \|A\| \in (1 \dots \|A\|)$
76		isorel	$⊢ (G {Isom}_{<, <} ((1 \dots \|A\|), A) \land (\|A\| \in (1 \dots \|A\|) \land G^{-1} (k) \in (1 \dots \|A\|))) \to (\|A\| < G^{-1} (k) \leftrightarrow G (\|A\|) < G (G^{-1} (k)))$
77	74 75 66 76	syl12anc	$⊢ (φ \land (k \in (G (\|A\|) + 1 \dots N) \land k \in A)) \to (\|A\| < G^{-1} (k) \leftrightarrow G (\|A\|) < G (G^{-1} (k)))$
78		f1ocnvfv2	$⊢ (G : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \land k \in A) \to G (G^{-1} (k)) = k$
79	60 65 78	syl2anc	$⊢ (φ \land (k \in (G (\|A\|) + 1 \dots N) \land k \in A)) \to G (G^{-1} (k)) = k$
80	79	breq2d	$⊢ (φ \land (k \in (G (\|A\|) + 1 \dots N) \land k \in A)) \to (G (\|A\|) < G (G^{-1} (k)) \leftrightarrow G (\|A\|) < k)$
81	77 80	bitrd	$⊢ (φ \land (k \in (G (\|A\|) + 1 \dots N) \land k \in A)) \to (\|A\| < G^{-1} (k) \leftrightarrow G (\|A\|) < k)$
82	73 81	mtbid	$⊢ (φ \land (k \in (G (\|A\|) + 1 \dots N) \land k \in A)) \to \neg G (\|A\|) < k$
83	82	expr	$⊢ (φ \land k \in (G (\|A\|) + 1 \dots N)) \to (k \in A \to \neg G (\|A\|) < k)$
84	59 83	mt2d	$⊢ (φ \land k \in (G (\|A\|) + 1 \dots N)) \to \neg k \in A$
85	47 84	eldifd	$⊢ (φ \land k \in (G (\|A\|) + 1 \dots N)) \to k \in ((M \dots N) ∖ A)$
86	85 9	syldan	$⊢ (φ \land k \in (G (\|A\|) + 1 \dots N)) \to F (k) = Z$
87	2 35 37 42 86	seqid2	$⊢ φ \to seq M (\underset{˙}{+}, F) (G (\|A\|)) = seq M (\underset{˙}{+}, F) (N)$
88	7 11	sstrdi	$⊢ φ \to A \subseteq ℤ_{\geq M}$
89	39	ssdifd	$⊢ φ \to (M \dots G (\|A\|)) ∖ A \subseteq (M \dots N) ∖ A$
90	89	sselda	$⊢ (φ \land k \in ((M \dots G (\|A\|)) ∖ A)) \to k \in ((M \dots N) ∖ A)$
91	90 9	syldan	$⊢ (φ \land k \in ((M \dots G (\|A\|)) ∖ A)) \to F (k) = Z$
92	1 2 3 4 5 32 88 41 91 10	seqcoll	$⊢ φ \to seq M (\underset{˙}{+}, F) (G (\|A\|)) = seq 1 (\underset{˙}{+}, H) (\|A\|)$
93	87 92	eqtr3d	$⊢ φ \to seq M (\underset{˙}{+}, F) (N) = seq 1 (\underset{˙}{+}, H) (\|A\|)$

Metamath Proof Explorer

Theorem seqcoll2

Proof