Metamath Proof Explorer

Theorem ltsosr

Description: Signed real 'less than' is a strict ordering. (Contributed by NM, 19-Feb-1996) (New usage is discouraged.)

Ref Expression
Assertion ltsosr 
|-

Proof

Step Hyp Ref Expression
1 df-nr 
 |-  R. = ( ( P. X. P. ) /. ~R )
2 breq1 
 |-  ( [ <. x , y >. ] ~R = f -> ( [ <. x , y >. ] ~R . ] ~R <-> f . ] ~R ) )
3 eqeq1 
 |-  ( [ <. x , y >. ] ~R = f -> ( [ <. x , y >. ] ~R = [ <. z , w >. ] ~R <-> f = [ <. z , w >. ] ~R ) )
4 breq2 
 |-  ( [ <. x , y >. ] ~R = f -> ( [ <. z , w >. ] ~R . ] ~R <-> [ <. z , w >. ] ~R
5 3 4 orbi12d 
 |-  ( [ <. x , y >. ] ~R = f -> ( ( [ <. x , y >. ] ~R = [ <. z , w >. ] ~R \/ [ <. z , w >. ] ~R . ] ~R ) <-> ( f = [ <. z , w >. ] ~R \/ [ <. z , w >. ] ~R
6 5 notbid 
 |-  ( [ <. x , y >. ] ~R = f -> ( -. ( [ <. x , y >. ] ~R = [ <. z , w >. ] ~R \/ [ <. z , w >. ] ~R . ] ~R ) <-> -. ( f = [ <. z , w >. ] ~R \/ [ <. z , w >. ] ~R
7 2 6 bibi12d 
 |-  ( [ <. x , y >. ] ~R = f -> ( ( [ <. x , y >. ] ~R . ] ~R <-> -. ( [ <. x , y >. ] ~R = [ <. z , w >. ] ~R \/ [ <. z , w >. ] ~R . ] ~R ) ) <-> ( f . ] ~R <-> -. ( f = [ <. z , w >. ] ~R \/ [ <. z , w >. ] ~R
8 breq2 
 |-  ( [ <. z , w >. ] ~R = g -> ( f . ] ~R <-> f
9 eqeq2 
 |-  ( [ <. z , w >. ] ~R = g -> ( f = [ <. z , w >. ] ~R <-> f = g ) )
10 breq1 
 |-  ( [ <. z , w >. ] ~R = g -> ( [ <. z , w >. ] ~R  g
11 9 10 orbi12d 
 |-  ( [ <. z , w >. ] ~R = g -> ( ( f = [ <. z , w >. ] ~R \/ [ <. z , w >. ] ~R  ( f = g \/ g
12 11 notbid 
 |-  ( [ <. z , w >. ] ~R = g -> ( -. ( f = [ <. z , w >. ] ~R \/ [ <. z , w >. ] ~R  -. ( f = g \/ g
13 8 12 bibi12d 
 |-  ( [ <. z , w >. ] ~R = g -> ( ( f . ] ~R <-> -. ( f = [ <. z , w >. ] ~R \/ [ <. z , w >. ] ~R  ( f  -. ( f = g \/ g
14 ltsrpr 
 |-  ( [ <. x , y >. ] ~R . ] ~R <-> ( x +P. w )
15 addclpr 
 |-  ( ( x e. P. /\ w e. P. ) -> ( x +P. w ) e. P. )
16 addclpr 
 |-  ( ( y e. P. /\ z e. P. ) -> ( y +P. z ) e. P. )
17 ltsopr 
 |-
18 sotric 
 |-  ( ( 
 ( ( x +P. w ) 
 -. ( ( x +P. w ) = ( y +P. z ) \/ ( y +P. z )
19 17 18 mpan 
 |-  ( ( ( x +P. w ) e. P. /\ ( y +P. z ) e. P. ) -> ( ( x +P. w ) 
 -. ( ( x +P. w ) = ( y +P. z ) \/ ( y +P. z )
20 15 16 19 syl2an 
 |-  ( ( ( x e. P. /\ w e. P. ) /\ ( y e. P. /\ z e. P. ) ) -> ( ( x +P. w ) 
 -. ( ( x +P. w ) = ( y +P. z ) \/ ( y +P. z )
21 20 an42s 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( ( x +P. w ) 
 -. ( ( x +P. w ) = ( y +P. z ) \/ ( y +P. z )
22 enreceq 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( [ <. x , y >. ] ~R = [ <. z , w >. ] ~R <-> ( x +P. w ) = ( y +P. z ) ) )
23 ltsrpr 
 |-  ( [ <. z , w >. ] ~R . ] ~R <-> ( z +P. y )
24 addcompr 
 |-  ( z +P. y ) = ( y +P. z )
25 addcompr 
 |-  ( w +P. x ) = ( x +P. w )
26 24 25 breq12i 
 |-  ( ( z +P. y ) 
 ( y +P. z )
27 23 26 bitri 
 |-  ( [ <. z , w >. ] ~R . ] ~R <-> ( y +P. z )
28 27 a1i 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( [ <. z , w >. ] ~R . ] ~R <-> ( y +P. z )
29 22 28 orbi12d 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( ( [ <. x , y >. ] ~R = [ <. z , w >. ] ~R \/ [ <. z , w >. ] ~R . ] ~R ) <-> ( ( x +P. w ) = ( y +P. z ) \/ ( y +P. z )
30 29 notbid 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( -. ( [ <. x , y >. ] ~R = [ <. z , w >. ] ~R \/ [ <. z , w >. ] ~R . ] ~R ) <-> -. ( ( x +P. w ) = ( y +P. z ) \/ ( y +P. z )
31 21 30 bitr4d 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( ( x +P. w ) 
 -. ( [ <. x , y >. ] ~R = [ <. z , w >. ] ~R \/ [ <. z , w >. ] ~R . ] ~R ) ) )
32 14 31 syl5bb 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( [ <. x , y >. ] ~R . ] ~R <-> -. ( [ <. x , y >. ] ~R = [ <. z , w >. ] ~R \/ [ <. z , w >. ] ~R . ] ~R ) ) )
33 1 7 13 32 2ecoptocl 
 |-  ( ( f e. R. /\ g e. R. ) -> ( f  -. ( f = g \/ g
34 2 anbi1d 
 |-  ( [ <. x , y >. ] ~R = f -> ( ( [ <. x , y >. ] ~R . ] ~R /\ [ <. z , w >. ] ~R . ] ~R ) <-> ( f . ] ~R /\ [ <. z , w >. ] ~R . ] ~R ) ) )
35 breq1 
 |-  ( [ <. x , y >. ] ~R = f -> ( [ <. x , y >. ] ~R . ] ~R <-> f . ] ~R ) )
36 34 35 imbi12d 
 |-  ( [ <. x , y >. ] ~R = f -> ( ( ( [ <. x , y >. ] ~R . ] ~R /\ [ <. z , w >. ] ~R . ] ~R ) -> [ <. x , y >. ] ~R . ] ~R ) <-> ( ( f . ] ~R /\ [ <. z , w >. ] ~R . ] ~R ) -> f . ] ~R ) ) )
37 breq1 
 |-  ( [ <. z , w >. ] ~R = g -> ( [ <. z , w >. ] ~R . ] ~R <-> g . ] ~R ) )
38 8 37 anbi12d 
 |-  ( [ <. z , w >. ] ~R = g -> ( ( f . ] ~R /\ [ <. z , w >. ] ~R . ] ~R ) <-> ( f . ] ~R ) ) )
39 38 imbi1d 
 |-  ( [ <. z , w >. ] ~R = g -> ( ( ( f . ] ~R /\ [ <. z , w >. ] ~R . ] ~R ) -> f . ] ~R ) <-> ( ( f . ] ~R ) -> f . ] ~R ) ) )
40 breq2 
 |-  ( [ <. v , u >. ] ~R = h -> ( g . ] ~R <-> g
41 40 anbi2d 
 |-  ( [ <. v , u >. ] ~R = h -> ( ( f . ] ~R ) <-> ( f
42 breq2 
 |-  ( [ <. v , u >. ] ~R = h -> ( f . ] ~R <-> f
43 41 42 imbi12d 
 |-  ( [ <. v , u >. ] ~R = h -> ( ( ( f . ] ~R ) -> f . ] ~R ) <-> ( ( f  f
44 ovex 
 |-  ( x +P. w ) e. _V
45 ovex 
 |-  ( y +P. z ) e. _V
46 ltapr 
 |-  ( h e. P. -> ( f 
 ( h +P. f )
47 vex 
 |-  u e. _V
48 addcompr 
 |-  ( f +P. g ) = ( g +P. f )
49 44 45 46 47 48 caovord2 
 |-  ( u e. P. -> ( ( x +P. w ) 
 ( ( x +P. w ) +P. u )
50 addasspr 
 |-  ( ( x +P. w ) +P. u ) = ( x +P. ( w +P. u ) )
51 addasspr 
 |-  ( ( y +P. z ) +P. u ) = ( y +P. ( z +P. u ) )
52 50 51 breq12i 
 |-  ( ( ( x +P. w ) +P. u ) 
 ( x +P. ( w +P. u ) )
53 49 52 bitrdi 
 |-  ( u e. P. -> ( ( x +P. w ) 
 ( x +P. ( w +P. u ) )
54 14 53 syl5bb 
 |-  ( u e. P. -> ( [ <. x , y >. ] ~R . ] ~R <-> ( x +P. ( w +P. u ) )
55 ltsrpr 
 |-  ( [ <. z , w >. ] ~R . ] ~R <-> ( z +P. u )
56 ltapr 
 |-  ( y e. P. -> ( ( z +P. u ) 
 ( y +P. ( z +P. u ) )
57 55 56 syl5bb 
 |-  ( y e. P. -> ( [ <. z , w >. ] ~R . ] ~R <-> ( y +P. ( z +P. u ) )
58 54 57 bi2anan9r 
 |-  ( ( y e. P. /\ u e. P. ) -> ( ( [ <. x , y >. ] ~R . ] ~R /\ [ <. z , w >. ] ~R . ] ~R ) <-> ( ( x +P. ( w +P. u ) )
59 ltrelpr 
 |-
60 17 59 sotri 
 |-  ( ( ( x +P. ( w +P. u ) ) 
 ( x +P. ( w +P. u ) )
61 dmplp 
 |-  dom +P. = ( P. X. P. )
62 0npr 
 |-  -. (/) e. P.
63 ltapr 
 |-  ( w e. P. -> ( ( x +P. u ) 
 ( w +P. ( x +P. u ) )
64 61 59 62 63 ndmovordi 
 |-  ( ( w +P. ( x +P. u ) ) 
 ( x +P. u )
65 vex 
 |-  x e. _V
66 vex 
 |-  w e. _V
67 addasspr 
 |-  ( ( f +P. g ) +P. h ) = ( f +P. ( g +P. h ) )
68 65 66 47 48 67 caov12 
 |-  ( x +P. ( w +P. u ) ) = ( w +P. ( x +P. u ) )
69 vex 
 |-  y e. _V
70 vex 
 |-  v e. _V
71 69 66 70 48 67 caov12 
 |-  ( y +P. ( w +P. v ) ) = ( w +P. ( y +P. v ) )
72 68 71 breq12i 
 |-  ( ( x +P. ( w +P. u ) ) 
 ( w +P. ( x +P. u ) )
73 ltsrpr 
 |-  ( [ <. x , y >. ] ~R . ] ~R <-> ( x +P. u )
74 64 72 73 3imtr4i 
 |-  ( ( x +P. ( w +P. u ) ) 
 [ <. x , y >. ] ~R . ] ~R )
75 60 74 syl 
 |-  ( ( ( x +P. ( w +P. u ) ) 
 [ <. x , y >. ] ~R . ] ~R )
76 58 75 syl6bi 
 |-  ( ( y e. P. /\ u e. P. ) -> ( ( [ <. x , y >. ] ~R . ] ~R /\ [ <. z , w >. ] ~R . ] ~R ) -> [ <. x , y >. ] ~R . ] ~R ) )
77 76 ad2ant2l 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( v e. P. /\ u e. P. ) ) -> ( ( [ <. x , y >. ] ~R . ] ~R /\ [ <. z , w >. ] ~R . ] ~R ) -> [ <. x , y >. ] ~R . ] ~R ) )
78 77 3adant2 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) /\ ( v e. P. /\ u e. P. ) ) -> ( ( [ <. x , y >. ] ~R . ] ~R /\ [ <. z , w >. ] ~R . ] ~R ) -> [ <. x , y >. ] ~R . ] ~R ) )
79 1 36 39 43 78 3ecoptocl 
 |-  ( ( f e. R. /\ g e. R. /\ h e. R. ) -> ( ( f  f
80 33 79 isso2i 
 |-