Metamath Proof Explorer


Theorem tgbtwnconn1lem2

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

Ref Expression
Hypotheses tgbtwnconn1.p 𝑃 = ( Base ‘ 𝐺 )
tgbtwnconn1.i 𝐼 = ( Itv ‘ 𝐺 )
tgbtwnconn1.g ( 𝜑𝐺 ∈ TarskiG )
tgbtwnconn1.a ( 𝜑𝐴𝑃 )
tgbtwnconn1.b ( 𝜑𝐵𝑃 )
tgbtwnconn1.c ( 𝜑𝐶𝑃 )
tgbtwnconn1.d ( 𝜑𝐷𝑃 )
tgbtwnconn1.1 ( 𝜑𝐴𝐵 )
tgbtwnconn1.2 ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
tgbtwnconn1.3 ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐷 ) )
tgbtwnconn1.m = ( dist ‘ 𝐺 )
tgbtwnconn1.e ( 𝜑𝐸𝑃 )
tgbtwnconn1.f ( 𝜑𝐹𝑃 )
tgbtwnconn1.h ( 𝜑𝐻𝑃 )
tgbtwnconn1.j ( 𝜑𝐽𝑃 )
tgbtwnconn1.4 ( 𝜑𝐷 ∈ ( 𝐴 𝐼 𝐸 ) )
tgbtwnconn1.5 ( 𝜑𝐶 ∈ ( 𝐴 𝐼 𝐹 ) )
tgbtwnconn1.6 ( 𝜑𝐸 ∈ ( 𝐴 𝐼 𝐻 ) )
tgbtwnconn1.7 ( 𝜑𝐹 ∈ ( 𝐴 𝐼 𝐽 ) )
tgbtwnconn1.8 ( 𝜑 → ( 𝐸 𝐷 ) = ( 𝐶 𝐷 ) )
tgbtwnconn1.9 ( 𝜑 → ( 𝐶 𝐹 ) = ( 𝐶 𝐷 ) )
tgbtwnconn1.10 ( 𝜑 → ( 𝐸 𝐻 ) = ( 𝐵 𝐶 ) )
tgbtwnconn1.11 ( 𝜑 → ( 𝐹 𝐽 ) = ( 𝐵 𝐷 ) )
Assertion tgbtwnconn1lem2 ( 𝜑 → ( 𝐸 𝐹 ) = ( 𝐶 𝐷 ) )

Proof

