Step |
Hyp |
Ref |
Expression |
1 |
|
simpl |
|- ( ( x = A /\ y = B ) -> x = A ) |
2 |
1
|
eqeq1d |
|- ( ( x = A /\ y = B ) -> ( x = 0 <-> A = 0 ) ) |
3 |
|
simpr |
|- ( ( x = A /\ y = B ) -> y = B ) |
4 |
3
|
eqeq1d |
|- ( ( x = A /\ y = B ) -> ( y = 0 <-> B = 0 ) ) |
5 |
2 4
|
orbi12d |
|- ( ( x = A /\ y = B ) -> ( ( x = 0 \/ y = 0 ) <-> ( A = 0 \/ B = 0 ) ) ) |
6 |
3
|
breq2d |
|- ( ( x = A /\ y = B ) -> ( 0 < y <-> 0 < B ) ) |
7 |
1
|
eqeq1d |
|- ( ( x = A /\ y = B ) -> ( x = +oo <-> A = +oo ) ) |
8 |
6 7
|
anbi12d |
|- ( ( x = A /\ y = B ) -> ( ( 0 < y /\ x = +oo ) <-> ( 0 < B /\ A = +oo ) ) ) |
9 |
3
|
breq1d |
|- ( ( x = A /\ y = B ) -> ( y < 0 <-> B < 0 ) ) |
10 |
1
|
eqeq1d |
|- ( ( x = A /\ y = B ) -> ( x = -oo <-> A = -oo ) ) |
11 |
9 10
|
anbi12d |
|- ( ( x = A /\ y = B ) -> ( ( y < 0 /\ x = -oo ) <-> ( B < 0 /\ A = -oo ) ) ) |
12 |
8 11
|
orbi12d |
|- ( ( x = A /\ y = B ) -> ( ( ( 0 < y /\ x = +oo ) \/ ( y < 0 /\ x = -oo ) ) <-> ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) ) ) |
13 |
1
|
breq2d |
|- ( ( x = A /\ y = B ) -> ( 0 < x <-> 0 < A ) ) |
14 |
3
|
eqeq1d |
|- ( ( x = A /\ y = B ) -> ( y = +oo <-> B = +oo ) ) |
15 |
13 14
|
anbi12d |
|- ( ( x = A /\ y = B ) -> ( ( 0 < x /\ y = +oo ) <-> ( 0 < A /\ B = +oo ) ) ) |
16 |
1
|
breq1d |
|- ( ( x = A /\ y = B ) -> ( x < 0 <-> A < 0 ) ) |
17 |
3
|
eqeq1d |
|- ( ( x = A /\ y = B ) -> ( y = -oo <-> B = -oo ) ) |
18 |
16 17
|
anbi12d |
|- ( ( x = A /\ y = B ) -> ( ( x < 0 /\ y = -oo ) <-> ( A < 0 /\ B = -oo ) ) ) |
19 |
15 18
|
orbi12d |
|- ( ( x = A /\ y = B ) -> ( ( ( 0 < x /\ y = +oo ) \/ ( x < 0 /\ y = -oo ) ) <-> ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) |
20 |
12 19
|
orbi12d |
|- ( ( x = A /\ y = B ) -> ( ( ( ( 0 < y /\ x = +oo ) \/ ( y < 0 /\ x = -oo ) ) \/ ( ( 0 < x /\ y = +oo ) \/ ( x < 0 /\ y = -oo ) ) ) <-> ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) ) |
21 |
6 10
|
anbi12d |
|- ( ( x = A /\ y = B ) -> ( ( 0 < y /\ x = -oo ) <-> ( 0 < B /\ A = -oo ) ) ) |
22 |
9 7
|
anbi12d |
|- ( ( x = A /\ y = B ) -> ( ( y < 0 /\ x = +oo ) <-> ( B < 0 /\ A = +oo ) ) ) |
23 |
21 22
|
orbi12d |
|- ( ( x = A /\ y = B ) -> ( ( ( 0 < y /\ x = -oo ) \/ ( y < 0 /\ x = +oo ) ) <-> ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) ) ) |
24 |
13 17
|
anbi12d |
|- ( ( x = A /\ y = B ) -> ( ( 0 < x /\ y = -oo ) <-> ( 0 < A /\ B = -oo ) ) ) |
25 |
16 14
|
anbi12d |
|- ( ( x = A /\ y = B ) -> ( ( x < 0 /\ y = +oo ) <-> ( A < 0 /\ B = +oo ) ) ) |
26 |
24 25
|
orbi12d |
|- ( ( x = A /\ y = B ) -> ( ( ( 0 < x /\ y = -oo ) \/ ( x < 0 /\ y = +oo ) ) <-> ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) |
27 |
23 26
|
orbi12d |
|- ( ( x = A /\ y = B ) -> ( ( ( ( 0 < y /\ x = -oo ) \/ ( y < 0 /\ x = +oo ) ) \/ ( ( 0 < x /\ y = -oo ) \/ ( x < 0 /\ y = +oo ) ) ) <-> ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) ) |
28 |
|
oveq12 |
|- ( ( x = A /\ y = B ) -> ( x x. y ) = ( A x. B ) ) |
29 |
27 28
|
ifbieq2d |
|- ( ( x = A /\ y = B ) -> if ( ( ( ( 0 < y /\ x = -oo ) \/ ( y < 0 /\ x = +oo ) ) \/ ( ( 0 < x /\ y = -oo ) \/ ( x < 0 /\ y = +oo ) ) ) , -oo , ( x x. y ) ) = if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) |
30 |
20 29
|
ifbieq2d |
|- ( ( x = A /\ y = B ) -> if ( ( ( ( 0 < y /\ x = +oo ) \/ ( y < 0 /\ x = -oo ) ) \/ ( ( 0 < x /\ y = +oo ) \/ ( x < 0 /\ y = -oo ) ) ) , +oo , if ( ( ( ( 0 < y /\ x = -oo ) \/ ( y < 0 /\ x = +oo ) ) \/ ( ( 0 < x /\ y = -oo ) \/ ( x < 0 /\ y = +oo ) ) ) , -oo , ( x x. y ) ) ) = if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) ) |
31 |
5 30
|
ifbieq2d |
|- ( ( x = A /\ y = B ) -> if ( ( x = 0 \/ y = 0 ) , 0 , if ( ( ( ( 0 < y /\ x = +oo ) \/ ( y < 0 /\ x = -oo ) ) \/ ( ( 0 < x /\ y = +oo ) \/ ( x < 0 /\ y = -oo ) ) ) , +oo , if ( ( ( ( 0 < y /\ x = -oo ) \/ ( y < 0 /\ x = +oo ) ) \/ ( ( 0 < x /\ y = -oo ) \/ ( x < 0 /\ y = +oo ) ) ) , -oo , ( x x. y ) ) ) ) = if ( ( A = 0 \/ B = 0 ) , 0 , if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) ) ) |
32 |
|
df-xmul |
|- *e = ( x e. RR* , y e. RR* |-> if ( ( x = 0 \/ y = 0 ) , 0 , if ( ( ( ( 0 < y /\ x = +oo ) \/ ( y < 0 /\ x = -oo ) ) \/ ( ( 0 < x /\ y = +oo ) \/ ( x < 0 /\ y = -oo ) ) ) , +oo , if ( ( ( ( 0 < y /\ x = -oo ) \/ ( y < 0 /\ x = +oo ) ) \/ ( ( 0 < x /\ y = -oo ) \/ ( x < 0 /\ y = +oo ) ) ) , -oo , ( x x. y ) ) ) ) ) |
33 |
|
c0ex |
|- 0 e. _V |
34 |
|
pnfex |
|- +oo e. _V |
35 |
|
mnfxr |
|- -oo e. RR* |
36 |
35
|
elexi |
|- -oo e. _V |
37 |
|
ovex |
|- ( A x. B ) e. _V |
38 |
36 37
|
ifex |
|- if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) e. _V |
39 |
34 38
|
ifex |
|- if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) e. _V |
40 |
33 39
|
ifex |
|- if ( ( A = 0 \/ B = 0 ) , 0 , if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) ) e. _V |
41 |
31 32 40
|
ovmpoa |
|- ( ( A e. RR* /\ B e. RR* ) -> ( A *e B ) = if ( ( A = 0 \/ B = 0 ) , 0 , if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) ) ) |