o1of2

Description: Show that a binary operation preserves eventual boundedness. (Contributed by Mario Carneiro, 15-Sep-2014)

	Ref	Expression
Hypotheses	o1of2.1	$⊢ (m \in ℝ \land n \in ℝ) \to M \in ℝ$
	o1of2.2	$⊢ (x \in ℂ \land y \in ℂ) \to x R y \in ℂ$
	o1of2.3	$⊢ ((m \in ℝ \land n \in ℝ) \land (x \in ℂ \land y \in ℂ)) \to ((\|x\| \leq m \land \|y\| \leq n) \to \|x R y\| \leq M)$
Assertion	o1of2	$⊢ (F \in 𝑂 (1) \land G \in 𝑂 (1)) \to F R_{f} G \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		o1of2.1	$⊢ (m \in ℝ \land n \in ℝ) \to M \in ℝ$
2		o1of2.2	$⊢ (x \in ℂ \land y \in ℂ) \to x R y \in ℂ$
3		o1of2.3	$⊢ ((m \in ℝ \land n \in ℝ) \land (x \in ℂ \land y \in ℂ)) \to ((\|x\| \leq m \land \|y\| \leq n) \to \|x R y\| \leq M)$
4		o1f	$⊢ F \in 𝑂 (1) \to F : dom F ⟶ ℂ$
5		o1bdd	$⊢ (F \in 𝑂 (1) \land F : dom F ⟶ ℂ) \to \exists a \in ℝ \exists m \in ℝ \forall z \in dom F (a \leq z \to \|F (z)\| \leq m)$
6	4 5	mpdan	$⊢ F \in 𝑂 (1) \to \exists a \in ℝ \exists m \in ℝ \forall z \in dom F (a \leq z \to \|F (z)\| \leq m)$
7	6	adantr	$⊢ (F \in 𝑂 (1) \land G \in 𝑂 (1)) \to \exists a \in ℝ \exists m \in ℝ \forall z \in dom F (a \leq z \to \|F (z)\| \leq m)$
8		o1f	$⊢ G \in 𝑂 (1) \to G : dom G ⟶ ℂ$
9		o1bdd	$⊢ (G \in 𝑂 (1) \land G : dom G ⟶ ℂ) \to \exists b \in ℝ \exists n \in ℝ \forall z \in dom G (b \leq z \to \|G (z)\| \leq n)$
10	8 9	mpdan	$⊢ G \in 𝑂 (1) \to \exists b \in ℝ \exists n \in ℝ \forall z \in dom G (b \leq z \to \|G (z)\| \leq n)$
11	10	adantl	$⊢ (F \in 𝑂 (1) \land G \in 𝑂 (1)) \to \exists b \in ℝ \exists n \in ℝ \forall z \in dom G (b \leq z \to \|G (z)\| \leq n)$
12		reeanv	$⊢ \exists a \in ℝ \exists b \in ℝ (\exists m \in ℝ \forall z \in dom F (a \leq z \to \|F (z)\| \leq m) \land \exists n \in ℝ \forall z \in dom G (b \leq z \to \|G (z)\| \leq n)) \leftrightarrow (\exists a \in ℝ \exists m \in ℝ \forall z \in dom F (a \leq z \to \|F (z)\| \leq m) \land \exists b \in ℝ \exists n \in ℝ \forall z \in dom G (b \leq z \to \|G (z)\| \leq n))$
13		reeanv	$⊢ \exists m \in ℝ \exists n \in ℝ (\forall z \in dom F (a \leq z \to \|F (z)\| \leq m) \land \forall z \in dom G (b \leq z \to \|G (z)\| \leq n)) \leftrightarrow (\exists m \in ℝ \forall z \in dom F (a \leq z \to \|F (z)\| \leq m) \land \exists n \in ℝ \forall z \in dom G (b \leq z \to \|G (z)\| \leq n))$
14		inss1	$⊢ dom F \cap dom G \subseteq dom F$
15		ssralv	$⊢ dom F \cap dom G \subseteq dom F \to (\forall z \in dom F (a \leq z \to \|F (z)\| \leq m) \to \forall z \in (dom F \cap dom G) (a \leq z \to \|F (z)\| \leq m))$
16	14 15	ax-mp	$⊢ \forall z \in dom F (a \leq z \to \|F (z)\| \leq m) \to \forall z \in (dom F \cap dom G) (a \leq z \to \|F (z)\| \leq m)$
17		inss2	$⊢ dom F \cap dom G \subseteq dom G$
18		ssralv	$⊢ dom F \cap dom G \subseteq dom G \to (\forall z \in dom G (b \leq z \to \|G (z)\| \leq n) \to \forall z \in (dom F \cap dom G) (b \leq z \to \|G (z)\| \leq n))$
19	17 18	ax-mp	$⊢ \forall z \in dom G (b \leq z \to \|G (z)\| \leq n) \to \forall z \in (dom F \cap dom G) (b \leq z \to \|G (z)\| \leq n)$
20	16 19	anim12i	$⊢ (\forall z \in dom F (a \leq z \to \|F (z)\| \leq m) \land \forall z \in dom G (b \leq z \to \|G (z)\| \leq n)) \to (\forall z \in (dom F \cap dom G) (a \leq z \to \|F (z)\| \leq m) \land \forall z \in (dom F \cap dom G) (b \leq z \to \|G (z)\| \leq n))$
21		r19.26	$⊢ \forall z \in (dom F \cap dom G) ((a \leq z \to \|F (z)\| \leq m) \land (b \leq z \to \|G (z)\| \leq n)) \leftrightarrow (\forall z \in (dom F \cap dom G) (a \leq z \to \|F (z)\| \leq m) \land \forall z \in (dom F \cap dom G) (b \leq z \to \|G (z)\| \leq n))$
22	20 21	sylibr	$⊢ (\forall z \in dom F (a \leq z \to \|F (z)\| \leq m) \land \forall z \in dom G (b \leq z \to \|G (z)\| \leq n)) \to \forall z \in (dom F \cap dom G) ((a \leq z \to \|F (z)\| \leq m) \land (b \leq z \to \|G (z)\| \leq n))$
23		anim12	$⊢ ((a \leq z \to \|F (z)\| \leq m) \land (b \leq z \to \|G (z)\| \leq n)) \to ((a \leq z \land b \leq z) \to (\|F (z)\| \leq m \land \|G (z)\| \leq n))$
24		simplrl	$⊢ (((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \to a \in ℝ$
25	24	adantr	$⊢ ((((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \land z \in (dom F \cap dom G)) \to a \in ℝ$
26		simplrr	$⊢ (((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \to b \in ℝ$
27	26	adantr	$⊢ ((((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \land z \in (dom F \cap dom G)) \to b \in ℝ$
28		o1dm	$⊢ F \in 𝑂 (1) \to dom F \subseteq ℝ$
29	28	ad3antrrr	$⊢ (((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \to dom F \subseteq ℝ$
30	14 29	sstrid	$⊢ (((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \to dom F \cap dom G \subseteq ℝ$
31	30	sselda	$⊢ ((((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \land z \in (dom F \cap dom G)) \to z \in ℝ$
32		maxle	$⊢ (a \in ℝ \land b \in ℝ \land z \in ℝ) \to (if (a \leq b, b, a) \leq z \leftrightarrow (a \leq z \land b \leq z))$
33	25 27 31 32	syl3anc	$⊢ ((((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \land z \in (dom F \cap dom G)) \to (if (a \leq b, b, a) \leq z \leftrightarrow (a \leq z \land b \leq z))$
34	33	biimpd	$⊢ ((((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \land z \in (dom F \cap dom G)) \to (if (a \leq b, b, a) \leq z \to (a \leq z \land b \leq z))$
35	4	ad3antrrr	$⊢ (((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \to F : dom F ⟶ ℂ$
36	14	sseli	$⊢ z \in (dom F \cap dom G) \to z \in dom F$
37		ffvelrn	$⊢ (F : dom F ⟶ ℂ \land z \in dom F) \to F (z) \in ℂ$
38	35 36 37	syl2an	$⊢ ((((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \land z \in (dom F \cap dom G)) \to F (z) \in ℂ$
39	8	ad3antlr	$⊢ (((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \to G : dom G ⟶ ℂ$
40	17	sseli	$⊢ z \in (dom F \cap dom G) \to z \in dom G$
41		ffvelrn	$⊢ (G : dom G ⟶ ℂ \land z \in dom G) \to G (z) \in ℂ$
42	39 40 41	syl2an	$⊢ ((((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \land z \in (dom F \cap dom G)) \to G (z) \in ℂ$
43	3	ralrimivva	$⊢ (m \in ℝ \land n \in ℝ) \to \forall x \in ℂ \forall y \in ℂ ((\|x\| \leq m \land \|y\| \leq n) \to \|x R y\| \leq M)$
44	43	ad2antlr	$⊢ ((((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \land z \in (dom F \cap dom G)) \to \forall x \in ℂ \forall y \in ℂ ((\|x\| \leq m \land \|y\| \leq n) \to \|x R y\| \leq M)$
45		fveq2	$⊢ x = F (z) \to \|x\| = \|F (z)\|$
46	45	breq1d	$⊢ x = F (z) \to (\|x\| \leq m \leftrightarrow \|F (z)\| \leq m)$
47	46	anbi1d	$⊢ x = F (z) \to ((\|x\| \leq m \land \|y\| \leq n) \leftrightarrow (\|F (z)\| \leq m \land \|y\| \leq n))$
48		fvoveq1	$⊢ x = F (z) \to \|x R y\| = \|F (z) R y\|$
49	48	breq1d	$⊢ x = F (z) \to (\|x R y\| \leq M \leftrightarrow \|F (z) R y\| \leq M)$
50	47 49	imbi12d	$⊢ x = F (z) \to (((\|x\| \leq m \land \|y\| \leq n) \to \|x R y\| \leq M) \leftrightarrow ((\|F (z)\| \leq m \land \|y\| \leq n) \to \|F (z) R y\| \leq M))$
51		fveq2	$⊢ y = G (z) \to \|y\| = \|G (z)\|$
52	51	breq1d	$⊢ y = G (z) \to (\|y\| \leq n \leftrightarrow \|G (z)\| \leq n)$
53	52	anbi2d	$⊢ y = G (z) \to ((\|F (z)\| \leq m \land \|y\| \leq n) \leftrightarrow (\|F (z)\| \leq m \land \|G (z)\| \leq n))$
54		oveq2	$⊢ y = G (z) \to F (z) R y = F (z) R G (z)$
55	54	fveq2d	$⊢ y = G (z) \to \|F (z) R y\| = \|F (z) R G (z)\|$
56	55	breq1d	$⊢ y = G (z) \to (\|F (z) R y\| \leq M \leftrightarrow \|F (z) R G (z)\| \leq M)$
57	53 56	imbi12d	$⊢ y = G (z) \to (((\|F (z)\| \leq m \land \|y\| \leq n) \to \|F (z) R y\| \leq M) \leftrightarrow ((\|F (z)\| \leq m \land \|G (z)\| \leq n) \to \|F (z) R G (z)\| \leq M))$
58	50 57	rspc2va	$⊢ ((F (z) \in ℂ \land G (z) \in ℂ) \land \forall x \in ℂ \forall y \in ℂ ((\|x\| \leq m \land \|y\| \leq n) \to \|x R y\| \leq M)) \to ((\|F (z)\| \leq m \land \|G (z)\| \leq n) \to \|F (z) R G (z)\| \leq M)$
59	38 42 44 58	syl21anc	$⊢ ((((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \land z \in (dom F \cap dom G)) \to ((\|F (z)\| \leq m \land \|G (z)\| \leq n) \to \|F (z) R G (z)\| \leq M)$
60	35	ffnd	$⊢ (((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \to F Fn dom F$
61	39	ffnd	$⊢ (((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \to G Fn dom G$
62		reex	$⊢ ℝ \in V$
63		ssexg	$⊢ (dom F \subseteq ℝ \land ℝ \in V) \to dom F \in V$
64	29 62 63	sylancl	$⊢ (((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \to dom F \in V$
65		dmexg	$⊢ G \in 𝑂 (1) \to dom G \in V$
66	65	ad3antlr	$⊢ (((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \to dom G \in V$
67		eqid	$⊢ dom F \cap dom G = dom F \cap dom G$
68		eqidd	$⊢ ((((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \land z \in dom F) \to F (z) = F (z)$
69		eqidd	$⊢ ((((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \land z \in dom G) \to G (z) = G (z)$
70	60 61 64 66 67 68 69	ofval	$⊢ ((((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \land z \in (dom F \cap dom G)) \to (F R_{f} G) (z) = F (z) R G (z)$
71	70	fveq2d	$⊢ ((((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \land z \in (dom F \cap dom G)) \to \|(F R_{f} G) (z)\| = \|F (z) R G (z)\|$
72	71	breq1d	$⊢ ((((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \land z \in (dom F \cap dom G)) \to (\|(F R_{f} G) (z)\| \leq M \leftrightarrow \|F (z) R G (z)\| \leq M)$
73	59 72	sylibrd	$⊢ ((((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \land z \in (dom F \cap dom G)) \to ((\|F (z)\| \leq m \land \|G (z)\| \leq n) \to \|(F R_{f} G) (z)\| \leq M)$
74	34 73	imim12d	$⊢ ((((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \land z \in (dom F \cap dom G)) \to (((a \leq z \land b \leq z) \to (\|F (z)\| \leq m \land \|G (z)\| \leq n)) \to (if (a \leq b, b, a) \leq z \to \|(F R_{f} G) (z)\| \leq M))$
75	23 74	syl5	$⊢ ((((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \land z \in (dom F \cap dom G)) \to (((a \leq z \to \|F (z)\| \leq m) \land (b \leq z \to \|G (z)\| \leq n)) \to (if (a \leq b, b, a) \leq z \to \|(F R_{f} G) (z)\| \leq M))$
76	75	ralimdva	$⊢ (((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \to (\forall z \in (dom F \cap dom G) ((a \leq z \to \|F (z)\| \leq m) \land (b \leq z \to \|G (z)\| \leq n)) \to \forall z \in (dom F \cap dom G) (if (a \leq b, b, a) \leq z \to \|(F R_{f} G) (z)\| \leq M))$
77	2	adantl	$⊢ ((((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \land (x \in ℂ \land y \in ℂ)) \to x R y \in ℂ$
78	77 35 39 64 66 67	off	$⊢ (((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \to (F R_{f} G) : dom F \cap dom G ⟶ ℂ$
79	26 24	ifcld	$⊢ (((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \to if (a \leq b, b, a) \in ℝ$
80	1	adantl	$⊢ (((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \to M \in ℝ$
81		elo12r	$⊢ (((F R_{f} G) : dom F \cap dom G ⟶ ℂ \land dom F \cap dom G \subseteq ℝ) \land (if (a \leq b, b, a) \in ℝ \land M \in ℝ) \land \forall z \in (dom F \cap dom G) (if (a \leq b, b, a) \leq z \to \|(F R_{f} G) (z)\| \leq M)) \to F R_{f} G \in 𝑂 (1)$
82	81	3expia	$⊢ (((F R_{f} G) : dom F \cap dom G ⟶ ℂ \land dom F \cap dom G \subseteq ℝ) \land (if (a \leq b, b, a) \in ℝ \land M \in ℝ)) \to (\forall z \in (dom F \cap dom G) (if (a \leq b, b, a) \leq z \to \|(F R_{f} G) (z)\| \leq M) \to F R_{f} G \in 𝑂 (1))$
83	78 30 79 80 82	syl22anc	$⊢ (((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \to (\forall z \in (dom F \cap dom G) (if (a \leq b, b, a) \leq z \to \|(F R_{f} G) (z)\| \leq M) \to F R_{f} G \in 𝑂 (1))$
84	76 83	syld	$⊢ (((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \to (\forall z \in (dom F \cap dom G) ((a \leq z \to \|F (z)\| \leq m) \land (b \leq z \to \|G (z)\| \leq n)) \to F R_{f} G \in 𝑂 (1))$
85	22 84	syl5	$⊢ (((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \land (m \in ℝ \land n \in ℝ)) \to ((\forall z \in dom F (a \leq z \to \|F (z)\| \leq m) \land \forall z \in dom G (b \leq z \to \|G (z)\| \leq n)) \to F R_{f} G \in 𝑂 (1))$
86	85	rexlimdvva	$⊢ ((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \to (\exists m \in ℝ \exists n \in ℝ (\forall z \in dom F (a \leq z \to \|F (z)\| \leq m) \land \forall z \in dom G (b \leq z \to \|G (z)\| \leq n)) \to F R_{f} G \in 𝑂 (1))$
87	13 86	syl5bir	$⊢ ((F \in 𝑂 (1) \land G \in 𝑂 (1)) \land (a \in ℝ \land b \in ℝ)) \to ((\exists m \in ℝ \forall z \in dom F (a \leq z \to \|F (z)\| \leq m) \land \exists n \in ℝ \forall z \in dom G (b \leq z \to \|G (z)\| \leq n)) \to F R_{f} G \in 𝑂 (1))$
88	87	rexlimdvva	$⊢ (F \in 𝑂 (1) \land G \in 𝑂 (1)) \to (\exists a \in ℝ \exists b \in ℝ (\exists m \in ℝ \forall z \in dom F (a \leq z \to \|F (z)\| \leq m) \land \exists n \in ℝ \forall z \in dom G (b \leq z \to \|G (z)\| \leq n)) \to F R_{f} G \in 𝑂 (1))$
89	12 88	syl5bir	$⊢ (F \in 𝑂 (1) \land G \in 𝑂 (1)) \to ((\exists a \in ℝ \exists m \in ℝ \forall z \in dom F (a \leq z \to \|F (z)\| \leq m) \land \exists b \in ℝ \exists n \in ℝ \forall z \in dom G (b \leq z \to \|G (z)\| \leq n)) \to F R_{f} G \in 𝑂 (1))$
90	7 11 89	mp2and	$⊢ (F \in 𝑂 (1) \land G \in 𝑂 (1)) \to F R_{f} G \in 𝑂 (1)$

Metamath Proof Explorer

Theorem o1of2

Proof