Metamath Proof Explorer


Theorem o1sub2

Description: The product of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014)

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 o1sub2
|- ( ph -> ( x e. A |-> ( B - 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 e. A |-> C ) ) = ( x e. A |-> ( B - C ) ) )
17 o1sub
 |-  ( ( ( x e. A |-> B ) e. O(1) /\ ( x e. A |-> C ) e. O(1) ) -> ( ( x e. A |-> B ) oF - ( x e. A |-> C ) ) e. O(1) )
18 3 4 17 syl2anc
 |-  ( ph -> ( ( x e. A |-> B ) oF - ( x e. A |-> C ) ) e. O(1) )
19 16 18 eqeltrrd
 |-  ( ph -> ( x e. A |-> ( B - C ) ) e. O(1) )