Metamath Proof Explorer

Theorem tgifscgr

Description: Inner five segment congruence. Take two triangles, A D C and E H K , with B between A and C and F between E and K . If the other components of the triangles are congruent, then so are B D and F H . Theorem 4.2 of Schwabhauser p. 34. (Contributed by Thierry Arnoux, 24-Mar-2019)

Ref Expression
Hypotheses tgbtwncgr.p 
|- P = ( Base ` G )
tgbtwncgr.m 
|- .- = ( dist ` G )
tgbtwncgr.i 
|- I = ( Itv ` G )
tgbtwncgr.g 
|- ( ph -> G e. TarskiG )
tgbtwncgr.a 
|- ( ph -> A e. P )
tgbtwncgr.b 
|- ( ph -> B e. P )
tgbtwncgr.c 
|- ( ph -> C e. P )
tgbtwncgr.d 
|- ( ph -> D e. P )
tgifscgr.e 
|- ( ph -> E e. P )
tgifscgr.f 
|- ( ph -> F e. P )
tgifscgr.g 
|- ( ph -> K e. P )
tgifscgr.h 
|- ( ph -> H e. P )
tgifscgr.1 
|- ( ph -> B e. ( A I C ) )
tgifscgr.2 
|- ( ph -> F e. ( E I K ) )
tgifscgr.3 
|- ( ph -> ( A .- C ) = ( E .- K ) )
tgifscgr.4 
|- ( ph -> ( B .- C ) = ( F .- K ) )
tgifscgr.5 
|- ( ph -> ( A .- D ) = ( E .- H ) )
tgifscgr.6 
|- ( ph -> ( C .- D ) = ( K .- H ) )
Assertion tgifscgr 
|- ( ph -> ( B .- D ) = ( F .- H ) )

Proof

Step Hyp Ref Expression
1 tgbtwncgr.p 
 |-  P = ( Base ` G )
2 tgbtwncgr.m 
 |-  .- = ( dist ` G )
3 tgbtwncgr.i 
 |-  I = ( Itv ` G )
4 tgbtwncgr.g 
 |-  ( ph -> G e. TarskiG )
5 tgbtwncgr.a 
 |-  ( ph -> A e. P )
6 tgbtwncgr.b 
 |-  ( ph -> B e. P )
7 tgbtwncgr.c 
 |-  ( ph -> C e. P )
8 tgbtwncgr.d 
 |-  ( ph -> D e. P )
9 tgifscgr.e 
 |-  ( ph -> E e. P )
10 tgifscgr.f 
 |-  ( ph -> F e. P )
11 tgifscgr.g 
 |-  ( ph -> K e. P )
12 tgifscgr.h 
 |-  ( ph -> H e. P )
13 tgifscgr.1 
 |-  ( ph -> B e. ( A I C ) )
14 tgifscgr.2 
 |-  ( ph -> F e. ( E I K ) )
15 tgifscgr.3 
 |-  ( ph -> ( A .- C ) = ( E .- K ) )
16 tgifscgr.4 
 |-  ( ph -> ( B .- C ) = ( F .- K ) )
17 tgifscgr.5 
 |-  ( ph -> ( A .- D ) = ( E .- H ) )
18 tgifscgr.6 
 |-  ( ph -> ( C .- D ) = ( K .- H ) )
19 4 adantr 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> G e. TarskiG )
20 6 adantr 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> B e. P )
21 8 adantr 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> D e. P )
22 10 adantr 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> F e. P )
23 simpr 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> ( # ` P ) = 1 )
24 12 adantr 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> H e. P )
25 1 2 3 19 20 21 22 23 24 tgldim0cgr 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> ( B .- D ) = ( F .- H ) )
26 18 ad2antrr 
 |-  ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A = C ) -> ( C .- D ) = ( K .- H ) )
27 4 ad2antrr 
 |-  ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A = C ) -> G e. TarskiG )
