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

Theorem tgbtwncom 25128
Description: Betweenness commutes. Theorem 3.2 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 15-Mar-2019.)
Hypotheses
Ref Expression
tkgeom.p 𝑃 = (Base‘𝐺)
tkgeom.d = (dist‘𝐺)
tkgeom.i 𝐼 = (Itv‘𝐺)
tkgeom.g (𝜑𝐺 ∈ TarskiG)
tgbtwntriv2.1 (𝜑𝐴𝑃)
tgbtwntriv2.2 (𝜑𝐵𝑃)
tgbtwncom.3 (𝜑𝐶𝑃)
tgbtwncom.4 (𝜑𝐵 ∈ (𝐴𝐼𝐶))
Assertion
Ref Expression
tgbtwncom (𝜑𝐵 ∈ (𝐶𝐼𝐴))

Proof of Theorem tgbtwncom
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 tkgeom.p . . . 4 𝑃 = (Base‘𝐺)
2 tkgeom.d . . . 4 = (dist‘𝐺)
3 tkgeom.i . . . 4 𝐼 = (Itv‘𝐺)
4 tkgeom.g . . . . 5 (𝜑𝐺 ∈ TarskiG)
54ad2antrr 758 . . . 4 (((𝜑𝑥𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐺 ∈ TarskiG)
6 tgbtwntriv2.2 . . . . 5 (𝜑𝐵𝑃)
76ad2antrr 758 . . . 4 (((𝜑𝑥𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐵𝑃)
8 simplr 788 . . . 4 (((𝜑𝑥𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝑥𝑃)
9 simprl 790 . . . 4 (((𝜑𝑥𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝑥 ∈ (𝐵𝐼𝐵))
101, 2, 3, 5, 7, 8, 9axtgbtwnid 25110 . . 3 (((𝜑𝑥𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐵 = 𝑥)
11 simprr 792 . . 3 (((𝜑𝑥𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝑥 ∈ (𝐶𝐼𝐴))
1210, 11eqeltrd 2688 . 2 (((𝜑𝑥𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐵 ∈ (𝐶𝐼𝐴))
13 tgbtwntriv2.1 . . 3 (𝜑𝐴𝑃)
14 tgbtwncom.3 . . 3 (𝜑𝐶𝑃)
15 tgbtwncom.4 . . 3 (𝜑𝐵 ∈ (𝐴𝐼𝐶))
161, 2, 3, 4, 6, 14tgbtwntriv2 25127 . . 3 (𝜑𝐶 ∈ (𝐵𝐼𝐶))
171, 2, 3, 4, 13, 6, 14, 6, 14, 15, 16axtgpasch 25111 . 2 (𝜑 → ∃𝑥𝑃 (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴)))
1812, 17r19.29a 3060 1 (𝜑𝐵 ∈ (𝐶𝐼𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1475  wcel 1977  cfv 5790  (class class class)co 6527  Basecbs 15644  distcds 15726  TarskiGcstrkg 25074  Itvcitv 25080
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-nul 4712
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4368  df-br 4579  df-iota 5754  df-fv 5798  df-ov 6530  df-trkgc 25092  df-trkgb 25093  df-trkgcb 25094  df-trkg 25097
This theorem is referenced by:  tgbtwncomb  25129  tgbtwntriv1  25131  tgbtwnexch3  25134  tgbtwnexch2  25136  tgbtwnouttr  25137  tgbtwnexch  25138  tgtrisegint  25139  tgifscgr  25149  tgcgrxfr  25159  tgbtwnconn1lem1  25213  tgbtwnconn1lem2  25214  tgbtwnconn1lem3  25215  tgbtwnconn1  25216  tgbtwnconn3  25218  tgbtwnconn22  25220  tgbtwnconnln1  25221  tgbtwnconnln2  25222  legtri3  25231  legtrid  25232  legbtwn  25235  tgcgrsub2  25236  hlln  25248  btwnhl2  25254  btwnhl  25255  hlcgrex  25257  hlcgreulem  25258  tglineeltr  25272  mirreu3  25295  mirmir  25303  mireq  25306  miriso  25311  mirconn  25319  mirbtwnhl  25321  mirhl2  25322  mircgrextend  25323  miduniq  25326  colmid  25329  krippenlem  25331  krippen  25332  midexlem  25333  ragflat  25345  ragcgr  25348  footex  25359  colperpexlem1  25368  colperpexlem3  25370  mideulem2  25372  opphllem  25373  midex  25375  oppcom  25382  opphllem5  25389  opphllem6  25390  outpasch  25393  hlpasch  25394  lnopp2hpgb  25401  colhp  25408  midbtwn  25417  hypcgrlem1  25437  hypcgrlem2  25438  cgrabtwn  25463  cgracol  25465  dfcgra2  25467  sacgr  25468  oacgr  25469  inagswap  25476  inaghl  25477
  Copyright terms: Public domain W3C validator