Metamath Proof Explorer

Theorem legtri3

Description: Equality from the less-than relationship. Proposition 5.9 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 )
legid.a 
|- ( ph -> A e. P )
legid.b 
|- ( ph -> B e. P )
legtrd.c 
|- ( ph -> C e. P )
legtrd.d 
|- ( ph -> D e. P )
legtri3.1 
|- ( ph -> ( A .- B ) .<_ ( C .- D ) )
legtri3.2 
|- ( ph -> ( C .- D ) .<_ ( A .- B ) )
Assertion legtri3 
|- ( ph -> ( 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 legid.a 
 |-  ( ph -> A e. P )
7 legid.b 
 |-  ( ph -> B e. P )
8 legtrd.c 
 |-  ( ph -> C e. P )
9 legtrd.d 
 |-  ( ph -> D e. P )
10 legtri3.1 
 |-  ( ph -> ( A .- B ) .<_ ( C .- D ) )
11 legtri3.2 
 |-  ( ph -> ( C .- D ) .<_ ( A .- B ) )
12 simpllr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( D e. ( C I y ) /\ ( C .- y ) = ( A .- B ) ) ) -> ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) )
13 12 simprd 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( D e. ( C I y ) /\ ( C .- y ) = ( A .- B ) ) ) -> ( A .- B ) = ( C .- x ) )
14 5 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( D e. ( C I y ) /\ ( C .- y ) = ( A .- B ) ) ) -> G e. TarskiG )
15 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( D e. ( C I y ) /\ ( C .- y ) = ( A .- B ) ) ) -> x e. P )
16 9 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( D e. ( C I y ) /\ ( C .- y ) = ( A .- B ) ) ) -> D e. P )
17 8 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( D e. ( C I y ) /\ ( C .- y ) = ( A .- B ) ) ) -> C e. P )
18 12 simpld 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( D e. ( C I y ) /\ ( C .- y ) = ( A .- B ) ) ) -> x e. ( C I D ) )
19 1 2 3 14 17 15 16 18 tgbtwncom 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( D e. ( C I y ) /\ ( C .- y ) = ( A .- B ) ) ) -> x e. ( D I C ) )
20 simpr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( D e. ( C I y ) /\ ( C .- y ) = ( A .- B ) ) ) -> ( D e. ( C I y ) /\ ( C .- y ) = ( A .- B ) ) )
21 20 simpld 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( D e. ( C I y ) /\ ( C .- y ) = ( A .- B ) ) ) -> D e. ( C I y ) )
22 simplr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( D e. ( C I y ) /\ ( C .- y ) = ( A .- B ) ) ) -> y e. P )
23 7 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( D e. ( C I y ) /\ ( C .- y ) = ( A .- B ) ) ) -> B e. P )
24 6 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( D e. ( C I y ) /\ ( C .- y ) = ( A .- B ) ) ) -> A e. P )
25 1 2 3 14 17 16 22 21 tgbtwncom 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( D e. ( C I y ) /\ ( C .- y ) = ( A .- B ) ) ) -> D e. ( y I C ) )
26 1 2 3 14 22 16 15 17 25 19 tgbtwnexch2 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( D e. ( C I y ) /\ ( C .- y ) = ( A .- B ) ) ) -> x e. ( y I C ) )
27 1 2 3 14 23 24 tgbtwntriv1 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( D e. ( C I y ) /\ ( C .- y ) = ( A .- B ) ) ) -> B e. ( B I A ) )
28 20 simprd 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( D e. ( C I y ) /\ ( C .- y ) = ( A .- B ) ) ) -> ( C .- y ) = ( A .- B ) )
29 1 2 3 14 17 22 24 23 28 tgcgrcomlr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( D e. ( C I y ) /\ ( C .- y ) = ( A .- B ) ) ) -> ( y .- C ) = ( B .- A ) )
30 13 eqcomd 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( D e. ( C I y ) /\ ( C .- y ) = ( A .- B ) ) ) -> ( C .- x ) = ( A .- B ) )
31 1 2 3 14 17 15 24 23 30 tgcgrcomlr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( D e. ( C I y ) /\ ( C .- y ) = ( A .- B ) ) ) -> ( x .- C ) = ( B .- A ) )
32 1 2 3 14 22 15 17 23 23 24 26 27 29 31 tgcgrsub 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( D e. ( C I y ) /\ ( C .- y ) = ( A .- B ) ) ) -> ( y .- x ) = ( B .- B ) )
33 1 2 3 14 22 15 23 32 axtgcgrid 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( D e. ( C I y ) /\ ( C .- y ) = ( A .- B ) ) ) -> y = x )
34 33 oveq2d 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( D e. ( C I y ) /\ ( C .- y ) = ( A .- B ) ) ) -> ( C I y ) = ( C I x ) )
35 21 34 eleqtrd 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( D e. ( C I y ) /\ ( C .- y ) = ( A .- B ) ) ) -> D e. ( C I x ) )
36 1 2 3 14 17 16 15 35 tgbtwncom 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( D e. ( C I y ) /\ ( C .- y ) = ( A .- B ) ) ) -> D e. ( x I C ) )
37 1 2 3 14 15 16 17 19 36 tgbtwnswapid 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( D e. ( C I y ) /\ ( C .- y ) = ( A .- B ) ) ) -> x = D )
38 37 oveq2d 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( D e. ( C I y ) /\ ( C .- y ) = ( A .- B ) ) ) -> ( C .- x ) = ( C .- D ) )
39 13 38 eqtrd 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( D e. ( C I y ) /\ ( C .- y ) = ( A .- B ) ) ) -> ( A .- B ) = ( C .- D ) )
40 1 2 3 4 5 8 9 6 7 legov2 
 |-  ( ph -> ( ( C .- D ) .<_ ( A .- B ) <-> E. y e. P ( D e. ( C I y ) /\ ( C .- y ) = ( A .- B ) ) ) )
41 11 40 mpbid 
 |-  ( ph -> E. y e. P ( D e. ( C I y ) /\ ( C .- y ) = ( A .- B ) ) )
42 41 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) -> E. y e. P ( D e. ( C I y ) /\ ( C .- y ) = ( A .- B ) ) )
43 39 42 r19.29a 
 |-  ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) -> ( A .- B ) = ( C .- D ) )
44 1 2 3 4 5 6 7 8 9 legov 
 |-  ( ph -> ( ( A .- B ) .<_ ( C .- D ) <-> E. x e. P ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) )
45 10 44 mpbid 
 |-  ( ph -> E. x e. P ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) )
46 43 45 r19.29a 
 |-  ( ph -> ( A .- B ) = ( C .- D ) )