Metamath Proof Explorer


Theorem mirbtwni

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 P=BaseG
mirval.d -˙=distG
mirval.i I=ItvG
mirval.l L=Line𝒢G
mirval.s S=pInv𝒢G
mirval.g φG𝒢Tarski
mirval.a φAP
mirfv.m M=SA
miriso.1 φXP
miriso.2 φYP
mirbtwni.z φZP
mirbtwni.b φYXIZ
Assertion mirbtwni φMYMXIMZ

Proof

Step Hyp Ref Expression
1 mirval.p P=BaseG
2 mirval.d -˙=distG
3 mirval.i I=ItvG
4 mirval.l L=Line𝒢G
5 mirval.s S=pInv𝒢G
6 mirval.g φG𝒢Tarski
7 mirval.a φAP
8 mirfv.m M=SA
9 miriso.1 φXP
10 miriso.2 φYP
11 mirbtwni.z φZP
12 mirbtwni.b φYXIZ
13 eqid 𝒢G=𝒢G
14 1 2 3 4 5 6 7 8 mirf φM:PP
15 14 9 ffvelrnd φMXP
16 14 10 ffvelrnd φMYP
17 14 11 ffvelrnd φMZP
18 1 2 3 4 5 6 7 8 9 10 miriso φMX-˙MY=X-˙Y
19 18 eqcomd φX-˙Y=MX-˙MY
20 1 2 3 4 5 6 7 8 10 11 miriso φMY-˙MZ=Y-˙Z
21 20 eqcomd φY-˙Z=MY-˙MZ
22 1 2 3 4 5 6 7 8 11 9 miriso φMZ-˙MX=Z-˙X
23 22 eqcomd φZ-˙X=MZ-˙MX
24 1 2 13 6 9 10 11 15 16 17 19 21 23 trgcgr φ⟨“XYZ”⟩𝒢G⟨“MXMYMZ”⟩
25 1 2 3 13 6 9 10 11 15 16 17 24 12 tgbtwnxfr φMYMXIMZ