Proof of Theorem tgbtwnconn1lem2
Step | Hyp | Ref
| Expression |
1 | | tgbtwnconn1.p |
. . . . 5
⊢ 𝑃 = (Base‘𝐺) |
2 | | tgbtwnconn1.m |
. . . . 5
⊢ − =
(dist‘𝐺) |
3 | | tgbtwnconn1.i |
. . . . 5
⊢ 𝐼 = (Itv‘𝐺) |
4 | | tgbtwnconn1.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
5 | | tgbtwnconn1.e |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ 𝑃) |
6 | | tgbtwnconn1.f |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ 𝑃) |
7 | 1, 2, 3, 4, 5, 6 | axtgcgrrflx 26833 |
. . . 4
⊢ (𝜑 → (𝐸 − 𝐹) = (𝐹 − 𝐸)) |
8 | 7 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐸 − 𝐹) = (𝐹 − 𝐸)) |
9 | 4 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐺 ∈ TarskiG) |
10 | 5 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐸 ∈ 𝑃) |
11 | | tgbtwnconn1.h |
. . . . . . . 8
⊢ (𝜑 → 𝐻 ∈ 𝑃) |
12 | 11 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐻 ∈ 𝑃) |
13 | | tgbtwnconn1.c |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
14 | 13 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐶 ∈ 𝑃) |
15 | | tgbtwnconn1.10 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸 − 𝐻) = (𝐵 − 𝐶)) |
16 | 15 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐸 − 𝐻) = (𝐵 − 𝐶)) |
17 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐵 = 𝐶) |
18 | 17 | oveq1d 7282 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐵 − 𝐶) = (𝐶 − 𝐶)) |
19 | 16, 18 | eqtrd 2778 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐸 − 𝐻) = (𝐶 − 𝐶)) |
20 | 1, 2, 3, 9, 10, 12, 14, 19 | axtgcgrid 26834 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐸 = 𝐻) |
21 | | tgbtwnconn1.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
22 | | tgbtwnconn1.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
23 | | tgbtwnconn1.d |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ 𝑃) |
24 | | tgbtwnconn1.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ≠ 𝐵) |
25 | | tgbtwnconn1.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) |
26 | | tgbtwnconn1.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) |
27 | | tgbtwnconn1.j |
. . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ 𝑃) |
28 | | tgbtwnconn1.4 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ (𝐴𝐼𝐸)) |
29 | | tgbtwnconn1.5 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐹)) |
30 | | tgbtwnconn1.6 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ (𝐴𝐼𝐻)) |
31 | | tgbtwnconn1.7 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (𝐴𝐼𝐽)) |
32 | | tgbtwnconn1.8 |
. . . . . . . 8
⊢ (𝜑 → (𝐸 − 𝐷) = (𝐶 − 𝐷)) |
33 | | tgbtwnconn1.9 |
. . . . . . . 8
⊢ (𝜑 → (𝐶 − 𝐹) = (𝐶 − 𝐷)) |
34 | | tgbtwnconn1.11 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 − 𝐽) = (𝐵 − 𝐷)) |
35 | 1, 3, 4, 21, 22, 13, 23, 24, 25, 26, 2, 5, 6, 11, 27, 28, 29, 30, 31, 32, 33, 15, 34 | tgbtwnconn1lem1 26943 |
. . . . . . 7
⊢ (𝜑 → 𝐻 = 𝐽) |
36 | 35 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐻 = 𝐽) |
37 | 20, 36 | eqtrd 2778 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐸 = 𝐽) |
38 | 37 | oveq2d 7283 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐹 − 𝐸) = (𝐹 − 𝐽)) |
39 | 34 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐹 − 𝐽) = (𝐵 − 𝐷)) |
40 | 17 | oveq1d 7282 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐵 − 𝐷) = (𝐶 − 𝐷)) |
41 | 38, 39, 40 | 3eqtrd 2782 |
. . 3
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐹 − 𝐸) = (𝐶 − 𝐷)) |
42 | 8, 41 | eqtrd 2778 |
. 2
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐸 − 𝐹) = (𝐶 − 𝐷)) |
43 | 4 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐺 ∈ TarskiG) |
44 | 6 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐹 ∈ 𝑃) |
45 | 5 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐸 ∈ 𝑃) |
46 | 23 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐷 ∈ 𝑃) |
47 | 13 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐶 ∈ 𝑃) |
48 | 22 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐵 ∈ 𝑃) |
49 | 27 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐽 ∈ 𝑃) |
50 | | simpr 485 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐵 ≠ 𝐶) |
51 | 1, 2, 3, 4, 21, 22, 13, 6, 25, 29 | tgbtwnexch3 26865 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ (𝐵𝐼𝐹)) |
52 | 51 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐶 ∈ (𝐵𝐼𝐹)) |
53 | 35 | oveq2d 7283 |
. . . . . . . 8
⊢ (𝜑 → (𝐴𝐼𝐻) = (𝐴𝐼𝐽)) |
54 | 30, 53 | eleqtrd 2841 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈ (𝐴𝐼𝐽)) |
55 | 1, 2, 3, 4, 21, 23, 5, 27, 28, 54 | tgbtwnexch3 26865 |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ (𝐷𝐼𝐽)) |
56 | 1, 2, 3, 4, 23, 5,
27, 55 | tgbtwncom 26859 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ (𝐽𝐼𝐷)) |
57 | 56 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐸 ∈ (𝐽𝐼𝐷)) |
58 | 35 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐻 = 𝐽) |
59 | 58 | oveq2d 7283 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐸 − 𝐻) = (𝐸 − 𝐽)) |
60 | 15 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐸 − 𝐻) = (𝐵 − 𝐶)) |
61 | 1, 2, 3, 43, 45, 49 | axtgcgrrflx 26833 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐸 − 𝐽) = (𝐽 − 𝐸)) |
62 | 59, 60, 61 | 3eqtr3d 2786 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐵 − 𝐶) = (𝐽 − 𝐸)) |
63 | 33, 32 | eqtr4d 2781 |
. . . . 5
⊢ (𝜑 → (𝐶 − 𝐹) = (𝐸 − 𝐷)) |
64 | 63 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐶 − 𝐹) = (𝐸 − 𝐷)) |
65 | 1, 2, 3, 4, 21, 22, 23, 5, 26, 28 | tgbtwnexch3 26865 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ (𝐵𝐼𝐸)) |
66 | 65 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐷 ∈ (𝐵𝐼𝐸)) |
67 | 1, 2, 3, 4, 21, 13, 6, 27, 29, 31 | tgbtwnexch3 26865 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (𝐶𝐼𝐽)) |
68 | 1, 2, 3, 4, 13, 6,
27, 67 | tgbtwncom 26859 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (𝐽𝐼𝐶)) |
69 | 68 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → 𝐹 ∈ (𝐽𝐼𝐶)) |
70 | 1, 2, 3, 4, 27, 6 | axtgcgrrflx 26833 |
. . . . . . 7
⊢ (𝜑 → (𝐽 − 𝐹) = (𝐹 − 𝐽)) |
71 | 70, 34 | eqtr2d 2779 |
. . . . . 6
⊢ (𝜑 → (𝐵 − 𝐷) = (𝐽 − 𝐹)) |
72 | 71 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐵 − 𝐷) = (𝐽 − 𝐹)) |
73 | 1, 2, 3, 4, 13, 6,
5, 23, 63 | tgcgrcomlr 26851 |
. . . . . . 7
⊢ (𝜑 → (𝐹 − 𝐶) = (𝐷 − 𝐸)) |
74 | 73 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐹 − 𝐶) = (𝐷 − 𝐸)) |
75 | 74 | eqcomd 2744 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐷 − 𝐸) = (𝐹 − 𝐶)) |
76 | 1, 2, 3, 43, 48, 46, 45, 49, 44, 47, 66, 69, 72, 75 | tgcgrextend 26856 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐵 − 𝐸) = (𝐽 − 𝐶)) |
77 | 1, 2, 3, 43, 47, 45 | axtgcgrrflx 26833 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐶 − 𝐸) = (𝐸 − 𝐶)) |
78 | 1, 2, 3, 43, 48, 47, 44, 49, 45, 46, 45, 47, 50, 52, 57, 62, 64, 76, 77 | axtg5seg 26836 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐹 − 𝐸) = (𝐷 − 𝐶)) |
79 | 1, 2, 3, 43, 44, 45, 46, 47, 78 | tgcgrcomlr 26851 |
. 2
⊢ ((𝜑 ∧ 𝐵 ≠ 𝐶) → (𝐸 − 𝐹) = (𝐶 − 𝐷)) |
80 | 42, 79 | pm2.61dane 3032 |
1
⊢ (𝜑 → (𝐸 − 𝐹) = (𝐶 − 𝐷)) |