Description: Point inversion preserves betweenness. 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 | |
||
mirbtwnb.z | |
||
Assertion | mirbtwnb | |
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 | mirbtwnb.z | |
|
12 | 6 | adantr | |
13 | 7 | adantr | |
14 | 9 | adantr | |
15 | 10 | adantr | |
16 | 11 | adantr | |
17 | simpr | |
|
18 | 1 2 3 4 5 12 13 8 14 15 16 17 | mirbtwni | |
19 | 6 | adantr | |
20 | 7 | adantr | |
21 | 1 2 3 4 5 19 20 8 | mirf | |
22 | 9 | adantr | |
23 | 21 22 | ffvelrnd | |
24 | 10 | adantr | |
25 | 21 24 | ffvelrnd | |
26 | 11 | adantr | |
27 | 21 26 | ffvelrnd | |
28 | simpr | |
|
29 | 1 2 3 4 5 19 20 8 23 25 27 28 | mirbtwni | |
30 | 1 2 3 4 5 6 7 8 10 | mirmir | |
31 | 1 2 3 4 5 6 7 8 9 | mirmir | |
32 | 1 2 3 4 5 6 7 8 11 | mirmir | |
33 | 31 32 | oveq12d | |
34 | 30 33 | eleq12d | |
35 | 34 | adantr | |
36 | 29 35 | mpbid | |
37 | 18 36 | impbida | |