Metamath Proof Explorer

Theorem tgbtwnconn1lem2

Description: Lemma for tgbtwnconn1 . (Contributed by Thierry Arnoux, 30-Apr-2019)

Ref Expression
Hypotheses tgbtwnconn1.p 
|- P = ( Base ` G )
tgbtwnconn1.i 
|- I = ( Itv ` G )
tgbtwnconn1.g 
|- ( ph -> G e. TarskiG )
tgbtwnconn1.a 
|- ( ph -> A e. P )
tgbtwnconn1.b 
|- ( ph -> B e. P )
tgbtwnconn1.c 
|- ( ph -> C e. P )
tgbtwnconn1.d 
|- ( ph -> D e. P )
tgbtwnconn1.1 
|- ( ph -> A =/= B )
tgbtwnconn1.2 
|- ( ph -> B e. ( A I C ) )
tgbtwnconn1.3 
|- ( ph -> B e. ( A I D ) )
tgbtwnconn1.m 
|- .- = ( dist ` G )
tgbtwnconn1.e 
|- ( ph -> E e. P )
tgbtwnconn1.f 
|- ( ph -> F e. P )
tgbtwnconn1.h 
|- ( ph -> H e. P )
tgbtwnconn1.j 
|- ( ph -> J e. P )
tgbtwnconn1.4 
|- ( ph -> D e. ( A I E ) )
tgbtwnconn1.5 
|- ( ph -> C e. ( A I F ) )
tgbtwnconn1.6 
|- ( ph -> E e. ( A I H ) )
tgbtwnconn1.7 
|- ( ph -> F e. ( A I J ) )
tgbtwnconn1.8 
|- ( ph -> ( E .- D ) = ( C .- D ) )
tgbtwnconn1.9 
|- ( ph -> ( C .- F ) = ( C .- D ) )
tgbtwnconn1.10 
|- ( ph -> ( E .- H ) = ( B .- C ) )
tgbtwnconn1.11 
|- ( ph -> ( F .- J ) = ( B .- D ) )
Assertion tgbtwnconn1lem2 
|- ( ph -> ( E .- F ) = ( C .- D ) )

Proof

Step Hyp Ref Expression
1 tgbtwnconn1.p 
 |-  P = ( Base ` G )
2 tgbtwnconn1.i 
 |-  I = ( Itv ` G )
3 tgbtwnconn1.g 
 |-  ( ph -> G e. TarskiG )
4 tgbtwnconn1.a 
 |-  ( ph -> A e. P )
5 tgbtwnconn1.b 
 |-  ( ph -> B e. P )
6 tgbtwnconn1.c 
 |-  ( ph -> C e. P )
7 tgbtwnconn1.d 
 |-  ( ph -> D e. P )
8 tgbtwnconn1.1 
 |-  ( ph -> A =/= B )
9 tgbtwnconn1.2 
 |-  ( ph -> B e. ( A I C ) )
10 tgbtwnconn1.3 
 |-  ( ph -> B e. ( A I D ) )
11 tgbtwnconn1.m 
 |-  .- = ( dist ` G )
12 tgbtwnconn1.e 
 |-  ( ph -> E e. P )
13 tgbtwnconn1.f 
 |-  ( ph -> F e. P )
14 tgbtwnconn1.h 
 |-  ( ph -> H e. P )
15 tgbtwnconn1.j 
 |-  ( ph -> J e. P )
16 tgbtwnconn1.4 
 |-  ( ph -> D e. ( A I E ) )
17 tgbtwnconn1.5 
 |-  ( ph -> C e. ( A I F ) )
18 tgbtwnconn1.6 
 |-  ( ph -> E e. ( A I H ) )
19 tgbtwnconn1.7 
 |-  ( ph -> F e. ( A I J ) )
20 tgbtwnconn1.8 
 |-  ( ph -> ( E .- D ) = ( C .- D ) )
21 tgbtwnconn1.9 
 |-  ( ph -> ( C .- F ) = ( C .- D ) )
22 tgbtwnconn1.10 
 |-  ( ph -> ( E .- H ) = ( B .- C ) )
23 tgbtwnconn1.11 
 |-  ( ph -> ( F .- J ) = ( B .- D ) )
24 1 11 2 3 12 13 axtgcgrrflx 
 |-  ( ph -> ( E .- F ) = ( F .- E ) )
25 24 adantr 
 |-  ( ( ph /\ B = C ) -> ( E .- F ) = ( F .- E ) )
26 3 adantr 
 |-  ( ( ph /\ B = C ) -> G e. TarskiG )
27 12 adantr 
 |-  ( ( ph /\ B = C ) -> E e. P )
28 14 adantr 
 |-  ( ( ph /\ B = C ) -> H e. P )
29 6 adantr 
 |-  ( ( ph /\ B = C ) -> C e. P )
30 22 adantr 
 |-  ( ( ph /\ B = C ) -> ( E .- H ) = ( B .- C ) )
31 simpr 
 |-  ( ( ph /\ B = C ) -> B = C )
32 31 oveq1d 
 |-  ( ( ph /\ B = C ) -> ( B .- C ) = ( C .- C ) )
33 30 32 eqtrd 
 |-  ( ( ph /\ B = C ) -> ( E .- H ) = ( C .- C ) )
34 1 11 2 26 27 28 29 33 axtgcgrid 
 |-  ( ( ph /\ B = C ) -> E = H )
35 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 tgbtwnconn1lem1 
 |-  ( ph -> H = J )
