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

Theorem tgbtwncom 28291
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 725 . . . 4 (((𝜑𝑥𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐺 ∈ TarskiG)
6 tgbtwntriv2.2 . . . . 5 (𝜑𝐵𝑃)
76ad2antrr 725 . . . 4 (((𝜑𝑥𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐵𝑃)
8 simplr 768 . . . 4 (((𝜑𝑥𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝑥𝑃)
9 simprl 770 . . . 4 (((𝜑𝑥𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝑥 ∈ (𝐵𝐼𝐵))
101, 2, 3, 5, 7, 8, 9axtgbtwnid 28269 . . 3 (((𝜑𝑥𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐵 = 𝑥)
11 simprr 772 . . 3 (((𝜑𝑥𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝑥 ∈ (𝐶𝐼𝐴))
1210, 11eqeltrd 2829 . 2 (((𝜑𝑥𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐵 ∈ (𝐶𝐼𝐴))
13 tgbtwntriv2.1 . . 3 (𝜑𝐴𝑃)
14 tgbtwncom.3 . . 3 (𝜑𝐶𝑃)
15 tgbtwncom.4 . . 3 (𝜑𝐵 ∈ (𝐴𝐼𝐶))
161, 2, 3, 4, 6, 14tgbtwntriv2 28290 . . 3 (𝜑𝐶 ∈ (𝐵𝐼𝐶))
171, 2, 3, 4, 13, 6, 14, 6, 14, 15, 16axtgpasch 28270 . 2 (𝜑 → ∃𝑥𝑃 (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴)))
1812, 17r19.29a 3159 1 (𝜑𝐵 ∈ (𝐶𝐼𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1534  wcel 2099  cfv 6548  (class class class)co 7420  Basecbs 17179  distcds 17241  TarskiGcstrkg 28230  Itvcitv 28236
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-nul 5306
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3430  df-v 3473  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-iota 6500  df-fv 6556  df-ov 7423  df-trkgc 28251  df-trkgb 28252  df-trkgcb 28253  df-trkg 28256
This theorem is referenced by:  tgbtwncomb  28292  tgbtwntriv1  28294  tgbtwnexch3  28297  tgbtwnexch2  28299  tgbtwnouttr  28300  tgbtwnexch  28301  tgtrisegint  28302  tgifscgr  28311  tgcgrxfr  28321  tgbtwnconn1lem1  28375  tgbtwnconn1lem2  28376  tgbtwnconn1lem3  28377  tgbtwnconn1  28378  tgbtwnconn3  28380  tgbtwnconn22  28382  tgbtwnconnln1  28383  tgbtwnconnln2  28384  legtri3  28393  legtrid  28394  legbtwn  28397  tgcgrsub2  28398  hlln  28410  btwnhl2  28416  btwnhl  28417  hlcgrex  28419  hlcgreulem  28420  tglineeltr  28434  mirreu3  28457  mirmir  28465  mireq  28468  miriso  28473  mirconn  28481  mirbtwnhl  28483  mirhl2  28484  mircgrextend  28485  miduniq  28488  colmid  28491  krippenlem  28493  krippen  28494  midexlem  28495  ragflat  28507  ragcgr  28510  footexALT  28521  footexlem1  28522  footexlem2  28523  colperpexlem1  28533  colperpexlem3  28535  mideulem2  28537  opphllem  28538  midex  28540  oppcom  28547  opphllem5  28554  opphllem6  28555  outpasch  28558  hlpasch  28559  lnopp2hpgb  28566  colhp  28573  midbtwn  28582  hypcgrlem1  28602  hypcgrlem2  28603  flatcgra  28627  cgrabtwn  28629  cgracol  28631  dfcgra2  28633  sacgr  28634  oacgr  28635  inagswap  28644  inaghl  28648
  Copyright terms: Public domain W3C validator