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 1094 | . . . 4 β’ ((π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ)) β (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ))) | |
3 | btwnlng1.p | . . . . . 6 β’ π = (BaseβπΊ) | |
4 | eqid 2736 | . . . . . 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 26892 | . . . . 5 β’ (π β (π β (ππΌπ) β π β (ππΌπ))) |
11 | 3, 4, 5, 6, 7, 9, 8 | tgbtwncomb 26892 | . . . . 5 β’ (π β (π β (ππΌπ) β π β (ππΌπ))) |
12 | 3, 4, 5, 6, 8, 7, 9 | tgbtwncomb 26892 | . . . . 5 β’ (π β (π β (ππΌπ) β π β (ππΌπ))) |
13 | 10, 11, 12 | 3orbi123d 1435 | . . . 4 β’ (π β ((π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ)) β (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ)))) |
14 | 2, 13 | bitrid 284 | . . 3 β’ (π β ((π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ)) β (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ)))) |
15 | btwnlng1.l | . . . 4 β’ πΏ = (LineGβπΊ) | |
16 | btwnlng1.d | . . . 4 β’ (π β π β π) | |
17 | 3, 15, 5, 6, 7, 9, 16, 8 | tgellng 26956 | . . 3 β’ (π β (π β (ππΏπ) β (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ)))) |
18 | 16 | necomd 2997 | . . . 4 β’ (π β π β π) |
19 | 3, 15, 5, 6, 9, 7, 18, 8 | tgellng 26956 | . . 3 β’ (π β (π β (ππΏπ) β (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ)))) |
20 | 14, 17, 19 | 3bitr4d 312 | . 2 β’ (π β (π β (ππΏπ) β π β (ππΏπ))) |
21 | 1, 20 | mpbird 258 | 1 β’ (π β π β (ππΏπ)) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 β¨ w3o 1086 = wceq 1539 β wcel 2104 β wne 2941 βcfv 6455 (class class class)co 7304 Basecbs 16954 distcds 17013 TarskiGcstrkg 26830 Itvcitv 26836 LineGclng 26837 |
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 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2707 ax-sep 5233 ax-nul 5240 ax-pr 5362 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 846 df-3or 1088 df-3an 1089 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2887 df-ne 2942 df-ral 3063 df-rex 3072 df-rab 3280 df-v 3440 df-sbc 3723 df-dif 3896 df-un 3898 df-in 3900 df-ss 3910 df-nul 4264 df-if 4467 df-pw 4542 df-sn 4567 df-pr 4569 df-op 4573 df-uni 4846 df-br 5083 df-opab 5145 df-id 5497 df-xp 5603 df-rel 5604 df-cnv 5605 df-co 5606 df-dm 5607 df-iota 6407 df-fun 6457 df-fv 6463 df-ov 7307 df-oprab 7308 df-mpo 7309 df-trkgc 26851 df-trkgb 26852 df-trkgcb 26853 df-trkg 26856 |
This theorem is referenced by: tglineelsb2 27035 tglinecom 27038 ncolncol 27049 coltr 27050 midexlem 27095 footexALT 27121 footexlem1 27122 footexlem2 27123 opphllem1 27150 opphllem2 27151 outpasch 27158 hlpasch 27159 trgcopy 27207 trgcopyeulem 27208 cgracgr 27221 tgasa1 27261 |
Copyright terms: Public domain | W3C validator |