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 762 | . . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐺 ∈ TarskiG) |
6 | tgbtwntriv2.2 | . . . . 5 ⊢ (𝜑 → 𝐵 ∈ 𝑃) | |
7 | 6 | ad2antrr 762 | . . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐵 ∈ 𝑃) |
8 | simplr 792 | . . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝑥 ∈ 𝑃) | |
9 | simprl 794 | . . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝑥 ∈ (𝐵𝐼𝐵)) | |
10 | 1, 2, 3, 5, 7, 8, 9 | axtgbtwnid 25365 | . . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐵 = 𝑥) |
11 | simprr 796 | . . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝑥 ∈ (𝐶𝐼𝐴)) | |
12 | 10, 11 | eqeltrd 2701 | . 2 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐵 ∈ (𝐶𝐼𝐴)) |
13 | tgbtwntriv2.1 | . . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑃) | |
14 | tgbtwncom.3 | . . 3 ⊢ (𝜑 → 𝐶 ∈ 𝑃) | |
15 | tgbtwncom.4 | . . 3 ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) | |
16 | 1, 2, 3, 4, 6, 14 | tgbtwntriv2 25382 | . . 3 ⊢ (𝜑 → 𝐶 ∈ (𝐵𝐼𝐶)) |
17 | 1, 2, 3, 4, 13, 6, 14, 6, 14, 15, 16 | axtgpasch 25366 | . 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) |
18 | 12, 17 | r19.29a 3078 | 1 ⊢ (𝜑 → 𝐵 ∈ (𝐶𝐼𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 = wceq 1483 ∈ wcel 1990 ‘cfv 5888 (class class class)co 6650 Basecbs 15857 distcds 15950 TarskiGcstrkg 25329 Itvcitv 25335 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-nul 4789 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-sbc 3436 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-iota 5851 df-fv 5896 df-ov 6653 df-trkgc 25347 df-trkgb 25348 df-trkgcb 25349 df-trkg 25352 |
This theorem is referenced by: tgbtwncomb 25384 tgbtwntriv1 25386 tgbtwnexch3 25389 tgbtwnexch2 25391 tgbtwnouttr 25392 tgbtwnexch 25393 tgtrisegint 25394 tgifscgr 25403 tgcgrxfr 25413 tgbtwnconn1lem1 25467 tgbtwnconn1lem2 25468 tgbtwnconn1lem3 25469 tgbtwnconn1 25470 tgbtwnconn3 25472 tgbtwnconn22 25474 tgbtwnconnln1 25475 tgbtwnconnln2 25476 legtri3 25485 legtrid 25486 legbtwn 25489 tgcgrsub2 25490 hlln 25502 btwnhl2 25508 btwnhl 25509 hlcgrex 25511 hlcgreulem 25512 tglineeltr 25526 mirreu3 25549 mirmir 25557 mireq 25560 miriso 25565 mirconn 25573 mirbtwnhl 25575 mirhl2 25576 mircgrextend 25577 miduniq 25580 colmid 25583 krippenlem 25585 krippen 25586 midexlem 25587 ragflat 25599 ragcgr 25602 footex 25613 colperpexlem1 25622 colperpexlem3 25624 mideulem2 25626 opphllem 25627 midex 25629 oppcom 25636 opphllem5 25643 opphllem6 25644 outpasch 25647 hlpasch 25648 lnopp2hpgb 25655 colhp 25662 midbtwn 25671 hypcgrlem1 25691 hypcgrlem2 25692 cgrabtwn 25717 cgracol 25719 dfcgra2 25721 sacgr 25722 oacgr 25723 inagswap 25730 inaghl 25731 |
Copyright terms: Public domain | W3C validator |