Metamath Proof Explorer

Theorem tgbtwnconn1lem1

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 tgbtwnconn1lem1 
|- ( ph -> H = J )

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 4 5 7 12 10 16 tgbtwnexch 
 |-  ( ph -> B e. ( A I E ) )
25 1 11 2 3 4 5 12 14 24 18 tgbtwnexch 
 |-  ( ph -> B e. ( A I H ) )
26 1 11 2 3 4 5 6 13 9 17 tgbtwnexch 
 |-  ( ph -> B e. ( A I F ) )
27 1 11 2 3 4 5 13 15 26 19 tgbtwnexch 
 |-  ( ph -> B e. ( A I J ) )
28 1 11 2 3 4 5 12 14 24 18 tgbtwnexch3 
 |-  ( ph -> E e. ( B I H ) )
29 1 11 2 3 4 6 13 15 17 19 tgbtwnexch 
 |-  ( ph -> C e. ( A I J ) )
30 1 11 2 3 4 5 6 15 9 29 tgbtwnexch3 
 |-  ( ph -> C e. ( B I J ) )
31 1 11 2 3 5 6 15 30 tgbtwncom 
 |-  ( ph -> C e. ( J I B ) )
32 1 11 2 3 4 5 7 12 10 16 tgbtwnexch3 
 |-  ( ph -> D e. ( B I E ) )
33 1 11 2 3 4 6 13 15 17 19 tgbtwnexch3 
 |-  ( ph -> F e. ( C I J ) )
34 1 11 2 3 6 13 15 33 tgbtwncom 
 |-  ( ph -> F e. ( J I C ) )
35 1 11 2 3 15 13 axtgcgrrflx 
 |-  ( ph -> ( J .- F ) = ( F .- J ) )
36 35 23 eqtr2d 
 |-  ( ph -> ( B .- D ) = ( J .- F ) )
37 20 21 eqtr4d 
 |-  ( ph -> ( E .- D ) = ( C .- F ) )
38 1 11 2 3 12 7 6 13 37 tgcgrcomlr 
 |-  ( ph -> ( D .- E ) = ( F .- C ) )
39 1 11 2 3 5 7 12 15 13 6 32 34 36 38 tgcgrextend 
 |-  ( ph -> ( B .- E ) = ( J .- C ) )
40 1 11 2 3 12 14 5 6 22 tgcgrcomr 
 |-  ( ph -> ( E .- H ) = ( C .- B ) )
41 1 11 2 3 5 12 14 15 6 5 28 31 39 40 tgcgrextend 
 |-  ( ph -> ( B .- H ) = ( J .- B ) )
42 1 11 2 3 5 15 axtgcgrrflx 
 |-  ( ph -> ( B .- J ) = ( J .- B ) )
43 1 11 2 3 5 15 5 4 14 15 8 25 27 41 42 tgsegconeq 
 |-  ( ph -> H = J )