Metamath Proof Explorer

Theorem legso

Description: The "shorter than" relation induces an order on pairs. Remark 5.13 of Schwabhauser p. 42. (Contributed by Thierry Arnoux, 27-Jun-2019)

Ref Expression
Hypotheses legval.p 
|- P = ( Base ` G )
legval.d 
|- .- = ( dist ` G )
legval.i 
|- I = ( Itv ` G )
legval.l 
|- .<_ = ( leG ` G )
legval.g 
|- ( ph -> G e. TarskiG )
legso.a 
|- E = ( .- " ( P X. P ) )
legso.f 
|- ( ph -> Fun .- )
legso.l 
|- .< = ( ( .<_ |` E ) \ _I )
legso.d 
|- ( ph -> ( P X. P ) C_ dom .- )
Assertion legso 
|- ( ph -> .< Or E )

Proof

Step Hyp Ref Expression
1 legval.p 
 |-  P = ( Base ` G )
2 legval.d 
 |-  .- = ( dist ` G )
3 legval.i 
 |-  I = ( Itv ` G )
4 legval.l 
 |-  .<_ = ( leG ` G )
5 legval.g 
 |-  ( ph -> G e. TarskiG )
6 legso.a 
 |-  E = ( .- " ( P X. P ) )
7 legso.f 
 |-  ( ph -> Fun .- )
8 legso.l 
 |-  .< = ( ( .<_ |` E ) \ _I )
9 legso.d 
 |-  ( ph -> ( P X. P ) C_ dom .- )
10 neirr 
 |-  -. ( x .- y ) =/= ( x .- y )
11 10 intnan 
 |-  -. ( ( x .- y ) .<_ ( x .- y ) /\ ( x .- y ) =/= ( x .- y ) )
12 5 adantr 
 |-  ( ( ph /\ a e. E ) -> G e. TarskiG )
13 12 ad3antrrr 
 |-  ( ( ( ( ( ph /\ a e. E ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) -> G e. TarskiG )
14 7 adantr 
 |-  ( ( ph /\ a e. E ) -> Fun .- )
15 14 ad3antrrr 
 |-  ( ( ( ( ( ph /\ a e. E ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) -> Fun .- )
16 9 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. E ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) -> ( P X. P ) C_ dom .- )
17 simpllr 
 |-  ( ( ( ( ( ph /\ a e. E ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) -> x e. P )
18 simplr 
 |-  ( ( ( ( ( ph /\ a e. E ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) -> y e. P )
19 1 2 3 4 13 6 15 8 16 17 18 ltgov 
 |-  ( ( ( ( ( ph /\ a e. E ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) -> ( ( x .- y ) .< ( x .- y ) <-> ( ( x .- y ) .<_ ( x .- y ) /\ ( x .- y ) =/= ( x .- y ) ) ) )
20 11 19 mtbiri 
 |-  ( ( ( ( ( ph /\ a e. E ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) -> -. ( x .- y ) .< ( x .- y ) )
21 simpr 
 |-  ( ( ( ( ( ph /\ a e. E ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) -> a = ( x .- y ) )
22 21 21 breq12d 
 |-  ( ( ( ( ( ph /\ a e. E ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) -> ( a .< a <-> ( x .- y ) .< ( x .- y ) ) )
23 20 22 mtbird 
 |-  ( ( ( ( ( ph /\ a e. E ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) -> -. a .< a )
24 simpr 
 |-  ( ( ph /\ a e. E ) -> a e. E )
25 1 2 3 4 12 6 14 24 ltgseg 
 |-  ( ( ph /\ a e. E ) -> E. x e. P E. y e. P a = ( x .- y ) )
26 23 25 r19.29vva 
 |-  ( ( ph /\ a e. E ) -> -. a .< a )
27 5 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) -> G e. TarskiG )
28 27 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) -> G e. TarskiG )
29 simp-9r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) -> x e. P )
30 simp-8r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) -> y e. P )
31 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) -> z e. P )
32 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) -> t e. P )
33 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) -> u e. P )
34 simplr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) -> v e. P )
35 simp-10r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) -> ( a .< b /\ b .< c ) )
36 35 simpld 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) -> a .< b )
37 simp-7r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) -> a = ( x .- y ) )
38 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) -> b = ( z .- t ) )
39 36 37 38 3brtr3d 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) -> ( x .- y ) .< ( z .- t ) )
40 7 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) -> Fun .- )
41 40 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) -> Fun .- )
42 9 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) -> ( P X. P ) C_ dom .- )
43 42 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) -> ( P X. P ) C_ dom .- )
44 1 2 3 4 28 6 41 8 43 29 30 ltgov 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) -> ( ( x .- y ) .< ( z .- t ) <-> ( ( x .- y ) .<_ ( z .- t ) /\ ( x .- y ) =/= ( z .- t ) ) ) )
45 39 44 mpbid 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) -> ( ( x .- y ) .<_ ( z .- t ) /\ ( x .- y ) =/= ( z .- t ) ) )
46 45 simpld 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) -> ( x .- y ) .<_ ( z .- t ) )
47 35 simprd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) -> b .< c )
48 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) -> c = ( u .- v ) )
49 47 38 48 3brtr3d 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) -> ( z .- t ) .< ( u .- v ) )
50 1 2 3 4 28 6 41 8 43 31 32 ltgov 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) -> ( ( z .- t ) .< ( u .- v ) <-> ( ( z .- t ) .<_ ( u .- v ) /\ ( z .- t ) =/= ( u .- v ) ) ) )
51 49 50 mpbid 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) -> ( ( z .- t ) .<_ ( u .- v ) /\ ( z .- t ) =/= ( u .- v ) ) )
52 51 simpld 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) -> ( z .- t ) .<_ ( u .- v ) )
53 1 2 3 4 28 29 30 31 32 33 34 46 52 legtrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) -> ( x .- y ) .<_ ( u .- v ) )
54 28 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) /\ ( x .- y ) = ( u .- v ) ) -> G e. TarskiG )
55 29 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) /\ ( x .- y ) = ( u .- v ) ) -> x e. P )
56 30 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) /\ ( x .- y ) = ( u .- v ) ) -> y e. P )
57 31 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) /\ ( x .- y ) = ( u .- v ) ) -> z e. P )
58 32 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) /\ ( x .- y ) = ( u .- v ) ) -> t e. P )
59 46 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) /\ ( x .- y ) = ( u .- v ) ) -> ( x .- y ) .<_ ( z .- t ) )
60 52 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) /\ ( x .- y ) = ( u .- v ) ) -> ( z .- t ) .<_ ( u .- v ) )
61 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) /\ ( x .- y ) = ( u .- v ) ) -> ( x .- y ) = ( u .- v ) )
62 60 61 breqtrrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) /\ ( x .- y ) = ( u .- v ) ) -> ( z .- t ) .<_ ( x .- y ) )
63 1 2 3 4 54 55 56 57 58 59 62 legtri3 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) /\ ( x .- y ) = ( u .- v ) ) -> ( x .- y ) = ( z .- t ) )
64 45 simprd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) -> ( x .- y ) =/= ( z .- t ) )
65 64 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) /\ ( x .- y ) = ( u .- v ) ) -> ( x .- y ) =/= ( z .- t ) )
66 65 neneqd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) /\ ( x .- y ) = ( u .- v ) ) -> -. ( x .- y ) = ( z .- t ) )
67 63 66 pm2.65da 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) -> -. ( x .- y ) = ( u .- v ) )
68 67 neqned 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) -> ( x .- y ) =/= ( u .- v ) )
69 1 2 3 4 28 6 41 8 43 29 30 ltgov 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) -> ( ( x .- y ) .< ( u .- v ) <-> ( ( x .- y ) .<_ ( u .- v ) /\ ( x .- y ) =/= ( u .- v ) ) ) )
70 53 68 69 mpbir2and 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) -> ( x .- y ) .< ( u .- v ) )
71 70 37 48 3brtr4d 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) /\ u e. P ) /\ v e. P ) /\ c = ( u .- v ) ) -> a .< c )
72 simp-5r 
 |-  ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) -> ( a e. E /\ b e. E /\ c e. E ) )
