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