Description: A condition for extending betweenness to a new set of points based on congruence with another set of points. Theorem 4.6 of Schwabhauser p. 36. (Contributed by Thierry Arnoux, 27-Apr-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | tgcgrxfr.p | |
|
tgcgrxfr.m | |
||
tgcgrxfr.i | |
||
tgcgrxfr.r | |
||
tgcgrxfr.g | |
||
tgbtwnxfr.a | |
||
tgbtwnxfr.b | |
||
tgbtwnxfr.c | |
||
tgbtwnxfr.d | |
||
tgbtwnxfr.e | |
||
tgbtwnxfr.f | |
||
tgbtwnxfr.2 | |
||
tgbtwnxfr.1 | |
||
Assertion | tgbtwnxfr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tgcgrxfr.p | |
|
2 | tgcgrxfr.m | |
|
3 | tgcgrxfr.i | |
|
4 | tgcgrxfr.r | |
|
5 | tgcgrxfr.g | |
|
6 | tgbtwnxfr.a | |
|
7 | tgbtwnxfr.b | |
|
8 | tgbtwnxfr.c | |
|
9 | tgbtwnxfr.d | |
|
10 | tgbtwnxfr.e | |
|
11 | tgbtwnxfr.f | |
|
12 | tgbtwnxfr.2 | |
|
13 | tgbtwnxfr.1 | |
|
14 | 5 | ad2antrr | |
15 | simplr | |
|
16 | 10 | ad2antrr | |
17 | 9 | ad2antrr | |
18 | 11 | ad2antrr | |
19 | simprl | |
|
20 | eqidd | |
|
21 | eqidd | |
|
22 | 6 | ad2antrr | |
23 | 7 | ad2antrr | |
24 | 8 | ad2antrr | |
25 | simprr | |
|
26 | 1 2 3 4 14 22 23 24 17 15 18 25 | trgcgrcom | |
27 | 12 | ad2antrr | |
28 | 1 2 3 4 14 17 15 18 22 23 24 26 17 16 18 27 | cgr3tr | |
29 | 1 2 3 4 14 17 15 18 17 16 18 28 | trgcgrcom | |
30 | 1 2 3 4 14 17 16 18 17 15 18 29 | cgr3simp1 | |
31 | 1 2 3 4 14 17 16 18 17 15 18 29 | cgr3simp2 | |
32 | 1 2 3 14 16 18 15 18 31 | tgcgrcomlr | |
33 | 1 2 3 14 17 15 18 16 17 15 18 15 19 19 20 21 30 32 | tgifscgr | |
34 | 1 2 3 14 15 16 15 33 | axtgcgrid | |
35 | 34 19 | eqeltrrd | |
36 | 1 2 3 4 5 6 7 8 9 10 11 12 | cgr3simp3 | |
37 | 1 2 3 5 8 6 11 9 36 | tgcgrcomlr | |
38 | 1 2 3 4 5 6 7 8 9 11 13 37 | tgcgrxfr | |
39 | 35 38 | r19.29a | |