This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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) )