Metamath Proof Explorer

Theorem tgcgrsub2

Description: Removing identical parts from the end of a line segment preserves congruence. In this version the order of points is not known. (Contributed by Thierry Arnoux, 3-Apr-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 )
tgcgrsub2.d 
|- ( ph -> D e. P )
tgcgrsub2.e 
|- ( ph -> E e. P )
tgcgrsub2.f 
|- ( ph -> F e. P )
tgcgrsub2.1 
|- ( ph -> ( B e. ( A I C ) \/ C e. ( A I B ) ) )
tgcgrsub2.2 
|- ( ph -> ( E e. ( D I F ) \/ F e. ( D I E ) ) )
tgcgrsub2.3 
|- ( ph -> ( A .- B ) = ( D .- E ) )
tgcgrsub2.4 
|- ( ph -> ( A .- C ) = ( D .- F ) )
Assertion tgcgrsub2 
|- ( ph -> ( B .- C ) = ( E .- F ) )

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 tgcgrsub2.d 
 |-  ( ph -> D e. P )
11 tgcgrsub2.e 
 |-  ( ph -> E e. P )
12 tgcgrsub2.f 
 |-  ( ph -> F e. P )
13 tgcgrsub2.1 
 |-  ( ph -> ( B e. ( A I C ) \/ C e. ( A I B ) ) )
14 tgcgrsub2.2 
 |-  ( ph -> ( E e. ( D I F ) \/ F e. ( D I E ) ) )
15 tgcgrsub2.3 
 |-  ( ph -> ( A .- B ) = ( D .- E ) )
16 tgcgrsub2.4 
 |-  ( ph -> ( A .- C ) = ( D .- F ) )
17 5 adantr 
 |-  ( ( ph /\ B e. ( A I C ) ) -> G e. TarskiG )
18 8 adantr 
 |-  ( ( ph /\ B e. ( A I C ) ) -> C e. P )
19 7 adantr 
 |-  ( ( ph /\ B e. ( A I C ) ) -> B e. P )
20 12 adantr 
 |-  ( ( ph /\ B e. ( A I C ) ) -> F e. P )
21 11 adantr 
 |-  ( ( ph /\ B e. ( A I C ) ) -> E e. P )
22 6 adantr 
 |-  ( ( ph /\ B e. ( A I C ) ) -> A e. P )
23 9 adantr 
 |-  ( ( ph /\ B e. ( A I C ) ) -> D e. P )
24 simpr 
 |-  ( ( ph /\ B e. ( A I C ) ) -> B e. ( A I C ) )
25 1 2 3 17 22 19 18 24 tgbtwncom 
 |-  ( ( ph /\ B e. ( A I C ) ) -> B e. ( C I A ) )
26 14 adantr 
 |-  ( ( ph /\ B e. ( A I C ) ) -> ( E e. ( D I F ) \/ F e. ( D I E ) ) )
27 1 2 3 4 17 22 19 18 24 btwnleg 
 |-  ( ( ph /\ B e. ( A I C ) ) -> ( A .- B ) .<_ ( A .- C ) )
28 15 adantr 
 |-  ( ( ph /\ B e. ( A I C ) ) -> ( A .- B ) = ( D .- E ) )
29 16 adantr 
 |-  ( ( ph /\ B e. ( A I C ) ) -> ( A .- C ) = ( D .- F ) )
30 27 28 29 3brtr3d 
 |-  ( ( ph /\ B e. ( A I C ) ) -> ( D .- E ) .<_ ( D .- F ) )
31 1 2 3 4 17 21 20 23 23 26 30 legbtwn 
 |-  ( ( ph /\ B e. ( A I C ) ) -> E e. ( D I F ) )
32 1 2 3 17 23 21 20 31 tgbtwncom 
 |-  ( ( ph /\ B e. ( A I C ) ) -> E e. ( F I D ) )
33 1 2 3 5 6 8 9 12 16 tgcgrcomlr 
 |-  ( ph -> ( C .- A ) = ( F .- D ) )
34 33 adantr 
 |-  ( ( ph /\ B e. ( A I C ) ) -> ( C .- A ) = ( F .- D ) )
35 1 2 3 5 6 7 9 11 15 tgcgrcomlr 
 |-  ( ph -> ( B .- A ) = ( E .- D ) )
36 35 adantr 
 |-  ( ( ph /\ B e. ( A I C ) ) -> ( B .- A ) = ( E .- D ) )
37 1 2 3 17 18 19 22 20 21 23 25 32 34 36 tgcgrsub 
 |-  ( ( ph /\ B e. ( A I C ) ) -> ( C .- B ) = ( F .- E ) )
38 1 2 3 17 18 19 20 21 37 tgcgrcomlr 
 |-  ( ( ph /\ B e. ( A I C ) ) -> ( B .- C ) = ( E .- F ) )
39 5 adantr 
 |-  ( ( ph /\ C e. ( A I B ) ) -> G e. TarskiG )
40 7 adantr 
 |-  ( ( ph /\ C e. ( A I B ) ) -> B e. P )
41 8 adantr 
 |-  ( ( ph /\ C e. ( A I B ) ) -> C e. P )
42 6 adantr 
 |-  ( ( ph /\ C e. ( A I B ) ) -> A e. P )
43 11 adantr 
 |-  ( ( ph /\ C e. ( A I B ) ) -> E e. P )
44 12 adantr 
 |-  ( ( ph /\ C e. ( A I B ) ) -> F e. P )
45 9 adantr 
 |-  ( ( ph /\ C e. ( A I B ) ) -> D e. P )
46 simpr 
 |-  ( ( ph /\ C e. ( A I B ) ) -> C e. ( A I B ) )
47 1 2 3 39 42 41 40 46 tgbtwncom 
 |-  ( ( ph /\ C e. ( A I B ) ) -> C e. ( B I A ) )
48 14 orcomd 
 |-  ( ph -> ( F e. ( D I E ) \/ E e. ( D I F ) ) )
49 48 adantr 
 |-  ( ( ph /\ C e. ( A I B ) ) -> ( F e. ( D I E ) \/ E e. ( D I F ) ) )
50 1 2 3 4 39 42 41 40 46 btwnleg 
 |-  ( ( ph /\ C e. ( A I B ) ) -> ( A .- C ) .<_ ( A .- B ) )
51 16 adantr 
 |-  ( ( ph /\ C e. ( A I B ) ) -> ( A .- C ) = ( D .- F ) )
52 15 adantr 
 |-  ( ( ph /\ C e. ( A I B ) ) -> ( A .- B ) = ( D .- E ) )
53 50 51 52 3brtr3d 
 |-  ( ( ph /\ C e. ( A I B ) ) -> ( D .- F ) .<_ ( D .- E ) )
54 1 2 3 4 39 44 43 45 45 49 53 legbtwn 
 |-  ( ( ph /\ C e. ( A I B ) ) -> F e. ( D I E ) )
55 1 2 3 39 45 44 43 54 tgbtwncom 
 |-  ( ( ph /\ C e. ( A I B ) ) -> F e. ( E I D ) )
56 35 adantr 
 |-  ( ( ph /\ C e. ( A I B ) ) -> ( B .- A ) = ( E .- D ) )
57 33 adantr 
 |-  ( ( ph /\ C e. ( A I B ) ) -> ( C .- A ) = ( F .- D ) )
58 1 2 3 39 40 41 42 43 44 45 47 55 56 57 tgcgrsub 
 |-  ( ( ph /\ C e. ( A I B ) ) -> ( B .- C ) = ( E .- F ) )
59 38 58 13 mpjaodan 
 |-  ( ph -> ( B .- C ) = ( E .- F ) )