| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > btwnlng1 | Structured version Visualization version GIF version | ||
| Description: Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.) |
| Ref | Expression |
|---|---|
| btwnlng1.p | ⊢ 𝑃 = (Base‘𝐺) |
| btwnlng1.i | ⊢ 𝐼 = (Itv‘𝐺) |
| btwnlng1.l | ⊢ 𝐿 = (LineG‘𝐺) |
| btwnlng1.g | ⊢ (𝜑 → 𝐺 ∈ TarskiG) |
| btwnlng1.x | ⊢ (𝜑 → 𝑋 ∈ 𝑃) |
| btwnlng1.y | ⊢ (𝜑 → 𝑌 ∈ 𝑃) |
| btwnlng1.z | ⊢ (𝜑 → 𝑍 ∈ 𝑃) |
| btwnlng1.d | ⊢ (𝜑 → 𝑋 ≠ 𝑌) |
| btwnlng1.1 | ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐼𝑌)) |
| Ref | Expression |
|---|---|
| btwnlng1 | ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐿𝑌)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | btwnlng1.1 | . . 3 ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐼𝑌)) | |
| 2 | 1 | 3mix1d 1337 | . 2 ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))) |
| 3 | btwnlng1.p | . . 3 ⊢ 𝑃 = (Base‘𝐺) | |
| 4 | btwnlng1.l | . . 3 ⊢ 𝐿 = (LineG‘𝐺) | |
| 5 | btwnlng1.i | . . 3 ⊢ 𝐼 = (Itv‘𝐺) | |
| 6 | btwnlng1.g | . . 3 ⊢ (𝜑 → 𝐺 ∈ TarskiG) | |
| 7 | btwnlng1.x | . . 3 ⊢ (𝜑 → 𝑋 ∈ 𝑃) | |
| 8 | btwnlng1.y | . . 3 ⊢ (𝜑 → 𝑌 ∈ 𝑃) | |
| 9 | btwnlng1.d | . . 3 ⊢ (𝜑 → 𝑋 ≠ 𝑌) | |
| 10 | btwnlng1.z | . . 3 ⊢ (𝜑 → 𝑍 ∈ 𝑃) | |
| 11 | 3, 4, 5, 6, 7, 8, 9, 10 | tgellng 28533 | . 2 ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐿𝑌) ↔ (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))) |
| 12 | 2, 11 | mpbird 257 | 1 ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐿𝑌)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∨ w3o 1085 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ‘cfv 6499 (class class class)co 7369 Basecbs 17155 TarskiGcstrkg 28407 Itvcitv 28413 LineGclng 28414 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5246 ax-nul 5256 ax-pr 5382 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-ral 3045 df-rex 3054 df-rab 3403 df-v 3446 df-sbc 3751 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-br 5103 df-opab 5165 df-id 5526 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-iota 6452 df-fun 6501 df-fv 6507 df-ov 7372 df-oprab 7373 df-mpo 7374 df-trkg 28433 |
| This theorem is referenced by: tglnne 28608 tglinerflx1 28613 tglinerflx2 28614 coltr3 28628 mirln2 28657 midexlem 28672 colperpexlem3 28712 mideulem2 28714 opphllem1 28727 opphllem2 28728 opphllem4 28730 hlpasch 28736 lnopp2hpgb 28743 colopp 28749 lmieu 28764 lmimid 28774 lmiisolem 28776 hypcgrlem1 28779 hypcgrlem2 28780 trgcopyeulem 28785 |
| Copyright terms: Public domain | W3C validator |