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

Theorem tgbtwncom 24260
Description: Betweeness commutes. Theorem 3.2 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 15-Mar-2019.)
Hypotheses
Ref Expression
tkgeom.p  |-  P  =  ( Base `  G
)
tkgeom.d  |-  .-  =  ( dist `  G )
tkgeom.i  |-  I  =  (Itv `  G )
tkgeom.g  |-  ( ph  ->  G  e. TarskiG )
tgbtwntriv2.1  |-  ( ph  ->  A  e.  P )
tgbtwntriv2.2  |-  ( ph  ->  B  e.  P )
tgbtwncom.3  |-  ( ph  ->  C  e.  P )
tgbtwncom.4  |-  ( ph  ->  B  e.  ( A I C ) )
Assertion
Ref Expression
tgbtwncom  |-  ( ph  ->  B  e.  ( C I A ) )

Proof of Theorem tgbtwncom
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 tkgeom.p . . . 4  |-  P  =  ( Base `  G
)
2 tkgeom.d . . . 4  |-  .-  =  ( dist `  G )
3 tkgeom.i . . . 4  |-  I  =  (Itv `  G )
4 tkgeom.g . . . . 5  |-  ( ph  ->  G  e. TarskiG )
54ad2antrr 724 . . . 4  |-  ( ( ( ph  /\  x  e.  P )  /\  (
x  e.  ( B I B )  /\  x  e.  ( C I A ) ) )  ->  G  e. TarskiG )
6 tgbtwntriv2.2 . . . . 5  |-  ( ph  ->  B  e.  P )
76ad2antrr 724 . . . 4  |-  ( ( ( ph  /\  x  e.  P )  /\  (
x  e.  ( B I B )  /\  x  e.  ( C I A ) ) )  ->  B  e.  P
)
8 simplr 754 . . . 4  |-  ( ( ( ph  /\  x  e.  P )  /\  (
x  e.  ( B I B )  /\  x  e.  ( C I A ) ) )  ->  x  e.  P
)
9 simprl 756 . . . 4  |-  ( ( ( ph  /\  x  e.  P )  /\  (
x  e.  ( B I B )  /\  x  e.  ( C I A ) ) )  ->  x  e.  ( B I B ) )
101, 2, 3, 5, 7, 8, 9axtgbtwnid 24242 . . 3  |-  ( ( ( ph  /\  x  e.  P )  /\  (
x  e.  ( B I B )  /\  x  e.  ( C I A ) ) )  ->  B  =  x )
11 simprr 758 . . 3  |-  ( ( ( ph  /\  x  e.  P )  /\  (
x  e.  ( B I B )  /\  x  e.  ( C I A ) ) )  ->  x  e.  ( C I A ) )
1210, 11eqeltrd 2490 . 2  |-  ( ( ( ph  /\  x  e.  P )  /\  (
x  e.  ( B I B )  /\  x  e.  ( C I A ) ) )  ->  B  e.  ( C I A ) )
13 tgbtwntriv2.1 . . 3  |-  ( ph  ->  A  e.  P )
14 tgbtwncom.3 . . 3  |-  ( ph  ->  C  e.  P )
15 tgbtwncom.4 . . 3  |-  ( ph  ->  B  e.  ( A I C ) )
161, 2, 3, 4, 6, 14tgbtwntriv2 24259 . . 3  |-  ( ph  ->  C  e.  ( B I C ) )
171, 2, 3, 4, 13, 6, 14, 6, 14, 15, 16axtgpasch 24243 . 2  |-  ( ph  ->  E. x  e.  P  ( x  e.  ( B I B )  /\  x  e.  ( C I A ) ) )
1812, 17r19.29a 2949 1  |-  ( ph  ->  B  e.  ( C I A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1405    e. wcel 1842   ` cfv 5569  (class class class)co 6278   Basecbs 14841   distcds 14918  TarskiGcstrkg 24206  Itvcitv 24212
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-nul 4525
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2759  df-rex 2760  df-rab 2763  df-v 3061  df-sbc 3278  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-pw 3957  df-sn 3973  df-pr 3975  df-op 3979  df-uni 4192  df-br 4396  df-iota 5533  df-fv 5577  df-ov 6281  df-trkgc 24224  df-trkgb 24225  df-trkgcb 24226  df-trkg 24229
This theorem is referenced by:  tgbtwncomb  24261  tgbtwntriv1  24263  tgbtwnexch3  24266  tgbtwnexch2  24268  tgbtwnouttr  24269  tgbtwnexch  24270  tgtrisegint  24271  tgifscgr  24281  tgcgrxfr  24290  tgbtwnconn1lem1  24342  tgbtwnconn1lem2  24343  tgbtwnconn1lem3  24344  tgbtwnconn1  24345  tgbtwnconn3  24347  tgbtwnconn22  24349  tgbtwnconnln1  24350  tgbtwnconnln2  24351  legtri3  24360  legtrid  24361  legbtwn  24364  tgcgrsub2  24365  hlln  24375  btwnhl2  24381  btwnhl  24382  hlcgrex  24383  tglineeltr  24396  mirreu3  24420  mirmir  24428  mireq  24431  miriso  24435  mirconn  24443  mirbtwnhl  24445  mirhl2  24446  miduniq  24448  colmid  24451  krippenlem  24453  krippen  24454  midexlem  24455  ragflat  24467  ragcgr  24470  footex  24481  colperpexlem1  24490  colperpexlem3  24492  mideulem2  24494  opphllem  24495  midex  24497  oppcom  24503  opphllem5  24510  opphllem6  24511  lnopp2hpgb  24520  colhp  24527  midbtwn  24535  hypcgrlem1  24555  hypcgrlem2  24556  dfcgra2  24579
  Copyright terms: Public domain W3C validator