36 35 adantr 
 |-  ( ( ph /\ B = C ) -> H = J )
37 34 36 eqtrd 
 |-  ( ( ph /\ B = C ) -> E = J )
38 37 oveq2d 
 |-  ( ( ph /\ B = C ) -> ( F .- E ) = ( F .- J ) )
39 23 adantr 
 |-  ( ( ph /\ B = C ) -> ( F .- J ) = ( B .- D ) )
40 31 oveq1d 
 |-  ( ( ph /\ B = C ) -> ( B .- D ) = ( C .- D ) )
41 38 39 40 3eqtrd 
 |-  ( ( ph /\ B = C ) -> ( F .- E ) = ( C .- D ) )
42 25 41 eqtrd 
 |-  ( ( ph /\ B = C ) -> ( E .- F ) = ( C .- D ) )
43 3 adantr 
 |-  ( ( ph /\ B =/= C ) -> G e. TarskiG )
44 13 adantr 
 |-  ( ( ph /\ B =/= C ) -> F e. P )
45 12 adantr 
 |-  ( ( ph /\ B =/= C ) -> E e. P )
46 7 adantr 
 |-  ( ( ph /\ B =/= C ) -> D e. P )
47 6 adantr 
 |-  ( ( ph /\ B =/= C ) -> C e. P )
48 5 adantr 
 |-  ( ( ph /\ B =/= C ) -> B e. P )
49 15 adantr 
 |-  ( ( ph /\ B =/= C ) -> J e. P )
50 simpr 
 |-  ( ( ph /\ B =/= C ) -> B =/= C )
51 1 11 2 3 4 5 6 13 9 17 tgbtwnexch3 
 |-  ( ph -> C e. ( B I F ) )
52 51 adantr 
 |-  ( ( ph /\ B =/= C ) -> C e. ( B I F ) )
53 35 oveq2d 
 |-  ( ph -> ( A I H ) = ( A I J ) )
54 18 53 eleqtrd 
 |-  ( ph -> E e. ( A I J ) )
55 1 11 2 3 4 7 12 15 16 54 tgbtwnexch3 
 |-  ( ph -> E e. ( D I J ) )
56 1 11 2 3 7 12 15 55 tgbtwncom 
 |-  ( ph -> E e. ( J I D ) )
57 56 adantr 
 |-  ( ( ph /\ B =/= C ) -> E e. ( J I D ) )
58 35 adantr 
 |-  ( ( ph /\ B =/= C ) -> H = J )
59 58 oveq2d 
 |-  ( ( ph /\ B =/= C ) -> ( E .- H ) = ( E .- J ) )
60 22 adantr 
 |-  ( ( ph /\ B =/= C ) -> ( E .- H ) = ( B .- C ) )
61 1 11 2 43 45 49 axtgcgrrflx 
 |-  ( ( ph /\ B =/= C ) -> ( E .- J ) = ( J .- E ) )
62 59 60 61 3eqtr3d 
 |-  ( ( ph /\ B =/= C ) -> ( B .- C ) = ( J .- E ) )
63 21 20 eqtr4d 
 |-  ( ph -> ( C .- F ) = ( E .- D ) )
64 63 adantr 
 |-  ( ( ph /\ B =/= C ) -> ( C .- F ) = ( E .- D ) )
65 1 11 2 3 4 5 7 12 10 16 tgbtwnexch3 
 |-  ( ph -> D e. ( B I E ) )
66 65 adantr 
 |-  ( ( ph /\ B =/= C ) -> D e. ( B I E ) )
67 1 11 2 3 4 6 13 15 17 19 tgbtwnexch3 
 |-  ( ph -> F e. ( C I J ) )
68 1 11 2 3 6 13 15 67 tgbtwncom 
 |-  ( ph -> F e. ( J I C ) )
69 68 adantr 
 |-  ( ( ph /\ B =/= C ) -> F e. ( J I C ) )
70 1 11 2 3 15 13 axtgcgrrflx 
 |-  ( ph -> ( J .- F ) = ( F .- J ) )
71 70 23 eqtr2d 
 |-  ( ph -> ( B .- D ) = ( J .- F ) )
72 71 adantr 
 |-  ( ( ph /\ B =/= C ) -> ( B .- D ) = ( J .- F ) )
73 1 11 2 3 6 13 12 7 63 tgcgrcomlr 
 |-  ( ph -> ( F .- C ) = ( D .- E ) )
74 73 adantr 
 |-  ( ( ph /\ B =/= C ) -> ( F .- C ) = ( D .- E ) )
75 74 eqcomd 
 |-  ( ( ph /\ B =/= C ) -> ( D .- E ) = ( F .- C ) )
76 1 11 2 43 48 46 45 49 44 47 66 69 72 75 tgcgrextend 
 |-  ( ( ph /\ B =/= C ) -> ( B .- E ) = ( J .- C ) )
77 1 11 2 43 47 45 axtgcgrrflx 
 |-  ( ( ph /\ B =/= C ) -> ( C .- E ) = ( E .- C ) )
78 1 11 2 43 48 47 44 49 45 46 45 47 50 52 57 62 64 76 77 axtg5seg 
 |-  ( ( ph /\ B =/= C ) -> ( F .- E ) = ( D .- C ) )
79 1 11 2 43 44 45 46 47 78 tgcgrcomlr 
 |-  ( ( ph /\ B =/= C ) -> ( E .- F ) = ( C .- D ) )
80 42 79 pm2.61dane 
 |-  ( ph -> ( E .- F ) = ( C .- D ) )