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 | ||
tglngval.l | |||
tglngval.i | |||
tglngval.g | |||
tglngval.x | |||
tglngval.y | |||
tgcolg.z | |||
colrot | |||
Assertion | colrot2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tglngval.p | ||
2 | tglngval.l | ||
3 | tglngval.i | ||
4 | tglngval.g | ||
5 | tglngval.x | ||
6 | tglngval.y | ||
7 | tgcolg.z | ||
8 | colrot | ||
9 | 1 2 3 4 5 6 7 8 | colrot1 | |
10 | 1 2 3 4 6 7 5 9 | colrot1 |