![]() |
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 1392 | . 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 25904 | . 2 ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐿𝑌) ↔ (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))) |
12 | 2, 11 | mpbird 249 | 1 ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐿𝑌)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ w3o 1070 = wceq 1601 ∈ wcel 2107 ≠ wne 2969 ‘cfv 6135 (class class class)co 6922 Basecbs 16255 TarskiGcstrkg 25781 Itvcitv 25787 LineGclng 25788 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-sep 5017 ax-nul 5025 ax-pr 5138 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3or 1072 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ne 2970 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3400 df-sbc 3653 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4672 df-br 4887 df-opab 4949 df-id 5261 df-xp 5361 df-rel 5362 df-cnv 5363 df-co 5364 df-dm 5365 df-iota 6099 df-fun 6137 df-fv 6143 df-ov 6925 df-oprab 6926 df-mpt2 6927 df-trkg 25804 |
This theorem is referenced by: tglnne 25979 tglinerflx1 25984 tglinerflx2 25985 coltr3 25999 mirln2 26028 midexlem 26043 colperpexlem3 26080 mideulem2 26082 opphllem1 26095 opphllem2 26096 opphllem4 26098 hlpasch 26104 lnopp2hpgb 26111 colopp 26117 colhp 26118 lmieu 26132 lmimid 26142 lmiisolem 26144 hypcgrlem1 26147 hypcgrlem2 26148 trgcopyeulem 26153 |
Copyright terms: Public domain | W3C validator |