Theorem colcom 27563

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
tglngval.p	⊢ 𝑃 = (Base‘𝐺)
tglngval.l	⊢ 𝐿 = (LineG‘𝐺)
tglngval.i	⊢ 𝐼 = (Itv‘𝐺)
tglngval.g	⊢ (𝜑 → 𝐺 ∈ TarskiG)
tglngval.x	⊢ (𝜑 → 𝑋 ∈ 𝑃)
tglngval.y	⊢ (𝜑 → 𝑌 ∈ 𝑃)
tgcolg.z	⊢ (𝜑 → 𝑍 ∈ 𝑃)
colrot	⊢ (𝜑 → (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌))

Assertion

Ref	Expression
colcom	⊢ (𝜑 → (𝑍 ∈ (𝑌𝐿𝑋) ∨ 𝑌 = 𝑋))

Proof of Theorem colcom

Step	Hyp	Ref	Expression
1		colrot	. 2 ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌))
2		3orcomb 1094	. . . 4 ⊢ ((𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)) ↔ (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍) ∨ 𝑋 ∈ (𝑍𝐼𝑌)))
3		tglngval.p	. . . . . 6 ⊢ 𝑃 = (Base‘𝐺)
4		eqid 2731	. . . . . 6 ⊢ (dist‘𝐺) = (dist‘𝐺)
5		tglngval.i	. . . . . 6 ⊢ 𝐼 = (Itv‘𝐺)
6		tglngval.g	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
7		tglngval.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
8		tgcolg.z	. . . . . 6 ⊢ (𝜑 → 𝑍 ∈ 𝑃)
9		tglngval.y	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ 𝑃)
10	3, 4, 5, 6, 7, 8, 9	tgbtwncomb 27494	. . . . 5 ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐼𝑌) ↔ 𝑍 ∈ (𝑌𝐼𝑋)))
11	3, 4, 5, 6, 7, 9, 8	tgbtwncomb 27494	. . . . 5 ⊢ (𝜑 → (𝑌 ∈ (𝑋𝐼𝑍) ↔ 𝑌 ∈ (𝑍𝐼𝑋)))
12	3, 4, 5, 6, 8, 7, 9	tgbtwncomb 27494	. . . . 5 ⊢ (𝜑 → (𝑋 ∈ (𝑍𝐼𝑌) ↔ 𝑋 ∈ (𝑌𝐼𝑍)))
13	10, 11, 12	3orbi123d 1435	. . . 4 ⊢ (𝜑 → ((𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍) ∨ 𝑋 ∈ (𝑍𝐼𝑌)) ↔ (𝑍 ∈ (𝑌𝐼𝑋) ∨ 𝑌 ∈ (𝑍𝐼𝑋) ∨ 𝑋 ∈ (𝑌𝐼𝑍))))
14	2, 13	bitrid 282	. . 3 ⊢ (𝜑 → ((𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)) ↔ (𝑍 ∈ (𝑌𝐼𝑋) ∨ 𝑌 ∈ (𝑍𝐼𝑋) ∨ 𝑋 ∈ (𝑌𝐼𝑍))))
15		tglngval.l	. . . 4 ⊢ 𝐿 = (LineG‘𝐺)
16	3, 15, 5, 6, 7, 9, 8	tgcolg 27559	. . 3 ⊢ (𝜑 → ((𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌) ↔ (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))))
17	3, 15, 5, 6, 9, 7, 8	tgcolg 27559	. . 3 ⊢ (𝜑 → ((𝑍 ∈ (𝑌𝐿𝑋) ∨ 𝑌 = 𝑋) ↔ (𝑍 ∈ (𝑌𝐼𝑋) ∨ 𝑌 ∈ (𝑍𝐼𝑋) ∨ 𝑋 ∈ (𝑌𝐼𝑍))))
18	14, 16, 17	3bitr4d 310	. 2 ⊢ (𝜑 → ((𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌) ↔ (𝑍 ∈ (𝑌𝐿𝑋) ∨ 𝑌 = 𝑋)))
19	1, 18	mpbid 231	1 ⊢ (𝜑 → (𝑍 ∈ (𝑌𝐿𝑋) ∨ 𝑌 = 𝑋))

Syntax hints:   → wi 4   ∨ wo 845   ∨ w3o 1086   = wceq 1541   ∈ wcel 2106  ‘cfv 6501  (class class class)co 7362  Basecbs 17094  distcds 17156  TarskiGcstrkg 27432  Itvcitv 27438  LineGclng 27439

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-sbc 3743  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6453  df-fun 6503  df-fv 6509  df-ov 7365  df-oprab 7366  df-mpo 7367  df-trkgc 27453  df-trkgb 27454  df-trkgcb 27455  df-trkg 27458

This theorem is referenced by:  ncolcom  27566  tglineeltr  27636  mirtrcgr  27688  symquadlem  27694  midexlem  27697  colperpexlem1  27735  mideulem2  27739  opphllem  27740  hlpasch  27761  colhp  27775  trgcopy  27809  cgrg3col4  27858  tgasa1  27863