Theorem tgbtwncom 28981

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.

Step	Hyp	Ref	Expression
1		tkgeom.p	. . . 4 ⊢ 𝑃 = (Base‘𝐺)
2		tkgeom.d	. . . 4 ⊢ − = (dist‘𝐺)
3		tkgeom.i	. . . 4 ⊢ 𝐼 = (Itv‘𝐺)
4		tkgeom.g	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
5	4	ad2antrr 739	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐺 ∈ TarskiG)
6		tgbtwntriv2.2	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
7	6	ad2antrr 739	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐵 ∈ 𝑃)
8		simplr 781	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝑥 ∈ 𝑃)
9		simprl 783	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝑥 ∈ (𝐵𝐼𝐵))
10	1, 2, 3, 5, 7, 8, 9	axtgbtwnid 28958	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐵 = 𝑥)
11		simprr 785	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝑥 ∈ (𝐶𝐼𝐴))
12	10, 11	eqeltrd 2864	. 2 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐵 ∈ (𝐶𝐼𝐴))
13		tgbtwntriv2.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
14		tgbtwncom.3	. . 3 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
15		tgbtwncom.4	. . 3 ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))
16	1, 2, 3, 4, 6, 14	tgbtwntriv2 28980	. . 3 ⊢ (𝜑 → 𝐶 ∈ (𝐵𝐼𝐶))
17	1, 2, 3, 4, 13, 6, 14, 6, 14, 15, 16	axtgpasch 28959	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴)))
18	12, 17	r19.29a 3174	1 ⊢ (𝜑 → 𝐵 ∈ (𝐶𝐼𝐴))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147  ‘cfv 6558  (class class class)co 7443  Basecbs 17416  distcds 17466  TarskiGcstrkg 28919  Itvcitv 28925

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5263

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6512  df-fv 6566  df-ov 7446  df-trkgc 28940  df-trkgb 28941  df-trkgcb 28942  df-trkg 28945

This theorem is used by:  tgbtwncomb  28982  tgbtwntriv1  28984  tgbtwnexch3  28987  tgbtwnexch2  28989  tgbtwnouttr  28990  tgbtwnexch  28991  tgtrisegint  28992  tgifscgr  29001  tgcgrxfr  29011  tgbtwnconn1lem1  29065  tgbtwnconn1lem2  29066  tgbtwnconn1lem3  29067  tgbtwnconn1  29068  tgbtwnconn3  29070  tgbtwnconn22  29072  tgbtwnconnln1  29073  tgbtwnconnln2  29074  legtri3  29083  legtrid  29084  legbtwn  29087  tgcgrsub2  29088  hlln  29103  btwnhl2  29109  btwnhl  29110  hlcgrex  29112  hlcgreulem  29113  tglineeltr  29129  mirreu3  29156  mirmir  29164  mireq  29167  miriso  29172  mirconn  29180  mirbtwnhl  29182  mirhl2  29183  mircgrextend  29184  miduniq  29187  colmid  29190  krippenlem  29192  krippen  29193  midexlem  29194  ragflat  29209  ragcgr  29212  footexALT  29223  footexlem1  29224  footexlem2  29225  colperpexlem1  29236  colperpexlem3  29238  mideulem2  29240  opphllem  29241  midex  29243  oppcom  29250  opphllem5  29257  opphllem6  29258  oppmir  29262  outpasch  29263  hlpasch  29264  lnopp2hpgb  29271  colhp  29278  lnincplng  29292  plngrotlem1  29295  plngrotlem2  29296  midbtwn  29314  hypcgrlem1  29335  hypcgrlem2  29336  flatcgra  29362  cgrabtwn  29364  cgracol  29366  dfcgra2  29368  sacgr  29369  oacgr  29370  ragsupplcgra  29375  tgaaddcpbllem1  29379  tgaaddcpbllem2  29380  tgaaddcpbl2  29383  inagswap  29390  inaghl  29394  angmgmaddov1lem  29416  angmgmaddov2lem  29417  angmgmaddcpbl  29420  prlngmolem1  29460  prlngsymquadopp  29473  inagbtwn  33078  tgextancd  33098  tgextahpl  33099  tgextalem1inag  33100  tgextamirnhl  33102  tgextaoa  33105  tgaasexc  33111