Theorem o1mul2

Description: The product of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 26-May-2016)

	Ref	Expression
Hypotheses	o1add2.1	|- ( ( ph /\ x e. A ) -> B e. V )
	o1add2.2	|- ( ( ph /\ x e. A ) -> C e. V )
	o1add2.3	|- ( ph -> ( x e. A |-> B ) e. O(1) )
	o1add2.4	|- ( ph -> ( x e. A |-> C ) e. O(1) )
Assertion	o1mul2	|- ( ph -> ( x e. A |-> ( B x. C ) ) e. O(1) )

Proof

Step	Hyp	Ref	Expression
1		o1add2.1	|- ( ( ph /\ x e. A ) -> B e. V )
2		o1add2.2	|- ( ( ph /\ x e. A ) -> C e. V )
3		o1add2.3	|- ( ph -> ( x e. A |-> B ) e. O(1) )
4		o1add2.4	|- ( ph -> ( x e. A |-> C ) e. O(1) )
5	1	ralrimiva	|- ( ph -> A. x e. A B e. V )
6		dmmptg	|- ( A. x e. A B e. V -> dom ( x e. A |-> B ) = A )
7	5 6	syl	|- ( ph -> dom ( x e. A |-> B ) = A )
8		o1dm	|- ( ( x e. A |-> B ) e. O(1) -> dom ( x e. A |-> B ) C_ RR )
9	3 8	syl	|- ( ph -> dom ( x e. A |-> B ) C_ RR )
10	7 9	eqsstrrd	|- ( ph -> A C_ RR )
11		reex	|- RR e. _V
12	11	ssex	|- ( A C_ RR -> A e. _V )
13	10 12	syl	|- ( ph -> A e. _V )
14		eqidd	|- ( ph -> ( x e. A |-> B ) = ( x e. A |-> B ) )
15		eqidd	|- ( ph -> ( x e. A |-> C ) = ( x e. A |-> C ) )
16	13 1 2 14 15	offval2	|- ( ph -> ( ( x e. A |-> B ) oF x. ( x e. A |-> C ) ) = ( x e. A |-> ( B x. C ) ) )
17		o1mul	|- ( ( ( x e. A |-> B ) e. O(1) /\ ( x e. A |-> C ) e. O(1) ) -> ( ( x e. A |-> B ) oF x. ( x e. A |-> C ) ) e. O(1) )
18	3 4 17	syl2anc	|- ( ph -> ( ( x e. A |-> B ) oF x. ( x e. A |-> C ) ) e. O(1) )
19	16 18	eqeltrrd	|- ( ph -> ( x e. A |-> ( B x. C ) ) e. O(1) )