Metamath Proof Explorer

Theorem colrot1

Description: Rotating the points defining a line. 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 colrot1 ⊢ φ → X ∈ Y L Z ∨ Y = Z

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 3orrot ⊢ Z ∈ X I Y ∨ X ∈ Z I Y ∨ Y ∈ X I Z ↔ X ∈ Z I Y ∨ Y ∈ X I Z ∨ Z ∈ X I Y
10 eqid ⊢ dist ⁡ G = dist ⁡ G
11 1 10 3 4 7 5 6 tgbtwncomb ⊢ φ → X ∈ Z I Y ↔ X ∈ Y I Z
12 biidd ⊢ φ → Y ∈ X I Z ↔ Y ∈ X I Z
13 1 10 3 4 5 7 6 tgbtwncomb ⊢ φ → Z ∈ X I Y ↔ Z ∈ Y I X
14 11 12 13 3orbi123d ⊢ φ → X ∈ Z I Y ∨ Y ∈ X I Z ∨ Z ∈ X I Y ↔ X ∈ Y I Z ∨ Y ∈ X I Z ∨ Z ∈ Y I X
15 9 14 syl5bb ⊢ φ → Z ∈ X I Y ∨ X ∈ Z I Y ∨ Y ∈ X I Z ↔ X ∈ Y I Z ∨ Y ∈ X I Z ∨ Z ∈ Y I X
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 7 5 tgcolg ⊢ φ → X ∈ Y L Z ∨ Y = Z ↔ X ∈ Y I Z ∨ Y ∈ X I Z ∨ Z ∈ Y I X
18 15 16 17 3bitr4d ⊢ φ → Z ∈ X L Y ∨ X = Y ↔ X ∈ Y L Z ∨ Y = Z
19 8 18 mpbid ⊢ φ → X ∈ Y L Z ∨ Y = Z