Theorem tgbtwncom 28733

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 738	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐺 ∈ TarskiG)
6		tgbtwntriv2.2	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
7	6	ad2antrr 738	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐵 ∈ 𝑃)
8		simplr 780	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝑥 ∈ 𝑃)
9		simprl 782	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝑥 ∈ (𝐵𝐼𝐵))
10	1, 2, 3, 5, 7, 8, 9	axtgbtwnid 28711	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐵 = 𝑥)
11		simprr 784	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝑥 ∈ (𝐶𝐼𝐴))
12	10, 11	eqeltrd 2861	. 2 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐵 ∈ (𝐶𝐼𝐴))
13		tgbtwntriv2.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
14		tgbtwncom.3	. . 3 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
15		tgbtwncom.4	. . 3 ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))
16	1, 2, 3, 4, 6, 14	tgbtwntriv2 28732	. . 3 ⊢ (𝜑 → 𝐶 ∈ (𝐵𝐼𝐶))
17	1, 2, 3, 4, 13, 6, 14, 6, 14, 15, 16	axtgpasch 28712	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴)))
18	12, 17	r19.29a 3171	1 ⊢ (𝜑 → 𝐵 ∈ (𝐶𝐼𝐴))

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1568   ∈ wcel 2141  ‘cfv 6536  (class class class)co 7410  Basecbs 17268  distcds 17318  TarskiGcstrkg 28672  Itvcitv 28678

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5268

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3415  df-v 3455  df-sbc 3744  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-iota 6492  df-fv 6544  df-ov 7413  df-trkgc 28693  df-trkgb 28694  df-trkgcb 28695  df-trkg 28698

This theorem is referenced by:  tgbtwncomb  28734  tgbtwntriv1  28736  tgbtwnexch3  28739  tgbtwnexch2  28741  tgbtwnouttr  28742  tgbtwnexch  28743  tgtrisegint  28744  tgifscgr  28753  tgcgrxfr  28763  tgbtwnconn1lem1  28817  tgbtwnconn1lem2  28818  tgbtwnconn1lem3  28819  tgbtwnconn1  28820  tgbtwnconn3  28822  tgbtwnconn22  28824  tgbtwnconnln1  28825  tgbtwnconnln2  28826  legtri3  28835  legtrid  28836  legbtwn  28839  tgcgrsub2  28840  hlln  28855  btwnhl2  28861  btwnhl  28862  hlcgrex  28864  hlcgreulem  28865  tglineeltr  28880  mirreu3  28907  mirmir  28915  mireq  28918  miriso  28923  mirconn  28931  mirbtwnhl  28933  mirhl2  28934  mircgrextend  28935  miduniq  28938  colmid  28941  krippenlem  28943  krippen  28944  midexlem  28945  ragflat  28959  ragcgr  28962  footexALT  28973  footexlem1  28974  footexlem2  28975  colperpexlem1  28986  colperpexlem3  28988  mideulem2  28990  opphllem  28991  midex  28993  oppcom  29000  opphllem5  29007  opphllem6  29008  oppmir  29011  outpasch  29012  hlpasch  29013  lnopp2hpgb  29020  colhp  29027  lnincplng  29040  plngrotlem1  29043  plngrotlem2  29044  midbtwn  29062  hypcgrlem1  29082  hypcgrlem2  29083  flatcgra  29108  cgrabtwn  29110  cgracol  29112  dfcgra2  29114  sacgr  29115  oacgr  29116  ragsupplcgra  29121  inagswap  29131  inaghl  29135  prlngmolem1  29175