73 72 simp3d 
 |-  ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) -> c e. E )
74 73 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) -> c e. E )
75 1 2 3 4 27 6 40 74 ltgseg 
 |-  ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) -> E. u e. P E. v e. P c = ( u .- v ) )
76 71 75 r19.29vva 
 |-  ( ( ( ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) -> a .< c )
77 5 ad5antr 
 |-  ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) -> G e. TarskiG )
78 7 ad5antr 
 |-  ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) -> Fun .- )
79 72 simp2d 
 |-  ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) -> b e. E )
80 1 2 3 4 77 6 78 79 ltgseg 
 |-  ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) -> E. z e. P E. t e. P b = ( z .- t ) )
81 76 80 r19.29vva 
 |-  ( ( ( ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) -> a .< c )
82 5 ad2antrr 
 |-  ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) -> G e. TarskiG )
83 7 ad2antrr 
 |-  ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) -> Fun .- )
84 simplr1 
 |-  ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) -> a e. E )
85 1 2 3 4 82 6 83 84 ltgseg 
 |-  ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) -> E. x e. P E. y e. P a = ( x .- y ) )
86 81 85 r19.29vva 
 |-  ( ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) /\ ( a .< b /\ b .< c ) ) -> a .< c )
87 86 ex 
 |-  ( ( ph /\ ( a e. E /\ b e. E /\ c e. E ) ) -> ( ( a .< b /\ b .< c ) -> a .< c ) )
