ulmshftlem

	Ref	Expression
Hypotheses	ulmshft.z	$⊢ Z = ℤ_{\geq M}$
	ulmshft.w	$⊢ W = ℤ_{\geq (M + K)}$
	ulmshft.m	$⊢ φ \to M \in ℤ$
	ulmshft.k	$⊢ φ \to K \in ℤ$
	ulmshft.f	$⊢ φ \to F : Z ⟶ ℂ^{S}$
	ulmshft.h	$⊢ φ \to H = (n \in W ⟼ F (n - K))$
Assertion	ulmshftlem	$⊢ φ \to (F \underset{u}{⇝} (S) G \to H \underset{u}{⇝} (S) G)$

Proof

Step	Hyp	Ref	Expression
1		ulmshft.z	$⊢ Z = ℤ_{\geq M}$
2		ulmshft.w	$⊢ W = ℤ_{\geq (M + K)}$
3		ulmshft.m	$⊢ φ \to M \in ℤ$
4		ulmshft.k	$⊢ φ \to K \in ℤ$
5		ulmshft.f	$⊢ φ \to F : Z ⟶ ℂ^{S}$
6		ulmshft.h	$⊢ φ \to H = (n \in W ⟼ F (n - K))$
7	3	ad2antrr	$⊢ ((φ \land F \underset{u}{⇝} (S) G) \land x \in ℝ^{+}) \to M \in ℤ$
8	5	ad2antrr	$⊢ ((φ \land F \underset{u}{⇝} (S) G) \land x \in ℝ^{+}) \to F : Z ⟶ ℂ^{S}$
9		eqidd	$⊢ (((φ \land F \underset{u}{⇝} (S) G) \land x \in ℝ^{+}) \land (m \in Z \land z \in S)) \to F (m) (z) = F (m) (z)$
10		eqidd	$⊢ (((φ \land F \underset{u}{⇝} (S) G) \land x \in ℝ^{+}) \land z \in S) \to G (z) = G (z)$
11		simplr	$⊢ ((φ \land F \underset{u}{⇝} (S) G) \land x \in ℝ^{+}) \to F \underset{u}{⇝} (S) G$
12		simpr	$⊢ ((φ \land F \underset{u}{⇝} (S) G) \land x \in ℝ^{+}) \to x \in ℝ^{+}$
13	1 7 8 9 10 11 12	ulmi	$⊢ ((φ \land F \underset{u}{⇝} (S) G) \land x \in ℝ^{+}) \to \exists i \in Z \forall m \in ℤ_{\geq i} \forall z \in S \|F (m) (z) - G (z)\| < x$
14		simpr	$⊢ (((φ \land F \underset{u}{⇝} (S) G) \land x \in ℝ^{+}) \land i \in Z) \to i \in Z$
15	14 1	eleqtrdi	$⊢ (((φ \land F \underset{u}{⇝} (S) G) \land x \in ℝ^{+}) \land i \in Z) \to i \in ℤ_{\geq M}$
16	4	ad3antrrr	$⊢ (((φ \land F \underset{u}{⇝} (S) G) \land x \in ℝ^{+}) \land i \in Z) \to K \in ℤ$
17		eluzadd	$⊢ (i \in ℤ_{\geq M} \land K \in ℤ) \to i + K \in ℤ_{\geq (M + K)}$
18	15 16 17	syl2anc	$⊢ (((φ \land F \underset{u}{⇝} (S) G) \land x \in ℝ^{+}) \land i \in Z) \to i + K \in ℤ_{\geq (M + K)}$
19	18 2	eleqtrrdi	$⊢ (((φ \land F \underset{u}{⇝} (S) G) \land x \in ℝ^{+}) \land i \in Z) \to i + K \in W$
20		eluzelz	$⊢ i \in ℤ_{\geq M} \to i \in ℤ$
21	15 20	syl	$⊢ (((φ \land F \underset{u}{⇝} (S) G) \land x \in ℝ^{+}) \land i \in Z) \to i \in ℤ$
22	21	adantr	$⊢ ((((φ \land F \underset{u}{⇝} (S) G) \land x \in ℝ^{+}) \land i \in Z) \land k \in ℤ_{\geq (i + K)}) \to i \in ℤ$
23	4	adantr	$⊢ (φ \land F \underset{u}{⇝} (S) G) \to K \in ℤ$
24	23	ad3antrrr	$⊢ ((((φ \land F \underset{u}{⇝} (S) G) \land x \in ℝ^{+}) \land i \in Z) \land k \in ℤ_{\geq (i + K)}) \to K \in ℤ$
25		simpr	$⊢ ((((φ \land F \underset{u}{⇝} (S) G) \land x \in ℝ^{+}) \land i \in Z) \land k \in ℤ_{\geq (i + K)}) \to k \in ℤ_{\geq (i + K)}$
26		eluzsub	$⊢ (i \in ℤ \land K \in ℤ \land k \in ℤ_{\geq (i + K)}) \to k - K \in ℤ_{\geq i}$
27	22 24 25 26	syl3anc	$⊢ ((((φ \land F \underset{u}{⇝} (S) G) \land x \in ℝ^{+}) \land i \in Z) \land k \in ℤ_{\geq (i + K)}) \to k - K \in ℤ_{\geq i}$
28		fveq2	$⊢ m = k - K \to F (m) = F (k - K)$
29	28	fveq1d	$⊢ m = k - K \to F (m) (z) = F (k - K) (z)$
30	29	fvoveq1d	$⊢ m = k - K \to \|F (m) (z) - G (z)\| = \|F (k - K) (z) - G (z)\|$
31	30	breq1d	$⊢ m = k - K \to (\|F (m) (z) - G (z)\| < x \leftrightarrow \|F (k - K) (z) - G (z)\| < x)$
32	31	ralbidv	$⊢ m = k - K \to (\forall z \in S \|F (m) (z) - G (z)\| < x \leftrightarrow \forall z \in S \|F (k - K) (z) - G (z)\| < x)$
33	32	rspcv	$⊢ k - K \in ℤ_{\geq i} \to (\forall m \in ℤ_{\geq i} \forall z \in S \|F (m) (z) - G (z)\| < x \to \forall z \in S \|F (k - K) (z) - G (z)\| < x)$
34	27 33	syl	$⊢ ((((φ \land F \underset{u}{⇝} (S) G) \land x \in ℝ^{+}) \land i \in Z) \land k \in ℤ_{\geq (i + K)}) \to (\forall m \in ℤ_{\geq i} \forall z \in S \|F (m) (z) - G (z)\| < x \to \forall z \in S \|F (k - K) (z) - G (z)\| < x)$
35	34	ralrimdva	$⊢ (((φ \land F \underset{u}{⇝} (S) G) \land x \in ℝ^{+}) \land i \in Z) \to (\forall m \in ℤ_{\geq i} \forall z \in S \|F (m) (z) - G (z)\| < x \to \forall k \in ℤ_{\geq (i + K)} \forall z \in S \|F (k - K) (z) - G (z)\| < x)$
36		fveq2	$⊢ j = i + K \to ℤ_{\geq j} = ℤ_{\geq (i + K)}$
37	36	raleqdv	$⊢ j = i + K \to (\forall k \in ℤ_{\geq j} \forall z \in S \|F (k - K) (z) - G (z)\| < x \leftrightarrow \forall k \in ℤ_{\geq (i + K)} \forall z \in S \|F (k - K) (z) - G (z)\| < x)$
38	37	rspcev	$⊢ (i + K \in W \land \forall k \in ℤ_{\geq (i + K)} \forall z \in S \|F (k - K) (z) - G (z)\| < x) \to \exists j \in W \forall k \in ℤ_{\geq j} \forall z \in S \|F (k - K) (z) - G (z)\| < x$
39	19 35 38	syl6an	$⊢ (((φ \land F \underset{u}{⇝} (S) G) \land x \in ℝ^{+}) \land i \in Z) \to (\forall m \in ℤ_{\geq i} \forall z \in S \|F (m) (z) - G (z)\| < x \to \exists j \in W \forall k \in ℤ_{\geq j} \forall z \in S \|F (k - K) (z) - G (z)\| < x)$
40	39	rexlimdva	$⊢ ((φ \land F \underset{u}{⇝} (S) G) \land x \in ℝ^{+}) \to (\exists i \in Z \forall m \in ℤ_{\geq i} \forall z \in S \|F (m) (z) - G (z)\| < x \to \exists j \in W \forall k \in ℤ_{\geq j} \forall z \in S \|F (k - K) (z) - G (z)\| < x)$
41	13 40	mpd	$⊢ ((φ \land F \underset{u}{⇝} (S) G) \land x \in ℝ^{+}) \to \exists j \in W \forall k \in ℤ_{\geq j} \forall z \in S \|F (k - K) (z) - G (z)\| < x$
42	41	ralrimiva	$⊢ (φ \land F \underset{u}{⇝} (S) G) \to \forall x \in ℝ^{+} \exists j \in W \forall k \in ℤ_{\geq j} \forall z \in S \|F (k - K) (z) - G (z)\| < x$
43	3 4	zaddcld	$⊢ φ \to M + K \in ℤ$
44	43	adantr	$⊢ (φ \land F \underset{u}{⇝} (S) G) \to M + K \in ℤ$
45	5	adantr	$⊢ (φ \land n \in W) \to F : Z ⟶ ℂ^{S}$
46	3	adantr	$⊢ (φ \land n \in W) \to M \in ℤ$
47	4	adantr	$⊢ (φ \land n \in W) \to K \in ℤ$
48		simpr	$⊢ (φ \land n \in W) \to n \in W$
49	48 2	eleqtrdi	$⊢ (φ \land n \in W) \to n \in ℤ_{\geq (M + K)}$
50		eluzsub	$⊢ (M \in ℤ \land K \in ℤ \land n \in ℤ_{\geq (M + K)}) \to n - K \in ℤ_{\geq M}$
51	46 47 49 50	syl3anc	$⊢ (φ \land n \in W) \to n - K \in ℤ_{\geq M}$
52	51 1	eleqtrrdi	$⊢ (φ \land n \in W) \to n - K \in Z$
53	45 52	ffvelrnd	$⊢ (φ \land n \in W) \to F (n - K) \in (ℂ^{S})$
54	6 53	fmpt3d	$⊢ φ \to H : W ⟶ ℂ^{S}$
55	54	adantr	$⊢ (φ \land F \underset{u}{⇝} (S) G) \to H : W ⟶ ℂ^{S}$
56	6	ad2antrr	$⊢ ((φ \land F \underset{u}{⇝} (S) G) \land (k \in W \land z \in S)) \to H = (n \in W ⟼ F (n - K))$
57	56	fveq1d	$⊢ ((φ \land F \underset{u}{⇝} (S) G) \land (k \in W \land z \in S)) \to H (k) = (n \in W ⟼ F (n - K)) (k)$
58		fvoveq1	$⊢ n = k \to F (n - K) = F (k - K)$
59		eqid	$⊢ (n \in W ⟼ F (n - K)) = (n \in W ⟼ F (n - K))$
60		fvex	$⊢ F (k - K) \in V$
61	58 59 60	fvmpt	$⊢ k \in W \to (n \in W ⟼ F (n - K)) (k) = F (k - K)$
62	61	ad2antrl	$⊢ ((φ \land F \underset{u}{⇝} (S) G) \land (k \in W \land z \in S)) \to (n \in W ⟼ F (n - K)) (k) = F (k - K)$
63	57 62	eqtrd	$⊢ ((φ \land F \underset{u}{⇝} (S) G) \land (k \in W \land z \in S)) \to H (k) = F (k - K)$
64	63	fveq1d	$⊢ ((φ \land F \underset{u}{⇝} (S) G) \land (k \in W \land z \in S)) \to H (k) (z) = F (k - K) (z)$
65		eqidd	$⊢ ((φ \land F \underset{u}{⇝} (S) G) \land z \in S) \to G (z) = G (z)$
66		ulmcl	$⊢ F \underset{u}{⇝} (S) G \to G : S ⟶ ℂ$
67	66	adantl	$⊢ (φ \land F \underset{u}{⇝} (S) G) \to G : S ⟶ ℂ$
68		ulmscl	$⊢ F \underset{u}{⇝} (S) G \to S \in V$
69	68	adantl	$⊢ (φ \land F \underset{u}{⇝} (S) G) \to S \in V$
70	2 44 55 64 65 67 69	ulm2	$⊢ (φ \land F \underset{u}{⇝} (S) G) \to (H \underset{u}{⇝} (S) G \leftrightarrow \forall x \in ℝ^{+} \exists j \in W \forall k \in ℤ_{\geq j} \forall z \in S \|F (k - K) (z) - G (z)\| < x)$
71	42 70	mpbird	$⊢ (φ \land F \underset{u}{⇝} (S) G) \to H \underset{u}{⇝} (S) G$
72	71	ex	$⊢ φ \to (F \underset{u}{⇝} (S) G \to H \underset{u}{⇝} (S) G)$

Metamath Proof Explorer

Theorem ulmshftlem

Proof