Theorem lncom 28606

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

Step	Hyp	Ref	Expression
1		lncom.1	. 2 ⊢ (𝜑 → 𝑍 ∈ (𝑌𝐿𝑋))
2		3orcomb 1093	. . . 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 28473	. . . . 5 ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐼𝑌) ↔ 𝑍 ∈ (𝑌𝐼𝑋)))
11	3, 4, 5, 6, 7, 9, 8	tgbtwncomb 28473	. . . . 5 ⊢ (𝜑 → (𝑌 ∈ (𝑋𝐼𝑍) ↔ 𝑌 ∈ (𝑍𝐼𝑋)))
12	3, 4, 5, 6, 8, 7, 9	tgbtwncomb 28473	. . . . 5 ⊢ (𝜑 → (𝑋 ∈ (𝑍𝐼𝑌) ↔ 𝑋 ∈ (𝑌𝐼𝑍)))
13	10, 11, 12	3orbi123d 1437	. . . 4 ⊢ (𝜑 → ((𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍) ∨ 𝑋 ∈ (𝑍𝐼𝑌)) ↔ (𝑍 ∈ (𝑌𝐼𝑋) ∨ 𝑌 ∈ (𝑍𝐼𝑋) ∨ 𝑋 ∈ (𝑌𝐼𝑍))))
14	2, 13	bitrid 283	. . 3 ⊢ (𝜑 → ((𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)) ↔ (𝑍 ∈ (𝑌𝐼𝑋) ∨ 𝑌 ∈ (𝑍𝐼𝑋) ∨ 𝑋 ∈ (𝑌𝐼𝑍))))
15		btwnlng1.l	. . . 4 ⊢ 𝐿 = (LineG‘𝐺)
16		btwnlng1.d	. . . 4 ⊢ (𝜑 → 𝑋 ≠ 𝑌)
17	3, 15, 5, 6, 7, 9, 16, 8	tgellng 28537	. . 3 ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐿𝑌) ↔ (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))))
18	16	necomd 2988	. . . 4 ⊢ (𝜑 → 𝑌 ≠ 𝑋)
19	3, 15, 5, 6, 9, 7, 18, 8	tgellng 28537	. . 3 ⊢ (𝜑 → (𝑍 ∈ (𝑌𝐿𝑋) ↔ (𝑍 ∈ (𝑌𝐼𝑋) ∨ 𝑌 ∈ (𝑍𝐼𝑋) ∨ 𝑋 ∈ (𝑌𝐼𝑍))))
20	14, 17, 19	3bitr4d 311	. 2 ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐿𝑌) ↔ 𝑍 ∈ (𝑌𝐿𝑋)))
21	1, 20	mpbird 257	1 ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐿𝑌))

Syntax hints:   → wi 4   ∨ w3o 1085   = wceq 1540   ∈ wcel 2109   ≠ wne 2933  ‘cfv 6536  (class class class)co 7410  Basecbs 17233  distcds 17285  TarskiGcstrkg 28411  Itvcitv 28417  LineGclng 28418

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-sbc 3771  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-iota 6489  df-fun 6538  df-fv 6544  df-ov 7413  df-oprab 7414  df-mpo 7415  df-trkgc 28432  df-trkgb 28433  df-trkgcb 28434  df-trkg 28437

This theorem is referenced by:  tglineelsb2  28616  tglinecom  28619  ncolncol  28630  coltr  28631  midexlem  28676  footexALT  28702  footexlem1  28703  footexlem2  28704  opphllem1  28731  opphllem2  28732  outpasch  28739  hlpasch  28740  trgcopy  28788  trgcopyeulem  28789  cgracgr  28802  tgasa1  28842