MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lncom Structured version   Visualization version   GIF version

Theorem lncom 27025
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.)
Hypotheses
Ref Expression
btwnlng1.p 𝑃 = (Baseβ€˜πΊ)
btwnlng1.i 𝐼 = (Itvβ€˜πΊ)
btwnlng1.l 𝐿 = (LineGβ€˜πΊ)
btwnlng1.g (πœ‘ β†’ 𝐺 ∈ TarskiG)
btwnlng1.x (πœ‘ β†’ 𝑋 ∈ 𝑃)
btwnlng1.y (πœ‘ β†’ π‘Œ ∈ 𝑃)
btwnlng1.z (πœ‘ β†’ 𝑍 ∈ 𝑃)
btwnlng1.d (πœ‘ β†’ 𝑋 β‰  π‘Œ)
lncom.1 (πœ‘ β†’ 𝑍 ∈ (π‘ŒπΏπ‘‹))
Assertion
Ref Expression
lncom (πœ‘ β†’ 𝑍 ∈ (π‘‹πΏπ‘Œ))

Proof of Theorem lncom
StepHypRef 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 (πœ‘ β†’ π‘Œ ∈ 𝑃)
103, 4, 5, 6, 7, 8, 9tgbtwncomb 26892 . . . . 5 (πœ‘ β†’ (𝑍 ∈ (π‘‹πΌπ‘Œ) ↔ 𝑍 ∈ (π‘ŒπΌπ‘‹)))
113, 4, 5, 6, 7, 9, 8tgbtwncomb 26892 . . . . 5 (πœ‘ β†’ (π‘Œ ∈ (𝑋𝐼𝑍) ↔ π‘Œ ∈ (𝑍𝐼𝑋)))
123, 4, 5, 6, 8, 7, 9tgbtwncomb 26892 . . . . 5 (πœ‘ β†’ (𝑋 ∈ (π‘πΌπ‘Œ) ↔ 𝑋 ∈ (π‘ŒπΌπ‘)))
1310, 11, 123orbi123d 1435 . . . 4 (πœ‘ β†’ ((𝑍 ∈ (π‘‹πΌπ‘Œ) ∨ π‘Œ ∈ (𝑋𝐼𝑍) ∨ 𝑋 ∈ (π‘πΌπ‘Œ)) ↔ (𝑍 ∈ (π‘ŒπΌπ‘‹) ∨ π‘Œ ∈ (𝑍𝐼𝑋) ∨ 𝑋 ∈ (π‘ŒπΌπ‘))))
142, 13bitrid 284 . . 3 (πœ‘ β†’ ((𝑍 ∈ (π‘‹πΌπ‘Œ) ∨ 𝑋 ∈ (π‘πΌπ‘Œ) ∨ π‘Œ ∈ (𝑋𝐼𝑍)) ↔ (𝑍 ∈ (π‘ŒπΌπ‘‹) ∨ π‘Œ ∈ (𝑍𝐼𝑋) ∨ 𝑋 ∈ (π‘ŒπΌπ‘))))
15 btwnlng1.l . . . 4 𝐿 = (LineGβ€˜πΊ)
16 btwnlng1.d . . . 4 (πœ‘ β†’ 𝑋 β‰  π‘Œ)
173, 15, 5, 6, 7, 9, 16, 8tgellng 26956 . . 3 (πœ‘ β†’ (𝑍 ∈ (π‘‹πΏπ‘Œ) ↔ (𝑍 ∈ (π‘‹πΌπ‘Œ) ∨ 𝑋 ∈ (π‘πΌπ‘Œ) ∨ π‘Œ ∈ (𝑋𝐼𝑍))))
1816necomd 2997 . . . 4 (πœ‘ β†’ π‘Œ β‰  𝑋)
193, 15, 5, 6, 9, 7, 18, 8tgellng 26956 . . 3 (πœ‘ β†’ (𝑍 ∈ (π‘ŒπΏπ‘‹) ↔ (𝑍 ∈ (π‘ŒπΌπ‘‹) ∨ π‘Œ ∈ (𝑍𝐼𝑋) ∨ 𝑋 ∈ (π‘ŒπΌπ‘))))
2014, 17, 193bitr4d 312 . 2 (πœ‘ β†’ (𝑍 ∈ (π‘‹πΏπ‘Œ) ↔ 𝑍 ∈ (π‘ŒπΏπ‘‹)))
211, 20mpbird 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