![]() |
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 719 | . . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐺 ∈ TarskiG) |
6 | tgbtwntriv2.2 | . . . . 5 ⊢ (𝜑 → 𝐵 ∈ 𝑃) | |
7 | 6 | ad2antrr 719 | . . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐵 ∈ 𝑃) |
8 | simplr 787 | . . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝑥 ∈ 𝑃) | |
9 | simprl 789 | . . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝑥 ∈ (𝐵𝐼𝐵)) | |
10 | 1, 2, 3, 5, 7, 8, 9 | axtgbtwnid 25778 | . . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐵 = 𝑥) |
11 | simprr 791 | . . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝑥 ∈ (𝐶𝐼𝐴)) | |
12 | 10, 11 | eqeltrd 2906 | . 2 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) → 𝐵 ∈ (𝐶𝐼𝐴)) |
13 | tgbtwntriv2.1 | . . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑃) | |
14 | tgbtwncom.3 | . . 3 ⊢ (𝜑 → 𝐶 ∈ 𝑃) | |
15 | tgbtwncom.4 | . . 3 ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) | |
16 | 1, 2, 3, 4, 6, 14 | tgbtwntriv2 25799 | . . 3 ⊢ (𝜑 → 𝐶 ∈ (𝐵𝐼𝐶)) |
17 | 1, 2, 3, 4, 13, 6, 14, 6, 14, 15, 16 | axtgpasch 25779 | . 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐵𝐼𝐵) ∧ 𝑥 ∈ (𝐶𝐼𝐴))) |
18 | 12, 17 | r19.29a 3288 | 1 ⊢ (𝜑 → 𝐵 ∈ (𝐶𝐼𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 = wceq 1658 ∈ wcel 2166 ‘cfv 6123 (class class class)co 6905 Basecbs 16222 distcds 16314 TarskiGcstrkg 25742 Itvcitv 25748 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2803 ax-nul 5013 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2605 df-eu 2640 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-ral 3122 df-rex 3123 df-rab 3126 df-v 3416 df-sbc 3663 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-nul 4145 df-if 4307 df-pw 4380 df-sn 4398 df-pr 4400 df-op 4404 df-uni 4659 df-br 4874 df-iota 6086 df-fv 6131 df-ov 6908 df-trkgc 25760 df-trkgb 25761 df-trkgcb 25762 df-trkg 25765 |
This theorem is referenced by: tgbtwncomb 25801 tgbtwntriv1 25803 tgbtwnexch3 25806 tgbtwnexch2 25808 tgbtwnouttr 25809 tgbtwnexch 25810 tgtrisegint 25811 tgifscgr 25820 tgcgrxfr 25830 tgbtwnconn1lem1 25884 tgbtwnconn1lem2 25885 tgbtwnconn1lem3 25886 tgbtwnconn1 25887 tgbtwnconn3 25889 tgbtwnconn22 25891 tgbtwnconnln1 25892 tgbtwnconnln2 25893 legtri3 25902 legtrid 25903 legbtwn 25906 tgcgrsub2 25907 hlln 25919 btwnhl2 25925 btwnhl 25926 hlcgrex 25928 hlcgreulem 25929 tglineeltr 25943 mirreu3 25966 mirmir 25974 mireq 25977 miriso 25982 mirconn 25990 mirbtwnhl 25992 mirhl2 25993 mircgrextend 25994 miduniq 25997 colmid 26000 krippenlem 26002 krippen 26003 midexlem 26004 ragflat 26016 ragcgr 26019 footex 26030 colperpexlem1 26039 colperpexlem3 26041 mideulem2 26043 opphllem 26044 midex 26046 oppcom 26053 opphllem5 26060 opphllem6 26061 outpasch 26064 hlpasch 26065 lnopp2hpgb 26072 colhp 26079 midbtwn 26088 hypcgrlem1 26108 hypcgrlem2 26109 cgrabtwn 26134 cgracol 26136 dfcgra2 26138 sacgr 26139 sacgrOLD 26140 oacgr 26141 inagswap 26148 inaghl 26149 |
Copyright terms: Public domain | W3C validator |