28 7 ad2antrr 
 |-  ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A = C ) -> C e. P )
29 6 ad2antrr 
 |-  ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A = C ) -> B e. P )
30 13 ad2antrr 
 |-  ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A = C ) -> B e. ( A I C ) )
31 simpr 
 |-  ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A = C ) -> A = C )
32 31 oveq1d 
 |-  ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A = C ) -> ( A I C ) = ( C I C ) )
33 30 32 eleqtrd 
 |-  ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A = C ) -> B e. ( C I C ) )
34 1 2 3 27 28 29 33 axtgbtwnid 
 |-  ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A = C ) -> C = B )
35 34 oveq1d 
 |-  ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A = C ) -> ( C .- D ) = ( B .- D ) )
36 11 ad2antrr 
 |-  ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A = C ) -> K e. P )
37 10 ad2antrr 
 |-  ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A = C ) -> F e. P )
38 14 ad2antrr 
 |-  ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A = C ) -> F e. ( E I K ) )
39 9 ad2antrr 
 |-  ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A = C ) -> E e. P )
40 5 ad2antrr 
 |-  ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A = C ) -> A e. P )
41 31 oveq2d 
 |-  ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A = C ) -> ( A .- A ) = ( A .- C ) )
42 15 ad2antrr 
 |-  ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A = C ) -> ( A .- C ) = ( E .- K ) )
43 41 42 eqtr2d 
 |-  ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A = C ) -> ( E .- K ) = ( A .- A ) )
44 1 2 3 27 39 36 40 43 axtgcgrid 
 |-  ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A = C ) -> E = K )
45 44 oveq1d 
 |-  ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A = C ) -> ( E I K ) = ( K I K ) )
46 38 45 eleqtrd 
 |-  ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A = C ) -> F e. ( K I K ) )
47 1 2 3 27 36 37 46 axtgbtwnid 
 |-  ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A = C ) -> K = F )
48 47 oveq1d 
 |-  ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A = C ) -> ( K .- H ) = ( F .- H ) )
49 26 35 48 3eqtr3d 
 |-  ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A = C ) -> ( B .- D ) = ( F .- H ) )
50 4 ad2antrr 
 |-  ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) -> G e. TarskiG )
51 50 ad2antrr 
 |-  ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) -> G e. TarskiG )
52 51 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) /\ f e. P ) /\ ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) ) -> G e. TarskiG )
53 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) /\ f e. P ) /\ ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) ) -> e e. P )
54 7 ad2antrr 
 |-  ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) -> C e. P )
55 54 ad2antrr 
 |-  ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) -> C e. P )
56 55 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) /\ f e. P ) /\ ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) ) -> C e. P )
57 6 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) /\ f e. P ) /\ ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) ) -> B e. P )
58 simplr 
 |-  ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) /\ f e. P ) /\ ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) ) -> f e. P )
59 11 ad4antr 
 |-  ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) -> K e. P )
60 59 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) /\ f e. P ) /\ ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) ) -> K e. P )
61 10 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) /\ f e. P ) /\ ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) ) -> F e. P )
62 8 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) /\ f e. P ) /\ ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) ) -> D e. P )
63 12 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) /\ f e. P ) /\ ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) ) -> H e. P )
64 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) /\ f e. P ) /\ ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) ) -> ( C e. ( A I e ) /\ C =/= e ) )
65 64 simprd 
 |-  ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) /\ f e. P ) /\ ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) ) -> C =/= e )
66 65 necomd 
 |-  ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) /\ f e. P ) /\ ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) ) -> e =/= C )
67 5 ad2antrr 
 |-  ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) -> A e. P )
68 67 ad4antr 
 |-  ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) /\ f e. P ) /\ ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) ) -> A e. P )
69 13 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) /\ f e. P ) /\ ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) ) -> B e. ( A I C ) )
70 64 simpld 
 |-  ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) /\ f e. P ) /\ ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) ) -> C e. ( A I e ) )
