Metamath Proof Explorer

Theorem ltgov

Description: Strict "shorter than" geometric relation between segments. (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 ltgov 
|- ( 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 8 breqi 
 |-  ( ( A .- B ) .< ( C .- D ) <-> ( A .- B ) ( ( .<_ |` E ) \ _I ) ( C .- D ) )
13 brdif 
 |-  ( ( A .- B ) ( ( .<_ |` E ) \ _I ) ( C .- D ) <-> ( ( A .- B ) ( .<_ |` E ) ( C .- D ) /\ -. ( A .- B ) _I ( C .- D ) ) )
14 12 13 bitri 
 |-  ( ( A .- B ) .< ( C .- D ) <-> ( ( A .- B ) ( .<_ |` E ) ( C .- D ) /\ -. ( A .- B ) _I ( C .- D ) ) )
15 ovex 
 |-  ( C .- D ) e. _V
16 15 brresi 
 |-  ( ( A .- B ) ( .<_ |` E ) ( C .- D ) <-> ( ( A .- B ) e. E /\ ( A .- B ) .<_ ( C .- D ) ) )
17 16 anbi1i 
 |-  ( ( ( A .- B ) ( .<_ |` E ) ( C .- D ) /\ -. ( A .- B ) _I ( C .- D ) ) <-> ( ( ( A .- B ) e. E /\ ( A .- B ) .<_ ( C .- D ) ) /\ -. ( A .- B ) _I ( C .- D ) ) )
18 an21 
 |-  ( ( ( ( A .- B ) e. E /\ ( A .- B ) .<_ ( C .- D ) ) /\ -. ( A .- B ) _I ( C .- D ) ) <-> ( ( A .- B ) .<_ ( C .- D ) /\ ( ( A .- B ) e. E /\ -. ( A .- B ) _I ( C .- D ) ) ) )
19 14 17 18 3bitri 
 |-  ( ( A .- B ) .< ( C .- D ) <-> ( ( A .- B ) .<_ ( C .- D ) /\ ( ( A .- B ) e. E /\ -. ( A .- B ) _I ( C .- D ) ) ) )
20 10 11 7 9 elovimad 
 |-  ( ph -> ( A .- B ) e. ( .- " ( P X. P ) ) )
21 20 6 eleqtrrdi 
 |-  ( ph -> ( A .- B ) e. E )
22 21 biantrurd 
 |-  ( ph -> ( -. ( A .- B ) _I ( C .- D ) <-> ( ( A .- B ) e. E /\ -. ( A .- B ) _I ( C .- D ) ) ) )
23 15 ideq 
 |-  ( ( A .- B ) _I ( C .- D ) <-> ( A .- B ) = ( C .- D ) )
24 23 necon3bbii 
 |-  ( -. ( A .- B ) _I ( C .- D ) <-> ( A .- B ) =/= ( C .- D ) )
25 22 24 bitr3di 
 |-  ( ph -> ( ( ( A .- B ) e. E /\ -. ( A .- B ) _I ( C .- D ) ) <-> ( A .- B ) =/= ( C .- D ) ) )
26 25 anbi2d 
 |-  ( ph -> ( ( ( A .- B ) .<_ ( C .- D ) /\ ( ( A .- B ) e. E /\ -. ( A .- B ) _I ( C .- D ) ) ) <-> ( ( A .- B ) .<_ ( C .- D ) /\ ( A .- B ) =/= ( C .- D ) ) ) )
27 19 26 syl5bb 
 |-  ( ph -> ( ( A .- B ) .< ( C .- D ) <-> ( ( A .- B ) .<_ ( C .- D ) /\ ( A .- B ) =/= ( C .- D ) ) ) )