88 26 87 ispod 
 |-  ( ph -> .< Po E )
89 5 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. E ) /\ b e. E ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) -> G e. TarskiG )
90 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. E ) /\ b e. E ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) -> x e. P )
91 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. E ) /\ b e. E ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) -> y e. P )
92 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. E ) /\ b e. E ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) -> z e. P )
93 simplr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. E ) /\ b e. E ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) -> t e. P )
94 1 2 3 4 89 90 91 92 93 legtrid 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. E ) /\ b e. E ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) -> ( ( x .- y ) .<_ ( z .- t ) \/ ( z .- t ) .<_ ( x .- y ) ) )
95 7 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. E ) /\ b e. E ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) -> Fun .- )
96 9 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. E ) /\ b e. E ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) -> ( P X. P ) C_ dom .- )
97 1 2 3 4 89 6 95 8 96 90 91 legov3 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. E ) /\ b e. E ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) -> ( ( x .- y ) .<_ ( z .- t ) <-> ( ( x .- y ) .< ( z .- t ) \/ ( x .- y ) = ( z .- t ) ) ) )
98 1 2 3 4 89 6 95 8 96 92 93 legov3 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. E ) /\ b e. E ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) -> ( ( z .- t ) .<_ ( x .- y ) <-> ( ( z .- t ) .< ( x .- y ) \/ ( z .- t ) = ( x .- y ) ) ) )
99 97 98 orbi12d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. E ) /\ b e. E ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) -> ( ( ( x .- y ) .<_ ( z .- t ) \/ ( z .- t ) .<_ ( x .- y ) ) <-> ( ( ( x .- y ) .< ( z .- t ) \/ ( x .- y ) = ( z .- t ) ) \/ ( ( z .- t ) .< ( x .- y ) \/ ( z .- t ) = ( x .- y ) ) ) ) )
100 94 99 mpbid 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. E ) /\ b e. E ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) -> ( ( ( x .- y ) .< ( z .- t ) \/ ( x .- y ) = ( z .- t ) ) \/ ( ( z .- t ) .< ( x .- y ) \/ ( z .- t ) = ( x .- y ) ) ) )
101 eqcom 
 |-  ( ( x .- y ) = ( z .- t ) <-> ( z .- t ) = ( x .- y ) )
102 101 orbi2i 
 |-  ( ( ( z .- t ) .< ( x .- y ) \/ ( x .- y ) = ( z .- t ) ) <-> ( ( z .- t ) .< ( x .- y ) \/ ( z .- t ) = ( x .- y ) ) )
103 102 orbi2i 
 |-  ( ( ( ( x .- y ) .< ( z .- t ) \/ ( x .- y ) = ( z .- t ) ) \/ ( ( z .- t ) .< ( x .- y ) \/ ( x .- y ) = ( z .- t ) ) ) <-> ( ( ( x .- y ) .< ( z .- t ) \/ ( x .- y ) = ( z .- t ) ) \/ ( ( z .- t ) .< ( x .- y ) \/ ( z .- t ) = ( x .- y ) ) ) )
104 df-3or 
 |-  ( ( ( x .- y ) .< ( z .- t ) \/ ( z .- t ) .< ( x .- y ) \/ ( x .- y ) = ( z .- t ) ) <-> ( ( ( x .- y ) .< ( z .- t ) \/ ( z .- t ) .< ( x .- y ) ) \/ ( x .- y ) = ( z .- t ) ) )
105 3orcomb 
 |-  ( ( ( x .- y ) .< ( z .- t ) \/ ( z .- t ) .< ( x .- y ) \/ ( x .- y ) = ( z .- t ) ) <-> ( ( x .- y ) .< ( z .- t ) \/ ( x .- y ) = ( z .- t ) \/ ( z .- t ) .< ( x .- y ) ) )
