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

Theorem tgbtwncom 23600
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 725 . . . 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 725 . . . 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 755 . . . 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 23584 . . 3  |-  ( ( ( ph  /\  x  e.  P )  /\  (
x  e.  ( B I B )  /\  x  e.  ( C I A ) ) )  ->  B  =  x )
11 simprr 756 . . 3  |-  ( ( ( ph  /\  x  e.  P )  /\  (
x  e.  ( B I B )  /\  x  e.  ( C I A ) ) )  ->  x  e.  ( C I A ) )
1210, 11eqeltrd 2548 . 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 23599 . . 3  |-  ( ph  ->  C  e.  ( B I C ) )
171, 2, 3, 4, 13, 6, 14, 6, 14, 15, 16axtgpasch 23585 . 2  |-  ( ph  ->  E. x  e.  P  ( x  e.  ( B I B )  /\  x  e.  ( C I A ) ) )
1812, 17r19.29a 2996 1  |-  ( ph  ->  B  e.  ( C I A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1374    e. wcel 1762   ` cfv 5579  (class class class)co 6275   Basecbs 14479   distcds 14553  TarskiGcstrkg 23546  Itvcitv 23553
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-nul 4569
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-sbc 3325  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-pw 4005  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-iota 5542  df-fv 5587  df-ov 6278  df-trkgc 23565  df-trkgb 23566  df-trkgcb 23567  df-trkg 23571
This theorem is referenced by:  tgbtwncomb  23601  tgbtwntriv1  23603  tgbtwnexch3  23606  tgbtwnexch2  23608  tgbtwnouttr  23609  tgbtwnexch  23610  tgtrisegint  23611  tgifscgr  23621  tgcgrxfr  23630  tgbtwnconn1lem1  23679  tgbtwnconn1lem2  23680  tgbtwnconn1lem3  23681  tgbtwnconn1  23682  tgbtwnconn3  23684  tgbtwnconn22  23686  tgbtwnconnln1  23687  tgbtwnconnln2  23688  legtri3  23697  legtrid  23698  legbtwn  23701  tglineeltr  23718  mirreu3  23741  mirmir  23749  mireq  23752  miriso  23756  miduniq  23763  colmid  23766  krippenlem  23768  krippen  23769  midexlem  23770  ragflat  23782  ragcgr  23785  footex  23796  colperpexlem1  23802  colperpexlem3  23804  mideulem  23806  mideu  23807  midbtwn  23815  hypcgrlem1  23834  hypcgrlem2  23835
  Copyright terms: Public domain W3C validator