71 1 2 3 52 68 57 56 53 69 70 tgbtwnexch3 
 |-  ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) /\ f e. P ) /\ ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) ) -> C e. ( B I e ) )
72 1 2 3 52 57 56 53 71 tgbtwncom 
 |-  ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) /\ f e. P ) /\ ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) ) -> C e. ( e I B ) )
73 9 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) /\ f e. P ) /\ ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) ) -> E e. P )
74 14 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) /\ f e. P ) /\ ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) ) -> F e. ( E I K ) )
75 simprl 
 |-  ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) /\ f e. P ) /\ ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) ) -> K e. ( E I f ) )
76 1 2 3 52 73 61 60 58 74 75 tgbtwnexch3 
 |-  ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) /\ f e. P ) /\ ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) ) -> K e. ( F I f ) )
77 1 2 3 52 61 60 58 76 tgbtwncom 
 |-  ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) /\ f e. P ) /\ ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) ) -> K e. ( f I F ) )
78 simprr 
 |-  ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) /\ f e. P ) /\ ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) ) -> ( K .- f ) = ( C .- e ) )
79 78 eqcomd 
 |-  ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) /\ f e. P ) /\ ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) ) -> ( C .- e ) = ( K .- f ) )
80 1 2 3 52 56 53 60 58 79 tgcgrcomlr 
 |-  ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) /\ f e. P ) /\ ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) ) -> ( e .- C ) = ( f .- K ) )
81 16 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) /\ f e. P ) /\ ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) ) -> ( B .- C ) = ( F .- K ) )
82 1 2 3 52 57 56 61 60 81 tgcgrcomlr 
 |-  ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) /\ f e. P ) /\ ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) ) -> ( C .- B ) = ( K .- F ) )
83 simp-5r 
 |-  ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) /\ f e. P ) /\ ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) ) -> A =/= C )
84 15 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) /\ f e. P ) /\ ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) ) -> ( A .- C ) = ( E .- K ) )
85 17 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) /\ f e. P ) /\ ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) ) -> ( A .- D ) = ( E .- H ) )
86 18 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) /\ f e. P ) /\ ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) ) -> ( C .- D ) = ( K .- H ) )
87 1 2 3 52 68 56 53 73 60 58 62 63 83 70 75 84 79 85 86 axtg5seg 
 |-  ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) /\ f e. P ) /\ ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) ) -> ( e .- D ) = ( f .- H ) )
88 1 2 3 52 53 56 57 58 60 61 62 63 66 72 77 80 82 87 86 axtg5seg 
 |-  ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) /\ f e. P ) /\ ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) ) -> ( B .- D ) = ( F .- H ) )
89 9 ad4antr 
 |-  ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) -> E e. P )
90 simplr 
 |-  ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) -> e e. P )
91 1 2 3 51 89 59 55 90 axtgsegcon 
 |-  ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) -> E. f e. P ( K e. ( E I f ) /\ ( K .- f ) = ( C .- e ) ) )
92 88 91 r19.29a 
 |-  ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) /\ e e. P ) /\ ( C e. ( A I e ) /\ C =/= e ) ) -> ( B .- D ) = ( F .- H ) )
93 simplr 
 |-  ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) -> 2 <_ ( # ` P ) )
94 1 2 3 50 67 54 93 tgbtwndiff 
 |-  ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) -> E. e e. P ( C e. ( A I e ) /\ C =/= e ) )
95 92 94 r19.29a 
 |-  ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ A =/= C ) -> ( B .- D ) = ( F .- H ) )
96 49 95 pm2.61dane 
 |-  ( ( ph /\ 2 <_ ( # ` P ) ) -> ( B .- D ) = ( F .- H ) )
97 1 5 tgldimor 
 |-  ( ph -> ( ( # ` P ) = 1 \/ 2 <_ ( # ` P ) ) )
98 25 96 97 mpjaodan 
 |-  ( ph -> ( B .- D ) = ( F .- H ) )