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

Theorem tgbtwncom 25428
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 762 . . . 4 (((𝜑𝑥𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐺 ∈ TarskiG)
6 tgbtwntriv2.2 . . . . 5 (𝜑𝐵𝑃)
76ad2antrr 762 . . . 4 (((𝜑𝑥𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐵𝑃)
8 simplr 807 . . . 4 (((𝜑𝑥𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝑥𝑃)
9 simprl 809 . . . 4 (((𝜑𝑥𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝑥 ∈ (𝐵𝐼𝐵))
101, 2, 3, 5, 7, 8, 9axtgbtwnid 25410 . . 3 (((𝜑𝑥𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐵 = 𝑥)
11 simprr 811 . . 3 (((𝜑𝑥𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝑥 ∈ (𝐶𝐼𝐴))
1210, 11eqeltrd 2730 . 2 (((𝜑𝑥𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐵 ∈ (𝐶𝐼𝐴))
13 tgbtwntriv2.1 . . 3 (𝜑𝐴𝑃)
14 tgbtwncom.3 . . 3 (𝜑𝐶𝑃)
15 tgbtwncom.4 . . 3 (𝜑𝐵 ∈ (𝐴𝐼𝐶))
161, 2, 3, 4, 6, 14tgbtwntriv2 25427 . . 3 (𝜑𝐶 ∈ (𝐵𝐼𝐶))
171, 2, 3, 4, 13, 6, 14, 6, 14, 15, 16axtgpasch 25411 . 2 (𝜑 → ∃𝑥𝑃 (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴)))
1812, 17r19.29a 3107 1 (𝜑𝐵 ∈ (𝐶𝐼𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1523  wcel 2030  cfv 5926  (class class class)co 6690  Basecbs 15904  distcds 15997  TarskiGcstrkg 25374  Itvcitv 25380
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-nul 4822
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693  df-trkgc 25392  df-trkgb 25393  df-trkgcb 25394  df-trkg 25397
This theorem is referenced by:  tgbtwncomb  25429  tgbtwntriv1  25431  tgbtwnexch3  25434  tgbtwnexch2  25436  tgbtwnouttr  25437  tgbtwnexch  25438  tgtrisegint  25439  tgifscgr  25448  tgcgrxfr  25458  tgbtwnconn1lem1  25512  tgbtwnconn1lem2  25513  tgbtwnconn1lem3  25514  tgbtwnconn1  25515  tgbtwnconn3  25517  tgbtwnconn22  25519  tgbtwnconnln1  25520  tgbtwnconnln2  25521  legtri3  25530  legtrid  25531  legbtwn  25534  tgcgrsub2  25535  hlln  25547  btwnhl2  25553  btwnhl  25554  hlcgrex  25556  hlcgreulem  25557  tglineeltr  25571  mirreu3  25594  mirmir  25602  mireq  25605  miriso  25610  mirconn  25618  mirbtwnhl  25620  mirhl2  25621  mircgrextend  25622  miduniq  25625  colmid  25628  krippenlem  25630  krippen  25631  midexlem  25632  ragflat  25644  ragcgr  25647  footex  25658  colperpexlem1  25667  colperpexlem3  25669  mideulem2  25671  opphllem  25672  midex  25674  oppcom  25681  opphllem5  25688  opphllem6  25689  outpasch  25692  hlpasch  25693  lnopp2hpgb  25700  colhp  25707  midbtwn  25716  hypcgrlem1  25736  hypcgrlem2  25737  cgrabtwn  25762  cgracol  25764  dfcgra2  25766  sacgr  25767  oacgr  25768  inagswap  25775  inaghl  25776
  Copyright terms: Public domain W3C validator