Step Hyp Ref Expression
1 tgbtwnconn1.p 𝑃 = ( Base ‘ 𝐺 )
2 tgbtwnconn1.i 𝐼 = ( Itv ‘ 𝐺 )
3 tgbtwnconn1.g ( 𝜑𝐺 ∈ TarskiG )
4 tgbtwnconn1.a ( 𝜑𝐴𝑃 )
5 tgbtwnconn1.b ( 𝜑𝐵𝑃 )
6 tgbtwnconn1.c ( 𝜑𝐶𝑃 )
7 tgbtwnconn1.d ( 𝜑𝐷𝑃 )
8 tgbtwnconn1.1 ( 𝜑𝐴𝐵 )
9 tgbtwnconn1.2 ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
10 tgbtwnconn1.3 ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐷 ) )
11 tgbtwnconn1.m = ( dist ‘ 𝐺 )
12 tgbtwnconn1.e ( 𝜑𝐸𝑃 )
13 tgbtwnconn1.f ( 𝜑𝐹𝑃 )
14 tgbtwnconn1.h ( 𝜑𝐻𝑃 )
15 tgbtwnconn1.j ( 𝜑𝐽𝑃 )
16 tgbtwnconn1.4 ( 𝜑𝐷 ∈ ( 𝐴 𝐼 𝐸 ) )
17 tgbtwnconn1.5 ( 𝜑𝐶 ∈ ( 𝐴 𝐼 𝐹 ) )
18 tgbtwnconn1.6 ( 𝜑𝐸 ∈ ( 𝐴 𝐼 𝐻 ) )
19 tgbtwnconn1.7 ( 𝜑𝐹 ∈ ( 𝐴 𝐼 𝐽 ) )
20 tgbtwnconn1.8 ( 𝜑 → ( 𝐸 𝐷 ) = ( 𝐶 𝐷 ) )
21 tgbtwnconn1.9 ( 𝜑 → ( 𝐶 𝐹 ) = ( 𝐶 𝐷 ) )
22 tgbtwnconn1.10 ( 𝜑 → ( 𝐸 𝐻 ) = ( 𝐵 𝐶 ) )
23 tgbtwnconn1.11 ( 𝜑 → ( 𝐹 𝐽 ) = ( 𝐵 𝐷 ) )
24 1 11 2 3 12 13 axtgcgrrflx ( 𝜑 → ( 𝐸 𝐹 ) = ( 𝐹 𝐸 ) )
25 24 adantr ( ( 𝜑𝐵 = 𝐶 ) → ( 𝐸 𝐹 ) = ( 𝐹 𝐸 ) )
26 3 adantr ( ( 𝜑𝐵 = 𝐶 ) → 𝐺 ∈ TarskiG )
27 12 adantr ( ( 𝜑𝐵 = 𝐶 ) → 𝐸𝑃 )
28 14 adantr ( ( 𝜑𝐵 = 𝐶 ) → 𝐻𝑃 )
29 6 adantr ( ( 𝜑𝐵 = 𝐶 ) → 𝐶𝑃 )
30 22 adantr ( ( 𝜑𝐵 = 𝐶 ) → ( 𝐸 𝐻 ) = ( 𝐵 𝐶 ) )
31 simpr ( ( 𝜑𝐵 = 𝐶 ) → 𝐵 = 𝐶 )
32 31 oveq1d ( ( 𝜑𝐵 = 𝐶 ) → ( 𝐵 𝐶 ) = ( 𝐶 𝐶 ) )
33 30 32 eqtrd ( ( 𝜑𝐵 = 𝐶 ) → ( 𝐸 𝐻 ) = ( 𝐶 𝐶 ) )
34 1 11 2 26 27 28 29 33 axtgcgrid ( ( 𝜑𝐵 = 𝐶 ) → 𝐸 = 𝐻 )
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 ( 𝜑𝐻 = 𝐽 )
36 35 adantr ( ( 𝜑𝐵 = 𝐶 ) → 𝐻 = 𝐽 )
37 34 36 eqtrd ( ( 𝜑𝐵 = 𝐶 ) → 𝐸 = 𝐽 )
38 37 oveq2d ( ( 𝜑𝐵 = 𝐶 ) → ( 𝐹 𝐸 ) = ( 𝐹 𝐽 ) )
39 23 adantr ( ( 𝜑𝐵 = 𝐶 ) → ( 𝐹 𝐽 ) = ( 𝐵 𝐷 ) )
40 31 oveq1d ( ( 𝜑𝐵 = 𝐶 ) → ( 𝐵 𝐷 ) = ( 𝐶 𝐷 ) )
41 38 39 40 3eqtrd ( ( 𝜑𝐵 = 𝐶 ) → ( 𝐹 𝐸 ) = ( 𝐶 𝐷 ) )
42 25 41 eqtrd ( ( 𝜑𝐵 = 𝐶 ) → ( 𝐸 𝐹 ) = ( 𝐶 𝐷 ) )
43 3 adantr ( ( 𝜑𝐵𝐶 ) → 𝐺 ∈ TarskiG )
44 13 adantr ( ( 𝜑𝐵𝐶 ) → 𝐹𝑃 )
45 12 adantr ( ( 𝜑𝐵𝐶 ) → 𝐸𝑃 )
46 7 adantr ( ( 𝜑𝐵𝐶 ) → 𝐷𝑃 )
47 6 adantr ( ( 𝜑𝐵𝐶 ) → 𝐶𝑃 )
48 5 adantr ( ( 𝜑𝐵𝐶 ) → 𝐵𝑃 )
49 15 adantr ( ( 𝜑𝐵𝐶 ) → 𝐽𝑃 )
50 simpr ( ( 𝜑𝐵𝐶 ) → 𝐵𝐶 )
51 1 11 2 3 4 5 6 13 9 17 tgbtwnexch3 ( 𝜑𝐶 ∈ ( 𝐵 𝐼 𝐹 ) )
52 51 adantr ( ( 𝜑𝐵𝐶 ) → 𝐶 ∈ ( 𝐵 𝐼 𝐹 ) )
53 35 oveq2d ( 𝜑 → ( 𝐴 𝐼 𝐻 ) = ( 𝐴 𝐼 𝐽 ) )
54 18 53 eleqtrd ( 𝜑𝐸 ∈ ( 𝐴 𝐼 𝐽 ) )
55 1 11 2 3 4 7 12 15 16 54 tgbtwnexch3 ( 𝜑𝐸 ∈ ( 𝐷 𝐼 𝐽 ) )
56 1 11 2 3 7 12 15 55 tgbtwncom ( 𝜑𝐸 ∈ ( 𝐽 𝐼 𝐷 ) )
57 56 adantr ( ( 𝜑𝐵𝐶 ) → 𝐸 ∈ ( 𝐽 𝐼 𝐷 ) )
58 35 adantr ( ( 𝜑𝐵𝐶 ) → 𝐻 = 𝐽 )
59 58 oveq2d ( ( 𝜑𝐵𝐶 ) → ( 𝐸 𝐻 ) = ( 𝐸 𝐽 ) )
60 22 adantr ( ( 𝜑𝐵𝐶 ) → ( 𝐸 𝐻 ) = ( 𝐵 𝐶 ) )
61 1 11 2 43 45 49 axtgcgrrflx ( ( 𝜑𝐵𝐶 ) → ( 𝐸 𝐽 ) = ( 𝐽 𝐸 ) )
62 59 60 61 3eqtr3d ( ( 𝜑𝐵𝐶 ) → ( 𝐵 𝐶 ) = ( 𝐽 𝐸 ) )
63 21 20 eqtr4d ( 𝜑 → ( 𝐶 𝐹 ) = ( 𝐸 𝐷 ) )
64 63 adantr ( ( 𝜑𝐵𝐶 ) → ( 𝐶 𝐹 ) = ( 𝐸 𝐷 ) )
65 1 11 2 3 4 5 7 12 10 16 tgbtwnexch3 ( 𝜑𝐷 ∈ ( 𝐵 𝐼 𝐸 ) )
66 65 adantr ( ( 𝜑𝐵𝐶 ) → 𝐷 ∈ ( 𝐵 𝐼 𝐸 ) )
67 1 11 2 3 4 6 13 15 17 19 tgbtwnexch3 ( 𝜑𝐹 ∈ ( 𝐶 𝐼 𝐽 ) )
68 1 11 2 3 6 13 15 67 tgbtwncom ( 𝜑𝐹 ∈ ( 𝐽 𝐼 𝐶 ) )
69 68 adantr ( ( 𝜑𝐵𝐶 ) → 𝐹 ∈ ( 𝐽 𝐼 𝐶 ) )
70 1 11 2 3 15 13 axtgcgrrflx ( 𝜑 → ( 𝐽 𝐹 ) = ( 𝐹 𝐽 ) )
71 70 23 eqtr2d ( 𝜑 → ( 𝐵 𝐷 ) = ( 𝐽 𝐹 ) )
72 71 adantr ( ( 𝜑𝐵𝐶 ) → ( 𝐵 𝐷 ) = ( 𝐽 𝐹 ) )
73 1 11 2 3 6 13 12 7 63 tgcgrcomlr ( 𝜑 → ( 𝐹 𝐶 ) = ( 𝐷 𝐸 ) )
74 73 adantr ( ( 𝜑𝐵𝐶 ) → ( 𝐹 𝐶 ) = ( 𝐷 𝐸 ) )
75 74 eqcomd ( ( 𝜑𝐵𝐶 ) → ( 𝐷 𝐸 ) = ( 𝐹 𝐶 ) )
76 1 11 2 43 48 46 45 49 44 47 66 69 72 75 tgcgrextend ( ( 𝜑𝐵𝐶 ) → ( 𝐵 𝐸 ) = ( 𝐽 𝐶 ) )
77 1 11 2 43 47 45 axtgcgrrflx ( ( 𝜑𝐵𝐶 ) → ( 𝐶 𝐸 ) = ( 𝐸 𝐶 ) )
78 1 11 2 43 48 47 44 49 45 46 45 47 50 52 57 62 64 76 77 axtg5seg ( ( 𝜑𝐵𝐶 ) → ( 𝐹 𝐸 ) = ( 𝐷 𝐶 ) )
79 1 11 2 43 44 45 46 47 78 tgcgrcomlr ( ( 𝜑𝐵𝐶 ) → ( 𝐸 𝐹 ) = ( 𝐶 𝐷 ) )
80 42 79 pm2.61dane ( 𝜑 → ( 𝐸 𝐹 ) = ( 𝐶 𝐷 ) )