Theorem btwnlng1 27270

Description: Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.)

Hypotheses

Ref	Expression
btwnlng1.p	⊢ 𝑃 = (Base‘𝐺)
btwnlng1.i	⊢ 𝐼 = (Itv‘𝐺)
btwnlng1.l	⊢ 𝐿 = (LineG‘𝐺)
btwnlng1.g	⊢ (𝜑 → 𝐺 ∈ TarskiG)
btwnlng1.x	⊢ (𝜑 → 𝑋 ∈ 𝑃)
btwnlng1.y	⊢ (𝜑 → 𝑌 ∈ 𝑃)
btwnlng1.z	⊢ (𝜑 → 𝑍 ∈ 𝑃)
btwnlng1.d	⊢ (𝜑 → 𝑋 ≠ 𝑌)
btwnlng1.1	⊢ (𝜑 → 𝑍 ∈ (𝑋𝐼𝑌))

Assertion

Ref	Expression
btwnlng1	⊢ (𝜑 → 𝑍 ∈ (𝑋𝐿𝑌))

Proof of Theorem btwnlng1

Step	Hyp	Ref	Expression
1		btwnlng1.1	. . 3 ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐼𝑌))
2	1	3mix1d 1335	. 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 27204	. 2 ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐿𝑌) ↔ (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))))
12	2, 11	mpbird 256	1 ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐿𝑌))

Syntax hints:   → wi 4   ∨ w3o 1085   = wceq 1540   ∈ wcel 2105   ≠ wne 2940  ‘cfv 6480  (class class class)co 7338  Basecbs 17010  TarskiGcstrkg 27078  Itvcitv 27084  LineGclng 27085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5244  ax-nul 5251  ax-pr 5373

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-sbc 3728  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4271  df-if 4475  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4854  df-br 5094  df-opab 5156  df-id 5519  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-iota 6432  df-fun 6482  df-fv 6488  df-ov 7341  df-oprab 7342  df-mpo 7343  df-trkg 27104

This theorem is referenced by:  tglnne  27279  tglinerflx1  27284  tglinerflx2  27285  coltr3  27299  mirln2  27328  midexlem  27343  colperpexlem3  27383  mideulem2  27385  opphllem1  27398  opphllem2  27399  opphllem4  27401  hlpasch  27407  lnopp2hpgb  27414  colopp  27420  lmieu  27435  lmimid  27445  lmiisolem  27447  hypcgrlem1  27450  hypcgrlem2  27451  trgcopyeulem  27456