Theorem tgbtwncom 28544

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 727	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐺 ∈ TarskiG)
6		tgbtwntriv2.2	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
7	6	ad2antrr 727	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐵 ∈ 𝑃)
8		simplr 769	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝑥 ∈ 𝑃)
9		simprl 771	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝑥 ∈ (𝐵𝐼𝐵))
10	1, 2, 3, 5, 7, 8, 9	axtgbtwnid 28522	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐵 = 𝑥)
11		simprr 773	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝑥 ∈ (𝐶𝐼𝐴))
12	10, 11	eqeltrd 2835	. 2 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐵 ∈ (𝐶𝐼𝐴))
13		tgbtwntriv2.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
14		tgbtwncom.3	. . 3 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
15		tgbtwncom.4	. . 3 ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))
16	1, 2, 3, 4, 6, 14	tgbtwntriv2 28543	. . 3 ⊢ (𝜑 → 𝐶 ∈ (𝐵𝐼𝐶))
17	1, 2, 3, 4, 13, 6, 14, 6, 14, 15, 16	axtgpasch 28523	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴)))
18	12, 17	r19.29a 3143	1 ⊢ (𝜑 → 𝐵 ∈ (𝐶𝐼𝐴))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ‘cfv 6487  (class class class)co 7356  Basecbs 17168  distcds 17218  TarskiGcstrkg 28483  Itvcitv 28489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707  ax-nul 5230

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-ne 2931  df-ral 3050  df-rex 3060  df-rab 3388  df-v 3429  df-sbc 3726  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-iota 6443  df-fv 6495  df-ov 7359  df-trkgc 28504  df-trkgb 28505  df-trkgcb 28506  df-trkg 28509

This theorem is referenced by:  tgbtwncomb  28545  tgbtwntriv1  28547  tgbtwnexch3  28550  tgbtwnexch2  28552  tgbtwnouttr  28553  tgbtwnexch  28554  tgtrisegint  28555  tgifscgr  28564  tgcgrxfr  28574  tgbtwnconn1lem1  28628  tgbtwnconn1lem2  28629  tgbtwnconn1lem3  28630  tgbtwnconn1  28631  tgbtwnconn3  28633  tgbtwnconn22  28635  tgbtwnconnln1  28636  tgbtwnconnln2  28637  legtri3  28646  legtrid  28647  legbtwn  28650  tgcgrsub2  28651  hlln  28663  btwnhl2  28669  btwnhl  28670  hlcgrex  28672  hlcgreulem  28673  tglineeltr  28687  mirreu3  28710  mirmir  28718  mireq  28721  miriso  28726  mirconn  28734  mirbtwnhl  28736  mirhl2  28737  mircgrextend  28738  miduniq  28741  colmid  28744  krippenlem  28746  krippen  28747  midexlem  28748  ragflat  28760  ragcgr  28763  footexALT  28774  footexlem1  28775  footexlem2  28776  colperpexlem1  28786  colperpexlem3  28788  mideulem2  28790  opphllem  28791  midex  28793  oppcom  28800  opphllem5  28807  opphllem6  28808  outpasch  28811  hlpasch  28812  lnopp2hpgb  28819  colhp  28826  midbtwn  28835  hypcgrlem1  28855  hypcgrlem2  28856  flatcgra  28880  cgrabtwn  28882  cgracol  28884  dfcgra2  28886  sacgr  28887  oacgr  28888  inagswap  28897  inaghl  28901