Metamath Proof Explorer

Theorem legov3

Description: An equivalent definition of the less-than relationship, from the strict relation. (Contributed by Thierry Arnoux, 15-Dec-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 .- )
ltgov.a 
|- ( ph -> A e. P )
ltgov.b 
|- ( ph -> B e. P )
Assertion legov3 
|- ( ph -> ( ( A .- B ) .<_ ( C .- D ) <-> ( ( A .- B ) .< ( C .- D ) \/ ( A .- B ) = ( C .- D ) ) ) )

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 ltgov.a 
 |-  ( ph -> A e. P )
11 ltgov.b 
 |-  ( ph -> B e. P )
12 1 2 3 4 5 6 7 8 9 10 11 ltgov 
 |-  ( ph -> ( ( A .- B ) .< ( C .- D ) <-> ( ( A .- B ) .<_ ( C .- D ) /\ ( A .- B ) =/= ( C .- D ) ) ) )
13 12 orbi1d 
 |-  ( ph -> ( ( ( A .- B ) .< ( C .- D ) \/ ( A .- B ) = ( C .- D ) ) <-> ( ( ( A .- B ) .<_ ( C .- D ) /\ ( A .- B ) =/= ( C .- D ) ) \/ ( A .- B ) = ( C .- D ) ) ) )
14 simprl 
 |-  ( ( ( ph /\ ( ( ( A .- B ) .<_ ( C .- D ) /\ ( A .- B ) =/= ( C .- D ) ) \/ ( A .- B ) = ( C .- D ) ) ) /\ ( ( A .- B ) .<_ ( C .- D ) /\ ( A .- B ) =/= ( C .- D ) ) ) -> ( A .- B ) .<_ ( C .- D ) )
15 1 2 3 4 5 10 11 legid 
 |-  ( ph -> ( A .- B ) .<_ ( A .- B ) )
16 15 adantr 
 |-  ( ( ph /\ ( A .- B ) = ( C .- D ) ) -> ( A .- B ) .<_ ( A .- B ) )
17 simpr 
 |-  ( ( ph /\ ( A .- B ) = ( C .- D ) ) -> ( A .- B ) = ( C .- D ) )
18 16 17 breqtrd 
 |-  ( ( ph /\ ( A .- B ) = ( C .- D ) ) -> ( A .- B ) .<_ ( C .- D ) )
19 18 adantlr 
 |-  ( ( ( ph /\ ( ( ( A .- B ) .<_ ( C .- D ) /\ ( A .- B ) =/= ( C .- D ) ) \/ ( A .- B ) = ( C .- D ) ) ) /\ ( A .- B ) = ( C .- D ) ) -> ( A .- B ) .<_ ( C .- D ) )
20 simpr 
 |-  ( ( ph /\ ( ( ( A .- B ) .<_ ( C .- D ) /\ ( A .- B ) =/= ( C .- D ) ) \/ ( A .- B ) = ( C .- D ) ) ) -> ( ( ( A .- B ) .<_ ( C .- D ) /\ ( A .- B ) =/= ( C .- D ) ) \/ ( A .- B ) = ( C .- D ) ) )
21 14 19 20 mpjaodan 
 |-  ( ( ph /\ ( ( ( A .- B ) .<_ ( C .- D ) /\ ( A .- B ) =/= ( C .- D ) ) \/ ( A .- B ) = ( C .- D ) ) ) -> ( A .- B ) .<_ ( C .- D ) )
22 simplr 
 |-  ( ( ( ph /\ ( A .- B ) .<_ ( C .- D ) ) /\ -. ( A .- B ) = ( C .- D ) ) -> ( A .- B ) .<_ ( C .- D ) )
23 simpr 
 |-  ( ( ( ph /\ ( A .- B ) .<_ ( C .- D ) ) /\ -. ( A .- B ) = ( C .- D ) ) -> -. ( A .- B ) = ( C .- D ) )
24 23 neqned 
 |-  ( ( ( ph /\ ( A .- B ) .<_ ( C .- D ) ) /\ -. ( A .- B ) = ( C .- D ) ) -> ( A .- B ) =/= ( C .- D ) )
25 22 24 jca 
 |-  ( ( ( ph /\ ( A .- B ) .<_ ( C .- D ) ) /\ -. ( A .- B ) = ( C .- D ) ) -> ( ( A .- B ) .<_ ( C .- D ) /\ ( A .- B ) =/= ( C .- D ) ) )
26 25 ex 
 |-  ( ( ph /\ ( A .- B ) .<_ ( C .- D ) ) -> ( -. ( A .- B ) = ( C .- D ) -> ( ( A .- B ) .<_ ( C .- D ) /\ ( A .- B ) =/= ( C .- D ) ) ) )
27 26 orrd 
 |-  ( ( ph /\ ( A .- B ) .<_ ( C .- D ) ) -> ( ( A .- B ) = ( C .- D ) \/ ( ( A .- B ) .<_ ( C .- D ) /\ ( A .- B ) =/= ( C .- D ) ) ) )
28 27 orcomd 
 |-  ( ( ph /\ ( A .- B ) .<_ ( C .- D ) ) -> ( ( ( A .- B ) .<_ ( C .- D ) /\ ( A .- B ) =/= ( C .- D ) ) \/ ( A .- B ) = ( C .- D ) ) )
29 21 28 impbida 
 |-  ( ph -> ( ( ( ( A .- B ) .<_ ( C .- D ) /\ ( A .- B ) =/= ( C .- D ) ) \/ ( A .- B ) = ( C .- D ) ) <-> ( A .- B ) .<_ ( C .- D ) ) )
30 13 29 bitr2d 
 |-  ( ph -> ( ( A .- B ) .<_ ( C .- D ) <-> ( ( A .- B ) .< ( C .- D ) \/ ( A .- B ) = ( C .- D ) ) ) )