Metamath Proof Explorer


Theorem tgbtwnxfr

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 P=BaseG
tgcgrxfr.m -˙=distG
tgcgrxfr.i I=ItvG
tgcgrxfr.r ˙=𝒢G
tgcgrxfr.g φG𝒢Tarski
tgbtwnxfr.a φAP
tgbtwnxfr.b φBP
tgbtwnxfr.c φCP
tgbtwnxfr.d φDP
tgbtwnxfr.e φEP
tgbtwnxfr.f φFP
tgbtwnxfr.2 φ⟨“ABC”⟩˙⟨“DEF”⟩
tgbtwnxfr.1 φBAIC
Assertion tgbtwnxfr φEDIF

Proof

Step Hyp Ref Expression
1 tgcgrxfr.p P=BaseG
2 tgcgrxfr.m -˙=distG
3 tgcgrxfr.i I=ItvG
4 tgcgrxfr.r ˙=𝒢G
5 tgcgrxfr.g φG𝒢Tarski
6 tgbtwnxfr.a φAP
7 tgbtwnxfr.b φBP
8 tgbtwnxfr.c φCP
9 tgbtwnxfr.d φDP
10 tgbtwnxfr.e φEP
11 tgbtwnxfr.f φFP
12 tgbtwnxfr.2 φ⟨“ABC”⟩˙⟨“DEF”⟩
13 tgbtwnxfr.1 φBAIC
14 5 ad2antrr φePeDIF⟨“ABC”⟩˙⟨“DeF”⟩G𝒢Tarski
15 simplr φePeDIF⟨“ABC”⟩˙⟨“DeF”⟩eP
16 10 ad2antrr φePeDIF⟨“ABC”⟩˙⟨“DeF”⟩EP
17 9 ad2antrr φePeDIF⟨“ABC”⟩˙⟨“DeF”⟩DP
18 11 ad2antrr φePeDIF⟨“ABC”⟩˙⟨“DeF”⟩FP
19 simprl φePeDIF⟨“ABC”⟩˙⟨“DeF”⟩eDIF
20 eqidd φePeDIF⟨“ABC”⟩˙⟨“DeF”⟩D-˙F=D-˙F
21 eqidd φePeDIF⟨“ABC”⟩˙⟨“DeF”⟩e-˙F=e-˙F
22 6 ad2antrr φePeDIF⟨“ABC”⟩˙⟨“DeF”⟩AP
23 7 ad2antrr φePeDIF⟨“ABC”⟩˙⟨“DeF”⟩BP
24 8 ad2antrr φePeDIF⟨“ABC”⟩˙⟨“DeF”⟩CP
25 simprr φePeDIF⟨“ABC”⟩˙⟨“DeF”⟩⟨“ABC”⟩˙⟨“DeF”⟩
26 1 2 3 4 14 22 23 24 17 15 18 25 trgcgrcom φePeDIF⟨“ABC”⟩˙⟨“DeF”⟩⟨“DeF”⟩˙⟨“ABC”⟩
27 12 ad2antrr φePeDIF⟨“ABC”⟩˙⟨“DeF”⟩⟨“ABC”⟩˙⟨“DEF”⟩
28 1 2 3 4 14 17 15 18 22 23 24 26 17 16 18 27 cgr3tr φePeDIF⟨“ABC”⟩˙⟨“DeF”⟩⟨“DeF”⟩˙⟨“DEF”⟩
29 1 2 3 4 14 17 15 18 17 16 18 28 trgcgrcom φePeDIF⟨“ABC”⟩˙⟨“DeF”⟩⟨“DEF”⟩˙⟨“DeF”⟩
30 1 2 3 4 14 17 16 18 17 15 18 29 cgr3simp1 φePeDIF⟨“ABC”⟩˙⟨“DeF”⟩D-˙E=D-˙e
31 1 2 3 4 14 17 16 18 17 15 18 29 cgr3simp2 φePeDIF⟨“ABC”⟩˙⟨“DeF”⟩E-˙F=e-˙F
32 1 2 3 14 16 18 15 18 31 tgcgrcomlr φePeDIF⟨“ABC”⟩˙⟨“DeF”⟩F-˙E=F-˙e
33 1 2 3 14 17 15 18 16 17 15 18 15 19 19 20 21 30 32 tgifscgr φePeDIF⟨“ABC”⟩˙⟨“DeF”⟩e-˙E=e-˙e
34 1 2 3 14 15 16 15 33 axtgcgrid φePeDIF⟨“ABC”⟩˙⟨“DeF”⟩e=E
35 34 19 eqeltrrd φePeDIF⟨“ABC”⟩˙⟨“DeF”⟩EDIF
36 1 2 3 4 5 6 7 8 9 10 11 12 cgr3simp3 φC-˙A=F-˙D
37 1 2 3 5 8 6 11 9 36 tgcgrcomlr φA-˙C=D-˙F
38 1 2 3 4 5 6 7 8 9 11 13 37 tgcgrxfr φePeDIF⟨“ABC”⟩˙⟨“DeF”⟩
39 35 38 r19.29a φEDIF