ulm2

Description: Simplify ulmval when F and G are known to be functions. (Contributed by Mario Carneiro, 26-Feb-2015)

	Ref	Expression
Hypotheses	ulm2.z	$⊢ Z = ℤ_{\geq M}$
	ulm2.m	$⊢ φ \to M \in ℤ$
	ulm2.f	$⊢ φ \to F : Z ⟶ ℂ^{S}$
	ulm2.b	$⊢ (φ \land (k \in Z \land z \in S)) \to F (k) (z) = B$
	ulm2.a	$⊢ (φ \land z \in S) \to G (z) = A$
	ulm2.g	$⊢ φ \to G : S ⟶ ℂ$
	ulm2.s	$⊢ φ \to S \in V$
Assertion	ulm2	$⊢ φ \to (F \underset{u}{⇝} (S) G \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|B - A\| < x)$

Proof

Step	Hyp	Ref	Expression
1		ulm2.z	$⊢ Z = ℤ_{\geq M}$
2		ulm2.m	$⊢ φ \to M \in ℤ$
3		ulm2.f	$⊢ φ \to F : Z ⟶ ℂ^{S}$
4		ulm2.b	$⊢ (φ \land (k \in Z \land z \in S)) \to F (k) (z) = B$
5		ulm2.a	$⊢ (φ \land z \in S) \to G (z) = A$
6		ulm2.g	$⊢ φ \to G : S ⟶ ℂ$
7		ulm2.s	$⊢ φ \to S \in V$
8		ulmval	$⊢ S \in V \to (F \underset{u}{⇝} (S) G \leftrightarrow \exists n \in ℤ (F : ℤ_{\geq n} ⟶ ℂ^{S} \land G : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < x))$
9	7 8	syl	$⊢ φ \to (F \underset{u}{⇝} (S) G \leftrightarrow \exists n \in ℤ (F : ℤ_{\geq n} ⟶ ℂ^{S} \land G : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < x))$
10		3anan12	$⊢ (F : ℤ_{\geq n} ⟶ ℂ^{S} \land G : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < x) \leftrightarrow (G : S ⟶ ℂ \land (F : ℤ_{\geq n} ⟶ ℂ^{S} \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < x))$
11	3	fdmd	$⊢ φ \to dom F = Z$
12		fdm	$⊢ F : ℤ_{\geq n} ⟶ ℂ^{S} \to dom F = ℤ_{\geq n}$
13	11 12	sylan9req	$⊢ (φ \land F : ℤ_{\geq n} ⟶ ℂ^{S}) \to Z = ℤ_{\geq n}$
14	1 13	eqtr3id	$⊢ (φ \land F : ℤ_{\geq n} ⟶ ℂ^{S}) \to ℤ_{\geq M} = ℤ_{\geq n}$
15	2	adantr	$⊢ (φ \land F : ℤ_{\geq n} ⟶ ℂ^{S}) \to M \in ℤ$
16		uz11	$⊢ M \in ℤ \to (ℤ_{\geq M} = ℤ_{\geq n} \leftrightarrow M = n)$
17	15 16	syl	$⊢ (φ \land F : ℤ_{\geq n} ⟶ ℂ^{S}) \to (ℤ_{\geq M} = ℤ_{\geq n} \leftrightarrow M = n)$
18	14 17	mpbid	$⊢ (φ \land F : ℤ_{\geq n} ⟶ ℂ^{S}) \to M = n$
19	18	eqcomd	$⊢ (φ \land F : ℤ_{\geq n} ⟶ ℂ^{S}) \to n = M$
20		fveq2	$⊢ n = M \to ℤ_{\geq n} = ℤ_{\geq M}$
21	20 1	eqtr4di	$⊢ n = M \to ℤ_{\geq n} = Z$
22	21	feq2d	$⊢ n = M \to (F : ℤ_{\geq n} ⟶ ℂ^{S} \leftrightarrow F : Z ⟶ ℂ^{S})$
23	22	biimparc	$⊢ (F : Z ⟶ ℂ^{S} \land n = M) \to F : ℤ_{\geq n} ⟶ ℂ^{S}$
24	3 23	sylan	$⊢ (φ \land n = M) \to F : ℤ_{\geq n} ⟶ ℂ^{S}$
25	19 24	impbida	$⊢ φ \to (F : ℤ_{\geq n} ⟶ ℂ^{S} \leftrightarrow n = M)$
26	25	anbi1d	$⊢ φ \to ((F : ℤ_{\geq n} ⟶ ℂ^{S} \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < x) \leftrightarrow (n = M \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < x))$
27	6	biantrurd	$⊢ φ \to ((F : ℤ_{\geq n} ⟶ ℂ^{S} \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < x) \leftrightarrow (G : S ⟶ ℂ \land (F : ℤ_{\geq n} ⟶ ℂ^{S} \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < x)))$
28		simp-4l	$⊢ ((((φ \land n = M) \land j \in ℤ_{\geq n}) \land k \in ℤ_{\geq j}) \land z \in S) \to φ$
29		simpr	$⊢ (φ \land n = M) \to n = M$
30		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
31	2 30	syl	$⊢ φ \to M \in ℤ_{\geq M}$
32	31 1	eleqtrrdi	$⊢ φ \to M \in Z$
33	32	adantr	$⊢ (φ \land n = M) \to M \in Z$
34	29 33	eqeltrd	$⊢ (φ \land n = M) \to n \in Z$
35	1	uztrn2	$⊢ (n \in Z \land j \in ℤ_{\geq n}) \to j \in Z$
36	34 35	sylan	$⊢ ((φ \land n = M) \land j \in ℤ_{\geq n}) \to j \in Z$
37	1	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
38	36 37	sylan	$⊢ (((φ \land n = M) \land j \in ℤ_{\geq n}) \land k \in ℤ_{\geq j}) \to k \in Z$
39	38	adantr	$⊢ ((((φ \land n = M) \land j \in ℤ_{\geq n}) \land k \in ℤ_{\geq j}) \land z \in S) \to k \in Z$
40		simpr	$⊢ ((((φ \land n = M) \land j \in ℤ_{\geq n}) \land k \in ℤ_{\geq j}) \land z \in S) \to z \in S$
41	28 39 40 4	syl12anc	$⊢ ((((φ \land n = M) \land j \in ℤ_{\geq n}) \land k \in ℤ_{\geq j}) \land z \in S) \to F (k) (z) = B$
42	28 5	sylancom	$⊢ ((((φ \land n = M) \land j \in ℤ_{\geq n}) \land k \in ℤ_{\geq j}) \land z \in S) \to G (z) = A$
43	41 42	oveq12d	$⊢ ((((φ \land n = M) \land j \in ℤ_{\geq n}) \land k \in ℤ_{\geq j}) \land z \in S) \to F (k) (z) - G (z) = B - A$
44	43	fveq2d	$⊢ ((((φ \land n = M) \land j \in ℤ_{\geq n}) \land k \in ℤ_{\geq j}) \land z \in S) \to \|F (k) (z) - G (z)\| = \|B - A\|$
45	44	breq1d	$⊢ ((((φ \land n = M) \land j \in ℤ_{\geq n}) \land k \in ℤ_{\geq j}) \land z \in S) \to (\|F (k) (z) - G (z)\| < x \leftrightarrow \|B - A\| < x)$
46	45	ralbidva	$⊢ (((φ \land n = M) \land j \in ℤ_{\geq n}) \land k \in ℤ_{\geq j}) \to (\forall z \in S \|F (k) (z) - G (z)\| < x \leftrightarrow \forall z \in S \|B - A\| < x)$
47	46	ralbidva	$⊢ ((φ \land n = M) \land j \in ℤ_{\geq n}) \to (\forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < x \leftrightarrow \forall k \in ℤ_{\geq j} \forall z \in S \|B - A\| < x)$
48	47	rexbidva	$⊢ (φ \land n = M) \to (\exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < x \leftrightarrow \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|B - A\| < x)$
49	48	ralbidv	$⊢ (φ \land n = M) \to (\forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < x \leftrightarrow \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|B - A\| < x)$
50	49	pm5.32da	$⊢ φ \to ((n = M \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < x) \leftrightarrow (n = M \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|B - A\| < x))$
51	26 27 50	3bitr3d	$⊢ φ \to ((G : S ⟶ ℂ \land (F : ℤ_{\geq n} ⟶ ℂ^{S} \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < x)) \leftrightarrow (n = M \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|B - A\| < x))$
52	10 51	bitrid	$⊢ φ \to ((F : ℤ_{\geq n} ⟶ ℂ^{S} \land G : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < x) \leftrightarrow (n = M \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|B - A\| < x))$
53	52	rexbidv	$⊢ φ \to (\exists n \in ℤ (F : ℤ_{\geq n} ⟶ ℂ^{S} \land G : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < x) \leftrightarrow \exists n \in ℤ (n = M \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|B - A\| < x))$
54	21	rexeqdv	$⊢ n = M \to (\exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|B - A\| < x \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|B - A\| < x)$
55	54	ralbidv	$⊢ n = M \to (\forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|B - A\| < x \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|B - A\| < x)$
56	55	ceqsrexv	$⊢ M \in ℤ \to (\exists n \in ℤ (n = M \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|B - A\| < x) \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|B - A\| < x)$
57	2 56	syl	$⊢ φ \to (\exists n \in ℤ (n = M \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|B - A\| < x) \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|B - A\| < x)$
58	9 53 57	3bitrd	$⊢ φ \to (F \underset{u}{⇝} (S) G \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|B - A\| < x)$

Metamath Proof Explorer

Theorem ulm2

Proof