Proof of Theorem tgcgrextend
Step | Hyp | Ref
| Expression |
1 | | tgcgrextend.4 |
. . . 4
⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹)) |
2 | 1 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → (𝐵 − 𝐶) = (𝐸 − 𝐹)) |
3 | | simpr 485 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐴 = 𝐵) |
4 | 3 | oveq1d 7282 |
. . 3
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → (𝐴 − 𝐶) = (𝐵 − 𝐶)) |
5 | | tkgeom.p |
. . . . 5
⊢ 𝑃 = (Base‘𝐺) |
6 | | tkgeom.d |
. . . . 5
⊢ − =
(dist‘𝐺) |
7 | | tkgeom.i |
. . . . 5
⊢ 𝐼 = (Itv‘𝐺) |
8 | | tkgeom.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
9 | 8 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐺 ∈ TarskiG) |
10 | | tgcgrextend.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
11 | 10 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐴 ∈ 𝑃) |
12 | | tgcgrextend.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
13 | 12 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐵 ∈ 𝑃) |
14 | | tgcgrextend.d |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ 𝑃) |
15 | 14 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐷 ∈ 𝑃) |
16 | | tgcgrextend.e |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ 𝑃) |
17 | 16 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐸 ∈ 𝑃) |
18 | | tgcgrextend.3 |
. . . . . 6
⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) |
19 | 18 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → (𝐴 − 𝐵) = (𝐷 − 𝐸)) |
20 | 5, 6, 7, 9, 11, 13, 15, 17, 19, 3 | tgcgreq 26853 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐷 = 𝐸) |
21 | 20 | oveq1d 7282 |
. . 3
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → (𝐷 − 𝐹) = (𝐸 − 𝐹)) |
22 | 2, 4, 21 | 3eqtr4d 2788 |
. 2
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → (𝐴 − 𝐶) = (𝐷 − 𝐹)) |
23 | 8 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐺 ∈ TarskiG) |
24 | | tgcgrextend.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
25 | 24 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐶 ∈ 𝑃) |
26 | 10 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐴 ∈ 𝑃) |
27 | | tgcgrextend.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ 𝑃) |
28 | 27 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐹 ∈ 𝑃) |
29 | 14 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐷 ∈ 𝑃) |
30 | 12 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐵 ∈ 𝑃) |
31 | 16 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐸 ∈ 𝑃) |
32 | | simpr 485 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐴 ≠ 𝐵) |
33 | | tgcgrextend.1 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) |
34 | 33 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐵 ∈ (𝐴𝐼𝐶)) |
35 | | tgcgrextend.2 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ (𝐷𝐼𝐹)) |
36 | 35 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐸 ∈ (𝐷𝐼𝐹)) |
37 | 18 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (𝐴 − 𝐵) = (𝐷 − 𝐸)) |
38 | 1 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (𝐵 − 𝐶) = (𝐸 − 𝐹)) |
39 | 5, 6, 7, 23, 26, 29 | tgcgrtriv 26855 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (𝐴 − 𝐴) = (𝐷 − 𝐷)) |
40 | 5, 6, 7, 23, 26, 30, 29, 31, 37 | tgcgrcomlr 26851 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (𝐵 − 𝐴) = (𝐸 − 𝐷)) |
41 | 5, 6, 7, 23, 26, 30, 25, 29, 31, 28, 26, 29, 32, 34, 36, 37, 38, 39, 40 | axtg5seg 26836 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (𝐶 − 𝐴) = (𝐹 − 𝐷)) |
42 | 5, 6, 7, 23, 25, 26, 28, 29, 41 | tgcgrcomlr 26851 |
. 2
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (𝐴 − 𝐶) = (𝐷 − 𝐹)) |
43 | 22, 42 | pm2.61dane 3032 |
1
⊢ (𝜑 → (𝐴 − 𝐶) = (𝐷 − 𝐹)) |