Proof of Theorem tgcgrsub2
| Step | Hyp | Ref
| Expression |
| 1 | | legval.p |
. . 3
⊢ 𝑃 = (Base‘𝐺) |
| 2 | | legval.d |
. . 3
⊢ − =
(dist‘𝐺) |
| 3 | | legval.i |
. . 3
⊢ 𝐼 = (Itv‘𝐺) |
| 4 | | legval.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
| 5 | 4 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → 𝐺 ∈ TarskiG) |
| 6 | | legtrd.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
| 7 | 6 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → 𝐶 ∈ 𝑃) |
| 8 | | legid.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
| 9 | 8 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → 𝐵 ∈ 𝑃) |
| 10 | | tgcgrsub2.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ 𝑃) |
| 11 | 10 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → 𝐹 ∈ 𝑃) |
| 12 | | tgcgrsub2.e |
. . . 4
⊢ (𝜑 → 𝐸 ∈ 𝑃) |
| 13 | 12 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → 𝐸 ∈ 𝑃) |
| 14 | | legid.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
| 15 | 14 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → 𝐴 ∈ 𝑃) |
| 16 | | legtrd.d |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ 𝑃) |
| 17 | 16 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → 𝐷 ∈ 𝑃) |
| 18 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → 𝐵 ∈ (𝐴𝐼𝐶)) |
| 19 | 1, 2, 3, 5, 15, 9,
7, 18 | tgbtwncom 28496 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → 𝐵 ∈ (𝐶𝐼𝐴)) |
| 20 | | legval.l |
. . . . . 6
⊢ ≤ =
(≤G‘𝐺) |
| 21 | | tgcgrsub2.2 |
. . . . . . 7
⊢ (𝜑 → (𝐸 ∈ (𝐷𝐼𝐹) ∨ 𝐹 ∈ (𝐷𝐼𝐸))) |
| 22 | 21 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → (𝐸 ∈ (𝐷𝐼𝐹) ∨ 𝐹 ∈ (𝐷𝐼𝐸))) |
| 23 | 1, 2, 3, 20, 5, 15, 9, 7, 18 | btwnleg 28596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → (𝐴 − 𝐵) ≤ (𝐴 − 𝐶)) |
| 24 | | tgcgrsub2.3 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) |
| 25 | 24 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → (𝐴 − 𝐵) = (𝐷 − 𝐸)) |
| 26 | | tgcgrsub2.4 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 − 𝐶) = (𝐷 − 𝐹)) |
| 27 | 26 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → (𝐴 − 𝐶) = (𝐷 − 𝐹)) |
| 28 | 23, 25, 27 | 3brtr3d 5174 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → (𝐷 − 𝐸) ≤ (𝐷 − 𝐹)) |
| 29 | 1, 2, 3, 20, 5, 13, 11, 17, 17, 22, 28 | legbtwn 28602 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → 𝐸 ∈ (𝐷𝐼𝐹)) |
| 30 | 1, 2, 3, 5, 17, 13, 11, 29 | tgbtwncom 28496 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → 𝐸 ∈ (𝐹𝐼𝐷)) |
| 31 | 1, 2, 3, 4, 14, 6,
16, 10, 26 | tgcgrcomlr 28488 |
. . . . 5
⊢ (𝜑 → (𝐶 − 𝐴) = (𝐹 − 𝐷)) |
| 32 | 31 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → (𝐶 − 𝐴) = (𝐹 − 𝐷)) |
| 33 | 1, 2, 3, 4, 14, 8,
16, 12, 24 | tgcgrcomlr 28488 |
. . . . 5
⊢ (𝜑 → (𝐵 − 𝐴) = (𝐸 − 𝐷)) |
| 34 | 33 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → (𝐵 − 𝐴) = (𝐸 − 𝐷)) |
| 35 | 1, 2, 3, 5, 7, 9, 15, 11, 13, 17, 19, 30, 32, 34 | tgcgrsub 28517 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → (𝐶 − 𝐵) = (𝐹 − 𝐸)) |
| 36 | 1, 2, 3, 5, 7, 9, 11, 13, 35 | tgcgrcomlr 28488 |
. 2
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → (𝐵 − 𝐶) = (𝐸 − 𝐹)) |
| 37 | 4 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → 𝐺 ∈ TarskiG) |
| 38 | 8 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → 𝐵 ∈ 𝑃) |
| 39 | 6 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → 𝐶 ∈ 𝑃) |
| 40 | 14 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → 𝐴 ∈ 𝑃) |
| 41 | 12 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → 𝐸 ∈ 𝑃) |
| 42 | 10 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → 𝐹 ∈ 𝑃) |
| 43 | 16 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → 𝐷 ∈ 𝑃) |
| 44 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → 𝐶 ∈ (𝐴𝐼𝐵)) |
| 45 | 1, 2, 3, 37, 40, 39, 38, 44 | tgbtwncom 28496 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → 𝐶 ∈ (𝐵𝐼𝐴)) |
| 46 | 21 | orcomd 872 |
. . . . . 6
⊢ (𝜑 → (𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐸 ∈ (𝐷𝐼𝐹))) |
| 47 | 46 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → (𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐸 ∈ (𝐷𝐼𝐹))) |
| 48 | 1, 2, 3, 20, 37, 40, 39, 38, 44 | btwnleg 28596 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → (𝐴 − 𝐶) ≤ (𝐴 − 𝐵)) |
| 49 | 26 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → (𝐴 − 𝐶) = (𝐷 − 𝐹)) |
| 50 | 24 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → (𝐴 − 𝐵) = (𝐷 − 𝐸)) |
| 51 | 48, 49, 50 | 3brtr3d 5174 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → (𝐷 − 𝐹) ≤ (𝐷 − 𝐸)) |
| 52 | 1, 2, 3, 20, 37, 42, 41, 43, 43, 47, 51 | legbtwn 28602 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → 𝐹 ∈ (𝐷𝐼𝐸)) |
| 53 | 1, 2, 3, 37, 43, 42, 41, 52 | tgbtwncom 28496 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → 𝐹 ∈ (𝐸𝐼𝐷)) |
| 54 | 33 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → (𝐵 − 𝐴) = (𝐸 − 𝐷)) |
| 55 | 31 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → (𝐶 − 𝐴) = (𝐹 − 𝐷)) |
| 56 | 1, 2, 3, 37, 38, 39, 40, 41, 42, 43, 45, 53, 54, 55 | tgcgrsub 28517 |
. 2
⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → (𝐵 − 𝐶) = (𝐸 − 𝐹)) |
| 57 | | tgcgrsub2.1 |
. 2
⊢ (𝜑 → (𝐵 ∈ (𝐴𝐼𝐶) ∨ 𝐶 ∈ (𝐴𝐼𝐵))) |
| 58 | 36, 56, 57 | mpjaodan 961 |
1
⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹)) |