Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > lncom | Structured version Visualization version GIF version |
Description: Swapping the points defining a line keeps it unchanged. Part of Theorem 4.11 of [Schwabhauser] p. 34. (Contributed by Thierry Arnoux, 3-Apr-2019.) |
Ref | Expression |
---|---|
btwnlng1.p | ⊢ 𝑃 = (Base‘𝐺) |
btwnlng1.i | ⊢ 𝐼 = (Itv‘𝐺) |
btwnlng1.l | ⊢ 𝐿 = (LineG‘𝐺) |
btwnlng1.g | ⊢ (𝜑 → 𝐺 ∈ TarskiG) |
btwnlng1.x | ⊢ (𝜑 → 𝑋 ∈ 𝑃) |
btwnlng1.y | ⊢ (𝜑 → 𝑌 ∈ 𝑃) |
btwnlng1.z | ⊢ (𝜑 → 𝑍 ∈ 𝑃) |
btwnlng1.d | ⊢ (𝜑 → 𝑋 ≠ 𝑌) |
lncom.1 | ⊢ (𝜑 → 𝑍 ∈ (𝑌𝐿𝑋)) |
Ref | Expression |
---|---|
lncom | ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐿𝑌)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lncom.1 | . 2 ⊢ (𝜑 → 𝑍 ∈ (𝑌𝐿𝑋)) | |
2 | 3orcomb 1090 | . . . 4 ⊢ ((𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)) ↔ (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍) ∨ 𝑋 ∈ (𝑍𝐼𝑌))) | |
3 | btwnlng1.p | . . . . . 6 ⊢ 𝑃 = (Base‘𝐺) | |
4 | eqid 2824 | . . . . . 6 ⊢ (dist‘𝐺) = (dist‘𝐺) | |
5 | btwnlng1.i | . . . . . 6 ⊢ 𝐼 = (Itv‘𝐺) | |
6 | btwnlng1.g | . . . . . 6 ⊢ (𝜑 → 𝐺 ∈ TarskiG) | |
7 | btwnlng1.x | . . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑃) | |
8 | btwnlng1.z | . . . . . 6 ⊢ (𝜑 → 𝑍 ∈ 𝑃) | |
9 | btwnlng1.y | . . . . . 6 ⊢ (𝜑 → 𝑌 ∈ 𝑃) | |
10 | 3, 4, 5, 6, 7, 8, 9 | tgbtwncomb 26278 | . . . . 5 ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐼𝑌) ↔ 𝑍 ∈ (𝑌𝐼𝑋))) |
11 | 3, 4, 5, 6, 7, 9, 8 | tgbtwncomb 26278 | . . . . 5 ⊢ (𝜑 → (𝑌 ∈ (𝑋𝐼𝑍) ↔ 𝑌 ∈ (𝑍𝐼𝑋))) |
12 | 3, 4, 5, 6, 8, 7, 9 | tgbtwncomb 26278 | . . . . 5 ⊢ (𝜑 → (𝑋 ∈ (𝑍𝐼𝑌) ↔ 𝑋 ∈ (𝑌𝐼𝑍))) |
13 | 10, 11, 12 | 3orbi123d 1431 | . . . 4 ⊢ (𝜑 → ((𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍) ∨ 𝑋 ∈ (𝑍𝐼𝑌)) ↔ (𝑍 ∈ (𝑌𝐼𝑋) ∨ 𝑌 ∈ (𝑍𝐼𝑋) ∨ 𝑋 ∈ (𝑌𝐼𝑍)))) |
14 | 2, 13 | syl5bb 285 | . . 3 ⊢ (𝜑 → ((𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)) ↔ (𝑍 ∈ (𝑌𝐼𝑋) ∨ 𝑌 ∈ (𝑍𝐼𝑋) ∨ 𝑋 ∈ (𝑌𝐼𝑍)))) |
15 | btwnlng1.l | . . . 4 ⊢ 𝐿 = (LineG‘𝐺) | |
16 | btwnlng1.d | . . . 4 ⊢ (𝜑 → 𝑋 ≠ 𝑌) | |
17 | 3, 15, 5, 6, 7, 9, 16, 8 | tgellng 26342 | . . 3 ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐿𝑌) ↔ (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))) |
18 | 16 | necomd 3074 | . . . 4 ⊢ (𝜑 → 𝑌 ≠ 𝑋) |
19 | 3, 15, 5, 6, 9, 7, 18, 8 | tgellng 26342 | . . 3 ⊢ (𝜑 → (𝑍 ∈ (𝑌𝐿𝑋) ↔ (𝑍 ∈ (𝑌𝐼𝑋) ∨ 𝑌 ∈ (𝑍𝐼𝑋) ∨ 𝑋 ∈ (𝑌𝐼𝑍)))) |
20 | 14, 17, 19 | 3bitr4d 313 | . 2 ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐿𝑌) ↔ 𝑍 ∈ (𝑌𝐿𝑋))) |
21 | 1, 20 | mpbird 259 | 1 ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐿𝑌)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ w3o 1082 = wceq 1536 ∈ wcel 2113 ≠ wne 3019 ‘cfv 6358 (class class class)co 7159 Basecbs 16486 distcds 16577 TarskiGcstrkg 26219 Itvcitv 26225 LineGclng 26226 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 ax-sep 5206 ax-nul 5213 ax-pr 5333 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-mo 2621 df-eu 2653 df-clab 2803 df-cleq 2817 df-clel 2896 df-nfc 2966 df-ne 3020 df-ral 3146 df-rex 3147 df-rab 3150 df-v 3499 df-sbc 3776 df-dif 3942 df-un 3944 df-in 3946 df-ss 3955 df-nul 4295 df-if 4471 df-pw 4544 df-sn 4571 df-pr 4573 df-op 4577 df-uni 4842 df-br 5070 df-opab 5132 df-id 5463 df-xp 5564 df-rel 5565 df-cnv 5566 df-co 5567 df-dm 5568 df-iota 6317 df-fun 6360 df-fv 6366 df-ov 7162 df-oprab 7163 df-mpo 7164 df-trkgc 26237 df-trkgb 26238 df-trkgcb 26239 df-trkg 26242 |
This theorem is referenced by: tglineelsb2 26421 tglinecom 26424 ncolncol 26435 coltr 26436 midexlem 26481 footexALT 26507 footexlem1 26508 footexlem2 26509 opphllem1 26536 opphllem2 26537 outpasch 26544 hlpasch 26545 trgcopy 26593 trgcopyeulem 26594 cgracgr 26607 tgasa1 26647 |
Copyright terms: Public domain | W3C validator |