Metamath Proof Explorer

Theorem colcom

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
Hypotheses tglngval.p ⊢ P = Base G
tglngval.l ⊢ L = Line 𝒢 ⁡ G
tglngval.i ⊢ I = Itv ⁡ G
tglngval.g ⊢ φ → G ∈ 𝒢 Tarski
tglngval.x ⊢ φ → X ∈ P
tglngval.y ⊢ φ → Y ∈ P
tgcolg.z ⊢ φ → Z ∈ P
colrot ⊢ φ → Z ∈ X L Y ∨ X = Y
Assertion colcom ⊢ φ → Z ∈ Y L X ∨ Y = X

Proof

Step Hyp Ref Expression
1 tglngval.p ⊢ P = Base G
2 tglngval.l ⊢ L = Line 𝒢 ⁡ G
3 tglngval.i ⊢ I = Itv ⁡ G
4 tglngval.g ⊢ φ → G ∈ 𝒢 Tarski
5 tglngval.x ⊢ φ → X ∈ P
6 tglngval.y ⊢ φ → Y ∈ P
7 tgcolg.z ⊢ φ → Z ∈ P
8 colrot ⊢ φ → Z ∈ X L Y ∨ X = Y
9 3orcomb ⊢ Z ∈ X I Y ∨ X ∈ Z I Y ∨ Y ∈ X I Z ↔ Z ∈ X I Y ∨ Y ∈ X I Z ∨ X ∈ Z I Y
10 eqid ⊢ dist ⁡ G = dist ⁡ G
11 1 10 3 4 5 7 6 tgbtwncomb ⊢ φ → Z ∈ X I Y ↔ Z ∈ Y I X
12 1 10 3 4 5 6 7 tgbtwncomb ⊢ φ → Y ∈ X I Z ↔ Y ∈ Z I X
13 1 10 3 4 7 5 6 tgbtwncomb ⊢ φ → X ∈ Z I Y ↔ X ∈ Y I Z
14 11 12 13 3orbi123d ⊢ φ → Z ∈ X I Y ∨ Y ∈ X I Z ∨ X ∈ Z I Y ↔ Z ∈ Y I X ∨ Y ∈ Z I X ∨ X ∈ Y I Z
15 9 14 syl5bb ⊢ φ → Z ∈ X I Y ∨ X ∈ Z I Y ∨ Y ∈ X I Z ↔ Z ∈ Y I X ∨ Y ∈ Z I X ∨ X ∈ Y I Z
16 1 2 3 4 5 6 7 tgcolg ⊢ φ → Z ∈ X L Y ∨ X = Y ↔ Z ∈ X I Y ∨ X ∈ Z I Y ∨ Y ∈ X I Z
17 1 2 3 4 6 5 7 tgcolg ⊢ φ → Z ∈ Y L X ∨ Y = X ↔ Z ∈ Y I X ∨ Y ∈ Z I X ∨ X ∈ Y I Z
18 15 16 17 3bitr4d ⊢ φ → Z ∈ X L Y ∨ X = Y ↔ Z ∈ Y L X ∨ Y = X
19 8 18 mpbid ⊢ φ → Z ∈ Y L X ∨ Y = X