o1co

Description: Sufficient condition for transforming the index set of an eventually bounded function. (Contributed by Mario Carneiro, 12-May-2016)

	Ref	Expression
Hypotheses	o1co.1	$⊢ φ \to F : A ⟶ ℂ$
	o1co.2	$⊢ φ \to F \in 𝑂 (1)$
	o1co.3	$⊢ φ \to G : B ⟶ A$
	o1co.4	$⊢ φ \to B \subseteq ℝ$
	o1co.5	$⊢ (φ \land m \in ℝ) \to \exists x \in ℝ \forall y \in B (x \leq y \to m \leq G (y))$
Assertion	o1co	$⊢ φ \to F \circ G \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		o1co.1	$⊢ φ \to F : A ⟶ ℂ$
2		o1co.2	$⊢ φ \to F \in 𝑂 (1)$
3		o1co.3	$⊢ φ \to G : B ⟶ A$
4		o1co.4	$⊢ φ \to B \subseteq ℝ$
5		o1co.5	$⊢ (φ \land m \in ℝ) \to \exists x \in ℝ \forall y \in B (x \leq y \to m \leq G (y))$
6	1	fdmd	$⊢ φ \to dom F = A$
7		o1dm	$⊢ F \in 𝑂 (1) \to dom F \subseteq ℝ$
8	2 7	syl	$⊢ φ \to dom F \subseteq ℝ$
9	6 8	eqsstrrd	$⊢ φ \to A \subseteq ℝ$
10		elo12	$⊢ (F : A ⟶ ℂ \land A \subseteq ℝ) \to (F \in 𝑂 (1) \leftrightarrow \exists m \in ℝ \exists n \in ℝ \forall z \in A (m \leq z \to \|F (z)\| \leq n))$
11	1 9 10	syl2anc	$⊢ φ \to (F \in 𝑂 (1) \leftrightarrow \exists m \in ℝ \exists n \in ℝ \forall z \in A (m \leq z \to \|F (z)\| \leq n))$
12	2 11	mpbid	$⊢ φ \to \exists m \in ℝ \exists n \in ℝ \forall z \in A (m \leq z \to \|F (z)\| \leq n)$
13		reeanv	$⊢ \exists x \in ℝ \exists n \in ℝ (\forall y \in B (x \leq y \to m \leq G (y)) \land \forall z \in A (m \leq z \to \|F (z)\| \leq n)) \leftrightarrow (\exists x \in ℝ \forall y \in B (x \leq y \to m \leq G (y)) \land \exists n \in ℝ \forall z \in A (m \leq z \to \|F (z)\| \leq n))$
14	3	ad3antrrr	$⊢ (((φ \land m \in ℝ) \land x \in ℝ) \land n \in ℝ) \to G : B ⟶ A$
15	14	ffvelrnda	$⊢ ((((φ \land m \in ℝ) \land x \in ℝ) \land n \in ℝ) \land y \in B) \to G (y) \in A$
16		breq2	$⊢ z = G (y) \to (m \leq z \leftrightarrow m \leq G (y))$
17		2fveq3	$⊢ z = G (y) \to \|F (z)\| = \|F (G (y))\|$
18	17	breq1d	$⊢ z = G (y) \to (\|F (z)\| \leq n \leftrightarrow \|F (G (y))\| \leq n)$
19	16 18	imbi12d	$⊢ z = G (y) \to ((m \leq z \to \|F (z)\| \leq n) \leftrightarrow (m \leq G (y) \to \|F (G (y))\| \leq n))$
20	19	rspcva	$⊢ (G (y) \in A \land \forall z \in A (m \leq z \to \|F (z)\| \leq n)) \to (m \leq G (y) \to \|F (G (y))\| \leq n)$
21	15 20	sylan	$⊢ (((((φ \land m \in ℝ) \land x \in ℝ) \land n \in ℝ) \land y \in B) \land \forall z \in A (m \leq z \to \|F (z)\| \leq n)) \to (m \leq G (y) \to \|F (G (y))\| \leq n)$
22	21	an32s	$⊢ (((((φ \land m \in ℝ) \land x \in ℝ) \land n \in ℝ) \land \forall z \in A (m \leq z \to \|F (z)\| \leq n)) \land y \in B) \to (m \leq G (y) \to \|F (G (y))\| \leq n)$
23	14	adantr	$⊢ ((((φ \land m \in ℝ) \land x \in ℝ) \land n \in ℝ) \land \forall z \in A (m \leq z \to \|F (z)\| \leq n)) \to G : B ⟶ A$
24		fvco3	$⊢ (G : B ⟶ A \land y \in B) \to (F \circ G) (y) = F (G (y))$
25	23 24	sylan	$⊢ (((((φ \land m \in ℝ) \land x \in ℝ) \land n \in ℝ) \land \forall z \in A (m \leq z \to \|F (z)\| \leq n)) \land y \in B) \to (F \circ G) (y) = F (G (y))$
26	25	fveq2d	$⊢ (((((φ \land m \in ℝ) \land x \in ℝ) \land n \in ℝ) \land \forall z \in A (m \leq z \to \|F (z)\| \leq n)) \land y \in B) \to \|(F \circ G) (y)\| = \|F (G (y))\|$
27	26	breq1d	$⊢ (((((φ \land m \in ℝ) \land x \in ℝ) \land n \in ℝ) \land \forall z \in A (m \leq z \to \|F (z)\| \leq n)) \land y \in B) \to (\|(F \circ G) (y)\| \leq n \leftrightarrow \|F (G (y))\| \leq n)$
28	22 27	sylibrd	$⊢ (((((φ \land m \in ℝ) \land x \in ℝ) \land n \in ℝ) \land \forall z \in A (m \leq z \to \|F (z)\| \leq n)) \land y \in B) \to (m \leq G (y) \to \|(F \circ G) (y)\| \leq n)$
29	28	imim2d	$⊢ (((((φ \land m \in ℝ) \land x \in ℝ) \land n \in ℝ) \land \forall z \in A (m \leq z \to \|F (z)\| \leq n)) \land y \in B) \to ((x \leq y \to m \leq G (y)) \to (x \leq y \to \|(F \circ G) (y)\| \leq n))$
30	29	ralimdva	$⊢ ((((φ \land m \in ℝ) \land x \in ℝ) \land n \in ℝ) \land \forall z \in A (m \leq z \to \|F (z)\| \leq n)) \to (\forall y \in B (x \leq y \to m \leq G (y)) \to \forall y \in B (x \leq y \to \|(F \circ G) (y)\| \leq n))$
31	30	expimpd	$⊢ (((φ \land m \in ℝ) \land x \in ℝ) \land n \in ℝ) \to ((\forall z \in A (m \leq z \to \|F (z)\| \leq n) \land \forall y \in B (x \leq y \to m \leq G (y))) \to \forall y \in B (x \leq y \to \|(F \circ G) (y)\| \leq n))$
32	31	ancomsd	$⊢ (((φ \land m \in ℝ) \land x \in ℝ) \land n \in ℝ) \to ((\forall y \in B (x \leq y \to m \leq G (y)) \land \forall z \in A (m \leq z \to \|F (z)\| \leq n)) \to \forall y \in B (x \leq y \to \|(F \circ G) (y)\| \leq n))$
33	32	reximdva	$⊢ ((φ \land m \in ℝ) \land x \in ℝ) \to (\exists n \in ℝ (\forall y \in B (x \leq y \to m \leq G (y)) \land \forall z \in A (m \leq z \to \|F (z)\| \leq n)) \to \exists n \in ℝ \forall y \in B (x \leq y \to \|(F \circ G) (y)\| \leq n))$
34	33	reximdva	$⊢ (φ \land m \in ℝ) \to (\exists x \in ℝ \exists n \in ℝ (\forall y \in B (x \leq y \to m \leq G (y)) \land \forall z \in A (m \leq z \to \|F (z)\| \leq n)) \to \exists x \in ℝ \exists n \in ℝ \forall y \in B (x \leq y \to \|(F \circ G) (y)\| \leq n))$
35	13 34	syl5bir	$⊢ (φ \land m \in ℝ) \to ((\exists x \in ℝ \forall y \in B (x \leq y \to m \leq G (y)) \land \exists n \in ℝ \forall z \in A (m \leq z \to \|F (z)\| \leq n)) \to \exists x \in ℝ \exists n \in ℝ \forall y \in B (x \leq y \to \|(F \circ G) (y)\| \leq n))$
36	5 35	mpand	$⊢ (φ \land m \in ℝ) \to (\exists n \in ℝ \forall z \in A (m \leq z \to \|F (z)\| \leq n) \to \exists x \in ℝ \exists n \in ℝ \forall y \in B (x \leq y \to \|(F \circ G) (y)\| \leq n))$
37	36	rexlimdva	$⊢ φ \to (\exists m \in ℝ \exists n \in ℝ \forall z \in A (m \leq z \to \|F (z)\| \leq n) \to \exists x \in ℝ \exists n \in ℝ \forall y \in B (x \leq y \to \|(F \circ G) (y)\| \leq n))$
38	12 37	mpd	$⊢ φ \to \exists x \in ℝ \exists n \in ℝ \forall y \in B (x \leq y \to \|(F \circ G) (y)\| \leq n)$
39		fco	$⊢ (F : A ⟶ ℂ \land G : B ⟶ A) \to (F \circ G) : B ⟶ ℂ$
40	1 3 39	syl2anc	$⊢ φ \to (F \circ G) : B ⟶ ℂ$
41		elo12	$⊢ ((F \circ G) : B ⟶ ℂ \land B \subseteq ℝ) \to (F \circ G \in 𝑂 (1) \leftrightarrow \exists x \in ℝ \exists n \in ℝ \forall y \in B (x \leq y \to \|(F \circ G) (y)\| \leq n))$
42	40 4 41	syl2anc	$⊢ φ \to (F \circ G \in 𝑂 (1) \leftrightarrow \exists x \in ℝ \exists n \in ℝ \forall y \in B (x \leq y \to \|(F \circ G) (y)\| \leq n))$
43	38 42	mpbird	$⊢ φ \to F \circ G \in 𝑂 (1)$

Metamath Proof Explorer

Theorem o1co

Proof