106 orordir 
 |-  ( ( ( ( x .- y ) .< ( z .- t ) \/ ( z .- t ) .< ( x .- y ) ) \/ ( x .- y ) = ( z .- t ) ) <-> ( ( ( x .- y ) .< ( z .- t ) \/ ( x .- y ) = ( z .- t ) ) \/ ( ( z .- t ) .< ( x .- y ) \/ ( x .- y ) = ( z .- t ) ) ) )
107 104 105 106 3bitr3ri 
 |-  ( ( ( ( x .- y ) .< ( z .- t ) \/ ( x .- y ) = ( z .- t ) ) \/ ( ( z .- t ) .< ( x .- y ) \/ ( x .- y ) = ( z .- t ) ) ) <-> ( ( x .- y ) .< ( z .- t ) \/ ( x .- y ) = ( z .- t ) \/ ( z .- t ) .< ( x .- y ) ) )
108 103 107 bitr3i 
 |-  ( ( ( ( x .- y ) .< ( z .- t ) \/ ( x .- y ) = ( z .- t ) ) \/ ( ( z .- t ) .< ( x .- y ) \/ ( z .- t ) = ( x .- y ) ) ) <-> ( ( x .- y ) .< ( z .- t ) \/ ( x .- y ) = ( z .- t ) \/ ( z .- t ) .< ( x .- y ) ) )
109 100 108 sylib 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. E ) /\ b e. E ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) -> ( ( x .- y ) .< ( z .- t ) \/ ( x .- y ) = ( z .- t ) \/ ( z .- t ) .< ( x .- y ) ) )
110 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. E ) /\ b e. E ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) -> a = ( x .- y ) )
111 simpr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. E ) /\ b e. E ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) -> b = ( z .- t ) )
112 110 111 breq12d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. E ) /\ b e. E ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) -> ( a .< b <-> ( x .- y ) .< ( z .- t ) ) )
113 110 111 eqeq12d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. E ) /\ b e. E ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) -> ( a = b <-> ( x .- y ) = ( z .- t ) ) )
114 111 110 breq12d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. E ) /\ b e. E ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) -> ( b .< a <-> ( z .- t ) .< ( x .- y ) ) )
115 112 113 114 3orbi123d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. E ) /\ b e. E ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) -> ( ( a .< b \/ a = b \/ b .< a ) <-> ( ( x .- y ) .< ( z .- t ) \/ ( x .- y ) = ( z .- t ) \/ ( z .- t ) .< ( x .- y ) ) ) )
116 109 115 mpbird 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. E ) /\ b e. E ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) /\ z e. P ) /\ t e. P ) /\ b = ( z .- t ) ) -> ( a .< b \/ a = b \/ b .< a ) )
117 5 ad2antrr 
 |-  ( ( ( ph /\ a e. E ) /\ b e. E ) -> G e. TarskiG )
118 7 ad2antrr 
 |-  ( ( ( ph /\ a e. E ) /\ b e. E ) -> Fun .- )
119 simpr 
 |-  ( ( ( ph /\ a e. E ) /\ b e. E ) -> b e. E )
120 1 2 3 4 117 6 118 119 ltgseg 
 |-  ( ( ( ph /\ a e. E ) /\ b e. E ) -> E. z e. P E. t e. P b = ( z .- t ) )
121 120 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ a e. E ) /\ b e. E ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) -> E. z e. P E. t e. P b = ( z .- t ) )
122 116 121 r19.29vva 
 |-  ( ( ( ( ( ( ph /\ a e. E ) /\ b e. E ) /\ x e. P ) /\ y e. P ) /\ a = ( x .- y ) ) -> ( a .< b \/ a = b \/ b .< a ) )
123 25 adantr 
 |-  ( ( ( ph /\ a e. E ) /\ b e. E ) -> E. x e. P E. y e. P a = ( x .- y ) )
124 122 123 r19.29vva 
 |-  ( ( ( ph /\ a e. E ) /\ b e. E ) -> ( a .< b \/ a = b \/ b .< a ) )
125 124 anasss 
 |-  ( ( ph /\ ( a e. E /\ b e. E ) ) -> ( a .< b \/ a = b \/ b .< a ) )
126 88 125 issod 
 |-  ( ph -> .< Or E )