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 = ( Base ` G )
mirval.d 
|- .- = ( dist ` G )
mirval.i 
|- I = ( Itv ` G )
mirval.l 
|- L = ( LineG ` G )
mirval.s 
|- S = ( pInvG ` G )
mirval.g 
|- ( ph -> G e. TarskiG )
mirval.a 
|- ( ph -> A e. P )
mirfv.m 
|- M = ( S ` A )
miriso.1 
|- ( ph -> X e. P )
miriso.2 
|- ( ph -> Y e. P )
mirbtwnb.z 
|- ( ph -> Z e. P )
Assertion mirbtwnb 
|- ( ph -> ( Y e. ( X I Z ) <-> ( M ` Y ) e. ( ( M ` X ) I ( M ` Z ) ) ) )

Proof

Step Hyp Ref Expression
1 mirval.p 
 |-  P = ( Base ` G )
2 mirval.d 
 |-  .- = ( dist ` G )
3 mirval.i 
 |-  I = ( Itv ` G )
4 mirval.l 
 |-  L = ( LineG ` G )
5 mirval.s 
 |-  S = ( pInvG ` G )
6 mirval.g 
 |-  ( ph -> G e. TarskiG )
7 mirval.a 
 |-  ( ph -> A e. P )
8 mirfv.m 
 |-  M = ( S ` A )
9 miriso.1 
 |-  ( ph -> X e. P )
10 miriso.2 
 |-  ( ph -> Y e. P )
11 mirbtwnb.z 
 |-  ( ph -> Z e. P )
12 6 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> G e. TarskiG )
13 7 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> A e. P )
14 9 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> X e. P )
15 10 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> Y e. P )
16 11 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> Z e. P )
17 simpr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> Y e. ( X I Z ) )
18 1 2 3 4 5 12 13 8 14 15 16 17 mirbtwni 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> ( M ` Y ) e. ( ( M ` X ) I ( M ` Z ) ) )
19 6 adantr 
 |-  ( ( ph /\ ( M ` Y ) e. ( ( M ` X ) I ( M ` Z ) ) ) -> G e. TarskiG )
20 7 adantr 
 |-  ( ( ph /\ ( M ` Y ) e. ( ( M ` X ) I ( M ` Z ) ) ) -> A e. P )
21 1 2 3 4 5 19 20 8 mirf 
 |-  ( ( ph /\ ( M ` Y ) e. ( ( M ` X ) I ( M ` Z ) ) ) -> M : P --> P )
22 9 adantr 
 |-  ( ( ph /\ ( M ` Y ) e. ( ( M ` X ) I ( M ` Z ) ) ) -> X e. P )
23 21 22 ffvelcdmd 
 |-  ( ( ph /\ ( M ` Y ) e. ( ( M ` X ) I ( M ` Z ) ) ) -> ( M ` X ) e. P )
24 10 adantr 
 |-  ( ( ph /\ ( M ` Y ) e. ( ( M ` X ) I ( M ` Z ) ) ) -> Y e. P )
25 21 24 ffvelcdmd 
 |-  ( ( ph /\ ( M ` Y ) e. ( ( M ` X ) I ( M ` Z ) ) ) -> ( M ` Y ) e. P )
26 11 adantr 
 |-  ( ( ph /\ ( M ` Y ) e. ( ( M ` X ) I ( M ` Z ) ) ) -> Z e. P )
27 21 26 ffvelcdmd 
 |-  ( ( ph /\ ( M ` Y ) e. ( ( M ` X ) I ( M ` Z ) ) ) -> ( M ` Z ) e. P )
28 simpr 
 |-  ( ( ph /\ ( M ` Y ) e. ( ( M ` X ) I ( M ` Z ) ) ) -> ( M ` Y ) e. ( ( M ` X ) I ( M ` Z ) ) )
29 1 2 3 4 5 19 20 8 23 25 27 28 mirbtwni 
 |-  ( ( ph /\ ( M ` Y ) e. ( ( M ` X ) I ( M ` Z ) ) ) -> ( M ` ( M ` Y ) ) e. ( ( M ` ( M ` X ) ) I ( M ` ( M ` Z ) ) ) )
30 1 2 3 4 5 6 7 8 10 mirmir 
 |-  ( ph -> ( M ` ( M ` Y ) ) = Y )
31 1 2 3 4 5 6 7 8 9 mirmir 
 |-  ( ph -> ( M ` ( M ` X ) ) = X )
32 1 2 3 4 5 6 7 8 11 mirmir 
 |-  ( ph -> ( M ` ( M ` Z ) ) = Z )
33 31 32 oveq12d 
 |-  ( ph -> ( ( M ` ( M ` X ) ) I ( M ` ( M ` Z ) ) ) = ( X I Z ) )
34 30 33 eleq12d 
 |-  ( ph -> ( ( M ` ( M ` Y ) ) e. ( ( M ` ( M ` X ) ) I ( M ` ( M ` Z ) ) ) <-> Y e. ( X I Z ) ) )
35 34 adantr 
 |-  ( ( ph /\ ( M ` Y ) e. ( ( M ` X ) I ( M ` Z ) ) ) -> ( ( M ` ( M ` Y ) ) e. ( ( M ` ( M ` X ) ) I ( M ` ( M ` Z ) ) ) <-> Y e. ( X I Z ) ) )
36 29 35 mpbid 
 |-  ( ( ph /\ ( M ` Y ) e. ( ( M ` X ) I ( M ` Z ) ) ) -> Y e. ( X I Z ) )
37 18 36 impbida 
 |-  ( ph -> ( Y e. ( X I Z ) <-> ( M ` Y ) e. ( ( M ` X ) I ( M ` Z ) ) ) )