Description: Point inversion preserves betweenness, first half of Theorem 7.15 of Schwabhauser p. 51. (Contributed by Thierry Arnoux, 9-Jun-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mirval.p | |
|
mirval.d | |
||
mirval.i | |
||
mirval.l | |
||
mirval.s | |
||
mirval.g | |
||
mirval.a | |
||
mirfv.m | |
||
miriso.1 | |
||
miriso.2 | |
||
mirbtwni.z | |
||
mirbtwni.b | |
||
Assertion | mirbtwni | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mirval.p | |
|
2 | mirval.d | |
|
3 | mirval.i | |
|
4 | mirval.l | |
|
5 | mirval.s | |
|
6 | mirval.g | |
|
7 | mirval.a | |
|
8 | mirfv.m | |
|
9 | miriso.1 | |
|
10 | miriso.2 | |
|
11 | mirbtwni.z | |
|
12 | mirbtwni.b | |
|
13 | eqid | |
|
14 | 1 2 3 4 5 6 7 8 | mirf | |
15 | 14 9 | ffvelrnd | |
16 | 14 10 | ffvelrnd | |
17 | 14 11 | ffvelrnd | |
18 | 1 2 3 4 5 6 7 8 9 10 | miriso | |
19 | 18 | eqcomd | |
20 | 1 2 3 4 5 6 7 8 10 11 | miriso | |
21 | 20 | eqcomd | |
22 | 1 2 3 4 5 6 7 8 11 9 | miriso | |
23 | 22 | eqcomd | |
24 | 1 2 13 6 9 10 11 15 16 17 19 21 23 | trgcgr | |
25 | 1 2 3 13 6 9 10 11 15 16 17 24 12 | tgbtwnxfr | |