isercolllem3

	Ref	Expression
Hypotheses	isercoll.z	$⊢ Z = ℤ_{\geq M}$
	isercoll.m	$⊢ φ \to M \in ℤ$
	isercoll.g	$⊢ φ \to G : ℕ ⟶ Z$
	isercoll.i	$⊢ (φ \land k \in ℕ) \to G (k) < G (k + 1)$
	isercoll.0	$⊢ (φ \land n \in (Z ∖ ran G)) \to F (n) = 0$
	isercoll.f	$⊢ (φ \land n \in Z) \to F (n) \in ℂ$
	isercoll.h	$⊢ (φ \land k \in ℕ) \to H (k) = F (G (k))$
Assertion	isercolllem3	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to seq M (+ F) (N) = seq 1 (+ H) (\|G [G^{-1} [(M \dots N)]]\|)$

Proof

Step	Hyp	Ref	Expression
1		isercoll.z	$⊢ Z = ℤ_{\geq M}$
2		isercoll.m	$⊢ φ \to M \in ℤ$
3		isercoll.g	$⊢ φ \to G : ℕ ⟶ Z$
4		isercoll.i	$⊢ (φ \land k \in ℕ) \to G (k) < G (k + 1)$
5		isercoll.0	$⊢ (φ \land n \in (Z ∖ ran G)) \to F (n) = 0$
6		isercoll.f	$⊢ (φ \land n \in Z) \to F (n) \in ℂ$
7		isercoll.h	$⊢ (φ \land k \in ℕ) \to H (k) = F (G (k))$
8		addlid	$⊢ n \in ℂ \to 0 + n = n$
9	8	adantl	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land n \in ℂ) \to 0 + n = n$
10		addrid	$⊢ n \in ℂ \to n + 0 = n$
11	10	adantl	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land n \in ℂ) \to n + 0 = n$
12		addcl	$⊢ (n \in ℂ \land k \in ℂ) \to n + k \in ℂ$
13	12	adantl	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land (n \in ℂ \land k \in ℂ)) \to n + k \in ℂ$
14		0cnd	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to 0 \in ℂ$
15		cnvimass	$⊢ G^{-1} [(M \dots N)] \subseteq dom G$
16	3	adantr	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to G : ℕ ⟶ Z$
17	15 16	fssdm	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to G^{-1} [(M \dots N)] \subseteq ℕ$
18	1 2 3 4	isercolllem1	$⊢ (φ \land G^{-1} [(M \dots N)] \subseteq ℕ) \to ({G ↾}_{G^{-1} [(M \dots N)]}) {Isom}_{<, <} (G^{-1} [(M \dots N)], G [G^{-1} [(M \dots N)]])$
19	17 18	syldan	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to ({G ↾}_{G^{-1} [(M \dots N)]}) {Isom}_{<, <} (G^{-1} [(M \dots N)], G [G^{-1} [(M \dots N)]])$
20	1 2 3 4	isercolllem2	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to (1 \dots \|G [G^{-1} [(M \dots N)]]\|) = G^{-1} [(M \dots N)]$
21		isoeq4	$⊢ (1 \dots \|G [G^{-1} [(M \dots N)]]\|) = G^{-1} [(M \dots N)] \to (({G ↾}_{G^{-1} [(M \dots N)]}) {Isom}_{<, <} ((1 \dots \|G [G^{-1} [(M \dots N)]]\|), G [G^{-1} [(M \dots N)]]) \leftrightarrow ({G ↾}_{G^{-1} [(M \dots N)]}) {Isom}_{<, <} (G^{-1} [(M \dots N)], G [G^{-1} [(M \dots N)]]))$
22	20 21	syl	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to (({G ↾}_{G^{-1} [(M \dots N)]}) {Isom}_{<, <} ((1 \dots \|G [G^{-1} [(M \dots N)]]\|), G [G^{-1} [(M \dots N)]]) \leftrightarrow ({G ↾}_{G^{-1} [(M \dots N)]}) {Isom}_{<, <} (G^{-1} [(M \dots N)], G [G^{-1} [(M \dots N)]]))$
23	19 22	mpbird	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to ({G ↾}_{G^{-1} [(M \dots N)]}) {Isom}_{<, <} ((1 \dots \|G [G^{-1} [(M \dots N)]]\|), G [G^{-1} [(M \dots N)]])$
24	15	a1i	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to G^{-1} [(M \dots N)] \subseteq dom G$
25		sseqin2	$⊢ G^{-1} [(M \dots N)] \subseteq dom G \leftrightarrow dom G \cap G^{-1} [(M \dots N)] = G^{-1} [(M \dots N)]$
26	24 25	sylib	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to dom G \cap G^{-1} [(M \dots N)] = G^{-1} [(M \dots N)]$
27		1nn	$⊢ 1 \in ℕ$
28	27	a1i	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to 1 \in ℕ$
29		ffvelcdm	$⊢ (G : ℕ ⟶ Z \land 1 \in ℕ) \to G (1) \in Z$
30	3 27 29	sylancl	$⊢ φ \to G (1) \in Z$
31	30 1	eleqtrdi	$⊢ φ \to G (1) \in ℤ_{\geq M}$
32	31	adantr	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to G (1) \in ℤ_{\geq M}$
33		simpr	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to N \in ℤ_{\geq G (1)}$
34		elfzuzb	$⊢ G (1) \in (M \dots N) \leftrightarrow (G (1) \in ℤ_{\geq M} \land N \in ℤ_{\geq G (1)})$
35	32 33 34	sylanbrc	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to G (1) \in (M \dots N)$
36		ffn	$⊢ G : ℕ ⟶ Z \to G Fn ℕ$
37		elpreima	$⊢ G Fn ℕ \to (1 \in G^{-1} [(M \dots N)] \leftrightarrow (1 \in ℕ \land G (1) \in (M \dots N)))$
38	16 36 37	3syl	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to (1 \in G^{-1} [(M \dots N)] \leftrightarrow (1 \in ℕ \land G (1) \in (M \dots N)))$
39	28 35 38	mpbir2and	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to 1 \in G^{-1} [(M \dots N)]$
40	39	ne0d	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to G^{-1} [(M \dots N)] \neq \emptyset$
41	26 40	eqnetrd	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to dom G \cap G^{-1} [(M \dots N)] \neq \emptyset$
42		imadisj	$⊢ G [G^{-1} [(M \dots N)]] = \emptyset \leftrightarrow dom G \cap G^{-1} [(M \dots N)] = \emptyset$
43	42	necon3bii	$⊢ G [G^{-1} [(M \dots N)]] \neq \emptyset \leftrightarrow dom G \cap G^{-1} [(M \dots N)] \neq \emptyset$
44	41 43	sylibr	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to G [G^{-1} [(M \dots N)]] \neq \emptyset$
45		ffun	$⊢ G : ℕ ⟶ Z \to Fun G$
46		funimacnv	$⊢ Fun G \to G [G^{-1} [(M \dots N)]] = (M \dots N) \cap ran G$
47	16 45 46	3syl	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to G [G^{-1} [(M \dots N)]] = (M \dots N) \cap ran G$
48		inss1	$⊢ (M \dots N) \cap ran G \subseteq (M \dots N)$
49	47 48	eqsstrdi	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to G [G^{-1} [(M \dots N)]] \subseteq (M \dots N)$
50		simpl	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to φ$
51		elfzuz	$⊢ n \in (M \dots N) \to n \in ℤ_{\geq M}$
52	51 1	eleqtrrdi	$⊢ n \in (M \dots N) \to n \in Z$
53	50 52 6	syl2an	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land n \in (M \dots N)) \to F (n) \in ℂ$
54	47	difeq2d	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to (M \dots N) ∖ G [G^{-1} [(M \dots N)]] = (M \dots N) ∖ ((M \dots N) \cap ran G)$
55		difin	$⊢ (M \dots N) ∖ ((M \dots N) \cap ran G) = (M \dots N) ∖ ran G$
56	54 55	eqtrdi	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to (M \dots N) ∖ G [G^{-1} [(M \dots N)]] = (M \dots N) ∖ ran G$
57	52	ssriv	$⊢ (M \dots N) \subseteq Z$
58		ssdif	$⊢ (M \dots N) \subseteq Z \to (M \dots N) ∖ ran G \subseteq Z ∖ ran G$
59	57 58	mp1i	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to (M \dots N) ∖ ran G \subseteq Z ∖ ran G$
60	56 59	eqsstrd	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to (M \dots N) ∖ G [G^{-1} [(M \dots N)]] \subseteq Z ∖ ran G$
61	60	sselda	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land n \in ((M \dots N) ∖ G [G^{-1} [(M \dots N)]])) \to n \in (Z ∖ ran G)$
62	5	adantlr	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land n \in (Z ∖ ran G)) \to F (n) = 0$
63	61 62	syldan	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land n \in ((M \dots N) ∖ G [G^{-1} [(M \dots N)]])) \to F (n) = 0$
64		elfznn	$⊢ k \in (1 \dots \|G [G^{-1} [(M \dots N)]]\|) \to k \in ℕ$
65	50 64 7	syl2an	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land k \in (1 \dots \|G [G^{-1} [(M \dots N)]]\|)) \to H (k) = F (G (k))$
66	20	eleq2d	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to (k \in (1 \dots \|G [G^{-1} [(M \dots N)]]\|) \leftrightarrow k \in G^{-1} [(M \dots N)])$
67	66	biimpa	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land k \in (1 \dots \|G [G^{-1} [(M \dots N)]]\|)) \to k \in G^{-1} [(M \dots N)]$
68	67	fvresd	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land k \in (1 \dots \|G [G^{-1} [(M \dots N)]]\|)) \to ({G ↾}_{G^{-1} [(M \dots N)]}) (k) = G (k)$
69	68	fveq2d	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land k \in (1 \dots \|G [G^{-1} [(M \dots N)]]\|)) \to F (({G ↾}_{G^{-1} [(M \dots N)]}) (k)) = F (G (k))$
70	65 69	eqtr4d	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land k \in (1 \dots \|G [G^{-1} [(M \dots N)]]\|)) \to H (k) = F (({G ↾}_{G^{-1} [(M \dots N)]}) (k))$
71	9 11 13 14 23 44 49 53 63 70	seqcoll2	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to seq M (+ F) (N) = seq 1 (+ H) (\|G [G^{-1} [(M \dots N)]]\|)$

Metamath Proof Explorer

Theorem isercolllem3

Proof