Metamath Proof Explorer

Theorem lnrot2

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 btwnlng1.p ⊢ P = Base G
btwnlng1.i ⊢ I = Itv ⁡ G
btwnlng1.l ⊢ L = Line 𝒢 ⁡ G
btwnlng1.g ⊢ φ → G ∈ 𝒢 Tarski
btwnlng1.x ⊢ φ → X ∈ P
btwnlng1.y ⊢ φ → Y ∈ P
btwnlng1.z ⊢ φ → Z ∈ P
btwnlng1.d ⊢ φ → X ≠ Y
lnrot2.1 ⊢ φ → X ∈ Y L Z
lnrot2.2 ⊢ φ → Y ≠ Z
Assertion lnrot2 ⊢ φ → Z ∈ X L Y

Proof

Step Hyp Ref Expression
1 btwnlng1.p ⊢ P = Base G
2 btwnlng1.i ⊢ I = Itv ⁡ G
3 btwnlng1.l ⊢ L = Line 𝒢 ⁡ G
4 btwnlng1.g ⊢ φ → G ∈ 𝒢 Tarski
5 btwnlng1.x ⊢ φ → X ∈ P
6 btwnlng1.y ⊢ φ → Y ∈ P
7 btwnlng1.z ⊢ φ → Z ∈ P
8 btwnlng1.d ⊢ φ → X ≠ Y
9 lnrot2.1 ⊢ φ → X ∈ Y L Z
10 lnrot2.2 ⊢ φ → Y ≠ Z
11 eqid ⊢ dist ⁡ G = dist ⁡ G
12 1 11 2 4 6 5 7 tgbtwncomb ⊢ φ → X ∈ Y I Z ↔ X ∈ Z I Y
13 biidd ⊢ φ → Y ∈ X I Z ↔ Y ∈ X I Z
14 1 11 2 4 6 7 5 tgbtwncomb ⊢ φ → Z ∈ Y I X ↔ Z ∈ X I Y
15 12 13 14 3orbi123d ⊢ φ → X ∈ Y I Z ∨ Y ∈ X I Z ∨ Z ∈ Y I X ↔ X ∈ Z I Y ∨ Y ∈ X I Z ∨ Z ∈ X I Y
16 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
17 15 16 bitr4di ⊢ φ → X ∈ Y I Z ∨ Y ∈ X I Z ∨ Z ∈ Y I X ↔ Z ∈ X I Y ∨ X ∈ Z I Y ∨ Y ∈ X I Z
18 1 3 2 4 6 7 10 5 tgellng ⊢ φ → X ∈ Y L Z ↔ X ∈ Y I Z ∨ Y ∈ X I Z ∨ Z ∈ Y I X
19 1 3 2 4 5 6 8 7 tgellng ⊢ φ → Z ∈ X L Y ↔ Z ∈ X I Y ∨ X ∈ Z I Y ∨ Y ∈ X I Z
20 17 18 19 3bitr4d ⊢ φ → X ∈ Y L Z ↔ Z ∈ X L Y
21 9 20 mpbid ⊢ φ → Z ∈ X L Y