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

Theorem lnhl 26737
Description: Either a point 𝐶 on the line AB is on the same side as 𝐴 or on the opposite side. (Contributed by Thierry Arnoux, 21-Sep-2020.)
Hypotheses
Ref Expression
ishlg.p 𝑃 = (Base‘𝐺)
ishlg.i 𝐼 = (Itv‘𝐺)
ishlg.k 𝐾 = (hlG‘𝐺)
ishlg.a (𝜑𝐴𝑃)
ishlg.b (𝜑𝐵𝑃)
ishlg.c (𝜑𝐶𝑃)
hlln.1 (𝜑𝐺 ∈ TarskiG)
hltr.d (𝜑𝐷𝑃)
lnhl.l 𝐿 = (LineG‘𝐺)
lnhl.1 (𝜑𝐶 ∈ (𝐴𝐿𝐵))
Assertion
Ref Expression
lnhl (𝜑 → (𝐶(𝐾𝐵)𝐴𝐵 ∈ (𝐴𝐼𝐶)))

Proof of Theorem lnhl
StepHypRef Expression
1 simpr 488 . . . 4 ((𝜑𝐶 = 𝐵) → 𝐶 = 𝐵)
2 ishlg.p . . . . . 6 𝑃 = (Base‘𝐺)
3 eqid 2739 . . . . . 6 (dist‘𝐺) = (dist‘𝐺)
4 ishlg.i . . . . . 6 𝐼 = (Itv‘𝐺)
5 hlln.1 . . . . . 6 (𝜑𝐺 ∈ TarskiG)
6 ishlg.a . . . . . 6 (𝜑𝐴𝑃)
7 ishlg.c . . . . . 6 (𝜑𝐶𝑃)
82, 3, 4, 5, 6, 7tgbtwntriv2 26609 . . . . 5 (𝜑𝐶 ∈ (𝐴𝐼𝐶))
98adantr 484 . . . 4 ((𝜑𝐶 = 𝐵) → 𝐶 ∈ (𝐴𝐼𝐶))
101, 9eqeltrrd 2841 . . 3 ((𝜑𝐶 = 𝐵) → 𝐵 ∈ (𝐴𝐼𝐶))
1110olcd 874 . 2 ((𝜑𝐶 = 𝐵) → (𝐶(𝐾𝐵)𝐴𝐵 ∈ (𝐴𝐼𝐶)))
12 lnhl.1 . . . . . 6 (𝜑𝐶 ∈ (𝐴𝐿𝐵))
13 lnhl.l . . . . . . 7 𝐿 = (LineG‘𝐺)
14 ishlg.b . . . . . . 7 (𝜑𝐵𝑃)
152, 13, 4, 5, 6, 14, 12tglngne 26672 . . . . . . 7 (𝜑𝐴𝐵)
162, 13, 4, 5, 6, 14, 15, 7tgellng 26675 . . . . . 6 (𝜑 → (𝐶 ∈ (𝐴𝐿𝐵) ↔ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐴𝐼𝐶))))
1712, 16mpbid 235 . . . . 5 (𝜑 → (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐴𝐼𝐶)))
18 df-3or 1090 . . . . 5 ((𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐴𝐼𝐶)) ↔ ((𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵)) ∨ 𝐵 ∈ (𝐴𝐼𝐶)))
1917, 18sylib 221 . . . 4 (𝜑 → ((𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵)) ∨ 𝐵 ∈ (𝐴𝐼𝐶)))
2019adantr 484 . . 3 ((𝜑𝐶𝐵) → ((𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵)) ∨ 𝐵 ∈ (𝐴𝐼𝐶)))
21 ishlg.k . . . . . . . 8 𝐾 = (hlG‘𝐺)
222, 4, 21, 7, 6, 14, 5ishlg 26724 . . . . . . 7 (𝜑 → (𝐶(𝐾𝐵)𝐴 ↔ (𝐶𝐵𝐴𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶)))))
2322adantr 484 . . . . . 6 ((𝜑𝐶𝐵) → (𝐶(𝐾𝐵)𝐴 ↔ (𝐶𝐵𝐴𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶)))))
24 df-3an 1091 . . . . . 6 ((𝐶𝐵𝐴𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶))) ↔ ((𝐶𝐵𝐴𝐵) ∧ (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶))))
2523, 24bitrdi 290 . . . . 5 ((𝜑𝐶𝐵) → (𝐶(𝐾𝐵)𝐴 ↔ ((𝐶𝐵𝐴𝐵) ∧ (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶)))))
2615anim1ci 619 . . . . . 6 ((𝜑𝐶𝐵) → (𝐶𝐵𝐴𝐵))
2726biantrurd 536 . . . . 5 ((𝜑𝐶𝐵) → ((𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶)) ↔ ((𝐶𝐵𝐴𝐵) ∧ (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶)))))
285adantr 484 . . . . . . 7 ((𝜑𝐶𝐵) → 𝐺 ∈ TarskiG)
2914adantr 484 . . . . . . 7 ((𝜑𝐶𝐵) → 𝐵𝑃)
307adantr 484 . . . . . . 7 ((𝜑𝐶𝐵) → 𝐶𝑃)
316adantr 484 . . . . . . 7 ((𝜑𝐶𝐵) → 𝐴𝑃)
322, 3, 4, 28, 29, 30, 31tgbtwncomb 26611 . . . . . 6 ((𝜑𝐶𝐵) → (𝐶 ∈ (𝐵𝐼𝐴) ↔ 𝐶 ∈ (𝐴𝐼𝐵)))
332, 3, 4, 28, 29, 31, 30tgbtwncomb 26611 . . . . . 6 ((𝜑𝐶𝐵) → (𝐴 ∈ (𝐵𝐼𝐶) ↔ 𝐴 ∈ (𝐶𝐼𝐵)))
3432, 33orbi12d 919 . . . . 5 ((𝜑𝐶𝐵) → ((𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶)) ↔ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))))
3525, 27, 343bitr2d 310 . . . 4 ((𝜑𝐶𝐵) → (𝐶(𝐾𝐵)𝐴 ↔ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))))
3635orbi1d 917 . . 3 ((𝜑𝐶𝐵) → ((𝐶(𝐾𝐵)𝐴𝐵 ∈ (𝐴𝐼𝐶)) ↔ ((𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵)) ∨ 𝐵 ∈ (𝐴𝐼𝐶))))
3720, 36mpbird 260 . 2 ((𝜑𝐶𝐵) → (𝐶(𝐾𝐵)𝐴𝐵 ∈ (𝐴𝐼𝐶)))
3811, 37pm2.61dane 3032 1 (𝜑 → (𝐶(𝐾𝐵)𝐴𝐵 ∈ (𝐴𝐼𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wo 847  w3o 1088  w3a 1089   = wceq 1543  wcel 2112  wne 2943   class class class wbr 5069  cfv 6400  (class class class)co 7234  Basecbs 16792  distcds 16843  TarskiGcstrkg 26552  Itvcitv 26558  LineGclng 26559  hlGchlg 26722
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-rep 5195  ax-sep 5208  ax-nul 5215  ax-pow 5274  ax-pr 5338  ax-un 7544
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3071  df-rab 3073  df-v 3425  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4456  df-pw 4531  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4836  df-iun 4922  df-br 5070  df-opab 5132  df-mpt 5152  df-id 5471  df-xp 5574  df-rel 5575  df-cnv 5576  df-co 5577  df-dm 5578  df-rn 5579  df-res 5580  df-ima 5581  df-iota 6358  df-fun 6402  df-fn 6403  df-f 6404  df-f1 6405  df-fo 6406  df-f1o 6407  df-fv 6408  df-ov 7237  df-oprab 7238  df-mpo 7239  df-1st 7782  df-2nd 7783  df-trkgc 26570  df-trkgb 26571  df-trkgcb 26572  df-trkg 26575  df-hlg 26723
This theorem is referenced by:  hlpasch  26878
  Copyright terms: Public domain W3C validator