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

Theorem tgbtwncom 26277
 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 724 . . . 4 (((𝜑𝑥𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐺 ∈ TarskiG)
6 tgbtwntriv2.2 . . . . 5 (𝜑𝐵𝑃)
76ad2antrr 724 . . . 4 (((𝜑𝑥𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐵𝑃)
8 simplr 767 . . . 4 (((𝜑𝑥𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝑥𝑃)
9 simprl 769 . . . 4 (((𝜑𝑥𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝑥 ∈ (𝐵𝐼𝐵))
101, 2, 3, 5, 7, 8, 9axtgbtwnid 26255 . . 3 (((𝜑𝑥𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐵 = 𝑥)
11 simprr 771 . . 3 (((𝜑𝑥𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝑥 ∈ (𝐶𝐼𝐴))
1210, 11eqeltrd 2916 . 2 (((𝜑𝑥𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐵 ∈ (𝐶𝐼𝐴))
13 tgbtwntriv2.1 . . 3 (𝜑𝐴𝑃)
14 tgbtwncom.3 . . 3 (𝜑𝐶𝑃)
15 tgbtwncom.4 . . 3 (𝜑𝐵 ∈ (𝐴𝐼𝐶))
161, 2, 3, 4, 6, 14tgbtwntriv2 26276 . . 3 (𝜑𝐶 ∈ (𝐵𝐼𝐶))
171, 2, 3, 4, 13, 6, 14, 6, 14, 15, 16axtgpasch 26256 . 2 (𝜑 → ∃𝑥𝑃 (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴)))
1812, 17r19.29a 3292 1 (𝜑𝐵 ∈ (𝐶𝐼𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398   = wceq 1536   ∈ wcel 2113  ‘cfv 6358  (class class class)co 7159  Basecbs 16486  distcds 16577  TarskiGcstrkg 26219  Itvcitv 26225 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-nul 5213 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ral 3146  df-rex 3147  df-rab 3150  df-v 3499  df-sbc 3776  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-br 5070  df-iota 6317  df-fv 6366  df-ov 7162  df-trkgc 26237  df-trkgb 26238  df-trkgcb 26239  df-trkg 26242 This theorem is referenced by:  tgbtwncomb  26278  tgbtwntriv1  26280  tgbtwnexch3  26283  tgbtwnexch2  26285  tgbtwnouttr  26286  tgbtwnexch  26287  tgtrisegint  26288  tgifscgr  26297  tgcgrxfr  26307  tgbtwnconn1lem1  26361  tgbtwnconn1lem2  26362  tgbtwnconn1lem3  26363  tgbtwnconn1  26364  tgbtwnconn3  26366  tgbtwnconn22  26368  tgbtwnconnln1  26369  tgbtwnconnln2  26370  legtri3  26379  legtrid  26380  legbtwn  26383  tgcgrsub2  26384  hlln  26396  btwnhl2  26402  btwnhl  26403  hlcgrex  26405  hlcgreulem  26406  tglineeltr  26420  mirreu3  26443  mirmir  26451  mireq  26454  miriso  26459  mirconn  26467  mirbtwnhl  26469  mirhl2  26470  mircgrextend  26471  miduniq  26474  colmid  26477  krippenlem  26479  krippen  26480  midexlem  26481  ragflat  26493  ragcgr  26496  footexALT  26507  footexlem1  26508  footexlem2  26509  colperpexlem1  26519  colperpexlem3  26521  mideulem2  26523  opphllem  26524  midex  26526  oppcom  26533  opphllem5  26540  opphllem6  26541  outpasch  26544  hlpasch  26545  lnopp2hpgb  26552  colhp  26559  midbtwn  26568  hypcgrlem1  26588  hypcgrlem2  26589  flatcgra  26613  cgrabtwn  26615  cgracol  26617  dfcgra2  26619  sacgr  26620  oacgr  26621  inagswap  26630  inaghl  26634
 Copyright terms: Public domain W3C validator