Metamath Proof Explorer


Theorem mirbtwnb

Description: Point inversion preserves betweenness. 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
mirbtwnb.z φZP
Assertion mirbtwnb φYXIZMYMXIMZ

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 mirbtwnb.z φZP
12 6 adantr φYXIZG𝒢Tarski
13 7 adantr φYXIZAP
14 9 adantr φYXIZXP
15 10 adantr φYXIZYP
16 11 adantr φYXIZZP
17 simpr φYXIZYXIZ
18 1 2 3 4 5 12 13 8 14 15 16 17 mirbtwni φYXIZMYMXIMZ
19 6 adantr φMYMXIMZG𝒢Tarski
20 7 adantr φMYMXIMZAP
21 1 2 3 4 5 19 20 8 mirf φMYMXIMZM:PP
22 9 adantr φMYMXIMZXP
23 21 22 ffvelrnd φMYMXIMZMXP
24 10 adantr φMYMXIMZYP
25 21 24 ffvelrnd φMYMXIMZMYP
26 11 adantr φMYMXIMZZP
27 21 26 ffvelrnd φMYMXIMZMZP
28 simpr φMYMXIMZMYMXIMZ
29 1 2 3 4 5 19 20 8 23 25 27 28 mirbtwni φMYMXIMZMMYMMXIMMZ
30 1 2 3 4 5 6 7 8 10 mirmir φMMY=Y
31 1 2 3 4 5 6 7 8 9 mirmir φMMX=X
32 1 2 3 4 5 6 7 8 11 mirmir φMMZ=Z
33 31 32 oveq12d φMMXIMMZ=XIZ
34 30 33 eleq12d φMMYMMXIMMZYXIZ
35 34 adantr φMYMXIMZMMYMMXIMMZYXIZ
36 29 35 mpbid φMYMXIMZYXIZ
37 18 36 impbida φYXIZMYMXIMZ