Step |
Hyp |
Ref |
Expression |
1 |
|
lo1sub.1 |
|- ( ( ph /\ x e. A ) -> B e. V ) |
2 |
|
lo1sub.2 |
|- ( ( ph /\ x e. A ) -> C e. RR ) |
3 |
|
lo1sub.3 |
|- ( ph -> ( x e. A |-> B ) e. <_O(1) ) |
4 |
|
lo1sub.4 |
|- ( ph -> ( x e. A |-> C ) e. O(1) ) |
5 |
1 3
|
lo1mptrcl |
|- ( ( ph /\ x e. A ) -> B e. RR ) |
6 |
5
|
recnd |
|- ( ( ph /\ x e. A ) -> B e. CC ) |
7 |
2
|
recnd |
|- ( ( ph /\ x e. A ) -> C e. CC ) |
8 |
6 7
|
negsubd |
|- ( ( ph /\ x e. A ) -> ( B + -u C ) = ( B - C ) ) |
9 |
8
|
mpteq2dva |
|- ( ph -> ( x e. A |-> ( B + -u C ) ) = ( x e. A |-> ( B - C ) ) ) |
10 |
2
|
renegcld |
|- ( ( ph /\ x e. A ) -> -u C e. RR ) |
11 |
2
|
o1lo1 |
|- ( ph -> ( ( x e. A |-> C ) e. O(1) <-> ( ( x e. A |-> C ) e. <_O(1) /\ ( x e. A |-> -u C ) e. <_O(1) ) ) ) |
12 |
4 11
|
mpbid |
|- ( ph -> ( ( x e. A |-> C ) e. <_O(1) /\ ( x e. A |-> -u C ) e. <_O(1) ) ) |
13 |
12
|
simprd |
|- ( ph -> ( x e. A |-> -u C ) e. <_O(1) ) |
14 |
5 10 3 13
|
lo1add |
|- ( ph -> ( x e. A |-> ( B + -u C ) ) e. <_O(1) ) |
15 |
9 14
|
eqeltrrd |
|- ( ph -> ( x e. A |-> ( B - C ) ) e. <_O(1) ) |