Metamath Proof Explorer


Theorem colrot2

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 colrot2 φ Y Z L X Z = 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 1 2 3 4 5 6 7 8 colrot1 φ X Y L Z Y = Z
10 1 2 3 4 6 7 5 9 colrot1 φ Y Z L X Z = X