MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  hlln Structured version   Visualization version   GIF version

Theorem hlln 28888
Description: The half-line relation implies colinearity, part of Theorem 6.4 of [Schwabhauser] p. 44. (Contributed by Thierry Arnoux, 22-Feb-2020.)
Hypotheses
Ref Expression
ishlg.p 𝑃 = (Base‘𝐺)
ishlg.i 𝐼 = (Itv‘𝐺)
ishlg.k 𝐾 = (hlG‘𝐺)
ishlg.a (𝜑𝐴𝑃)
ishlg.b (𝜑𝐵𝑃)
ishlg.c (𝜑𝐶𝑃)
hlln.1 (𝜑𝐺 ∈ TarskiG)
hlln.l 𝐿 = (LineG‘𝐺)
hlln.2 (𝜑𝐴(𝐾𝐶)𝐵)
Assertion
Ref Expression
hlln (𝜑𝐴 ∈ (𝐵𝐿𝐶))

Proof of Theorem hlln
StepHypRef Expression
1 ishlg.p . . . . 5 𝑃 = (Base‘𝐺)
2 eqid 2763 . . . . 5 (dist‘𝐺) = (dist‘𝐺)
3 ishlg.i . . . . 5 𝐼 = (Itv‘𝐺)
4 hlln.1 . . . . . 6 (𝜑𝐺 ∈ TarskiG)
54adantr 485 . . . . 5 ((𝜑𝐴 ∈ (𝐶𝐼𝐵)) → 𝐺 ∈ TarskiG)
6 ishlg.c . . . . . 6 (𝜑𝐶𝑃)
76adantr 485 . . . . 5 ((𝜑𝐴 ∈ (𝐶𝐼𝐵)) → 𝐶𝑃)
8 ishlg.a . . . . . 6 (𝜑𝐴𝑃)
98adantr 485 . . . . 5 ((𝜑𝐴 ∈ (𝐶𝐼𝐵)) → 𝐴𝑃)
10 ishlg.b . . . . . 6 (𝜑𝐵𝑃)
1110adantr 485 . . . . 5 ((𝜑𝐴 ∈ (𝐶𝐼𝐵)) → 𝐵𝑃)
12 simpr 489 . . . . 5 ((𝜑𝐴 ∈ (𝐶𝐼𝐵)) → 𝐴 ∈ (𝐶𝐼𝐵))
131, 2, 3, 5, 7, 9, 11, 12tgbtwncom 28766 . . . 4 ((𝜑𝐴 ∈ (𝐶𝐼𝐵)) → 𝐴 ∈ (𝐵𝐼𝐶))
14133mix1d 1355 . . 3 ((𝜑𝐴 ∈ (𝐶𝐼𝐵)) → (𝐴 ∈ (𝐵𝐼𝐶) ∨ 𝐵 ∈ (𝐴𝐼𝐶) ∨ 𝐶 ∈ (𝐵𝐼𝐴)))
154adantr 485 . . . . 5 ((𝜑𝐵 ∈ (𝐶𝐼𝐴)) → 𝐺 ∈ TarskiG)
166adantr 485 . . . . 5 ((𝜑𝐵 ∈ (𝐶𝐼𝐴)) → 𝐶𝑃)
1710adantr 485 . . . . 5 ((𝜑𝐵 ∈ (𝐶𝐼𝐴)) → 𝐵𝑃)
188adantr 485 . . . . 5 ((𝜑𝐵 ∈ (𝐶𝐼𝐴)) → 𝐴𝑃)
19 simpr 489 . . . . 5 ((𝜑𝐵 ∈ (𝐶𝐼𝐴)) → 𝐵 ∈ (𝐶𝐼𝐴))
201, 2, 3, 15, 16, 17, 18, 19tgbtwncom 28766 . . . 4 ((𝜑𝐵 ∈ (𝐶𝐼𝐴)) → 𝐵 ∈ (𝐴𝐼𝐶))
21203mix2d 1356 . . 3 ((𝜑𝐵 ∈ (𝐶𝐼𝐴)) → (𝐴 ∈ (𝐵𝐼𝐶) ∨ 𝐵 ∈ (𝐴𝐼𝐶) ∨ 𝐶 ∈ (𝐵𝐼𝐴)))
22 hlln.2 . . . . 5 (𝜑𝐴(𝐾𝐶)𝐵)
23 ishlg.k . . . . . 6 𝐾 = (hlG‘𝐺)
241, 3, 23, 8, 10, 6, 4ishlg 28883 . . . . 5 (𝜑 → (𝐴(𝐾𝐶)𝐵 ↔ (𝐴𝐶𝐵𝐶 ∧ (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴)))))
2522, 24mpbid 235 . . . 4 (𝜑 → (𝐴𝐶𝐵𝐶 ∧ (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴))))
2625simp3d 1162 . . 3 (𝜑 → (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴)))
2714, 21, 26mpjaodan 973 . 2 (𝜑 → (𝐴 ∈ (𝐵𝐼𝐶) ∨ 𝐵 ∈ (𝐴𝐼𝐶) ∨ 𝐶 ∈ (𝐵𝐼𝐴)))
28 hlln.l . . 3 𝐿 = (LineG‘𝐺)
2925simp2d 1161 . . 3 (𝜑𝐵𝐶)
301, 28, 3, 4, 10, 6, 29, 8tgellng 28831 . 2 (𝜑 → (𝐴 ∈ (𝐵𝐿𝐶) ↔ (𝐴 ∈ (𝐵𝐼𝐶) ∨ 𝐵 ∈ (𝐴𝐼𝐶) ∨ 𝐶 ∈ (𝐵𝐼𝐴))))
3127, 30mpbird 260 1 (𝜑𝐴 ∈ (𝐵𝐿𝐶))
Colors of variables:    wff setvar class
This proof depends on syntax axioms:  wi 4  wa 400  wo 860  w3o 1102  w3a 1103   = wceq 1570  wcel 2143  wne 2958   class class class wbr 5109  cfv 6536  (class class class)co 7410  Basecbs 17273  distcds 17323  TarskiGcstrkg 28705  Itvcitv 28711  LineGclng 28712  hlGchlg 28878
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5238  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732
This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-oprab 7414  df-mpo 7415  df-trkgc 28726  df-trkgb 28727  df-trkgcb 28728  df-trkg 28731  df-hlg 28879
This theorem is used by:  hlperpnel  29015  opphllem4  29040  opphl  29044  hlpasch  29047  colhp  29061  hphl  29062  trgcopy  29124  cgracgr  29138  cgraswap  29140  acopy  29153  acopyeu  29154  ragcgra  29155  cgrarag  29156  perpeqlem  29159  tgasa1  29184  tgaltai  29226
  Copyright terms: Public domain W3C validator