![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > tgbtwncom | Structured version Visualization version GIF version |
Description: Betweenness commutes. Theorem 3.2 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 15-Mar-2019.) |
Ref | Expression |
---|---|
tkgeom.p | ⊢ 𝑃 = (Base‘𝐺) |
tkgeom.d | ⊢ − = (dist‘𝐺) |
tkgeom.i | ⊢ 𝐼 = (Itv‘𝐺) |
tkgeom.g | ⊢ (𝜑 → 𝐺 ∈ TarskiG) |
tgbtwntriv2.1 | ⊢ (𝜑 → 𝐴 ∈ 𝑃) |
tgbtwntriv2.2 | ⊢ (𝜑 → 𝐵 ∈ 𝑃) |
tgbtwncom.3 | ⊢ (𝜑 → 𝐶 ∈ 𝑃) |
tgbtwncom.4 | ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) |
Ref | Expression |
---|---|
tgbtwncom | ⊢ (𝜑 → 𝐵 ∈ (𝐶𝐼𝐴)) |
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 725 | . . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐺 ∈ TarskiG) |
6 | tgbtwntriv2.2 | . . . . 5 ⊢ (𝜑 → 𝐵 ∈ 𝑃) | |
7 | 6 | ad2antrr 725 | . . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐵 ∈ 𝑃) |
8 | simplr 768 | . . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝑥 ∈ 𝑃) | |
9 | simprl 770 | . . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝑥 ∈ (𝐵𝐼𝐵)) | |
10 | 1, 2, 3, 5, 7, 8, 9 | axtgbtwnid 28269 | . . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐵 = 𝑥) |
11 | simprr 772 | . . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝑥 ∈ (𝐶𝐼𝐴)) | |
12 | 10, 11 | eqeltrd 2829 | . 2 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐵 ∈ (𝐶𝐼𝐴)) |
13 | tgbtwntriv2.1 | . . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑃) | |
14 | tgbtwncom.3 | . . 3 ⊢ (𝜑 → 𝐶 ∈ 𝑃) | |
15 | tgbtwncom.4 | . . 3 ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) | |
16 | 1, 2, 3, 4, 6, 14 | tgbtwntriv2 28290 | . . 3 ⊢ (𝜑 → 𝐶 ∈ (𝐵𝐼𝐶)) |
17 | 1, 2, 3, 4, 13, 6, 14, 6, 14, 15, 16 | axtgpasch 28270 | . 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) |
18 | 12, 17 | r19.29a 3159 | 1 ⊢ (𝜑 → 𝐵 ∈ (𝐶𝐼𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 = wceq 1534 ∈ wcel 2099 ‘cfv 6548 (class class class)co 7420 Basecbs 17179 distcds 17241 TarskiGcstrkg 28230 Itvcitv 28236 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 ax-nul 5306 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-ne 2938 df-ral 3059 df-rex 3068 df-rab 3430 df-v 3473 df-sbc 3777 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4909 df-br 5149 df-iota 6500 df-fv 6556 df-ov 7423 df-trkgc 28251 df-trkgb 28252 df-trkgcb 28253 df-trkg 28256 |
This theorem is referenced by: tgbtwncomb 28292 tgbtwntriv1 28294 tgbtwnexch3 28297 tgbtwnexch2 28299 tgbtwnouttr 28300 tgbtwnexch 28301 tgtrisegint 28302 tgifscgr 28311 tgcgrxfr 28321 tgbtwnconn1lem1 28375 tgbtwnconn1lem2 28376 tgbtwnconn1lem3 28377 tgbtwnconn1 28378 tgbtwnconn3 28380 tgbtwnconn22 28382 tgbtwnconnln1 28383 tgbtwnconnln2 28384 legtri3 28393 legtrid 28394 legbtwn 28397 tgcgrsub2 28398 hlln 28410 btwnhl2 28416 btwnhl 28417 hlcgrex 28419 hlcgreulem 28420 tglineeltr 28434 mirreu3 28457 mirmir 28465 mireq 28468 miriso 28473 mirconn 28481 mirbtwnhl 28483 mirhl2 28484 mircgrextend 28485 miduniq 28488 colmid 28491 krippenlem 28493 krippen 28494 midexlem 28495 ragflat 28507 ragcgr 28510 footexALT 28521 footexlem1 28522 footexlem2 28523 colperpexlem1 28533 colperpexlem3 28535 mideulem2 28537 opphllem 28538 midex 28540 oppcom 28547 opphllem5 28554 opphllem6 28555 outpasch 28558 hlpasch 28559 lnopp2hpgb 28566 colhp 28573 midbtwn 28582 hypcgrlem1 28602 hypcgrlem2 28603 flatcgra 28627 cgrabtwn 28629 cgracol 28631 dfcgra2 28633 sacgr 28634 oacgr 28635 inagswap 28644 inaghl 28648 |
Copyright terms: Public domain | W3C validator |