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 ⊢ 𝑃 = ( Base ‘ 𝐺 )
mirval.d ⊢ − = ( dist ‘ 𝐺 )
mirval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
mirval.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
mirval.s ⊢ 𝑆 = ( pInvG ‘ 𝐺 )
mirval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
mirval.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
mirfv.m ⊢ 𝑀 = ( 𝑆 ‘ 𝐴 )
miriso.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
miriso.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
mirbtwnb.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
Assertion mirbtwnb ( 𝜑 → ( 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ↔ ( 𝑀 ‘ 𝑌 ) ∈ ( ( 𝑀 ‘ 𝑋 ) 𝐼 ( 𝑀 ‘ 𝑍 ) ) ) )

Proof

Step Hyp Ref Expression
1 mirval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 mirval.d ⊢ − = ( dist ‘ 𝐺 )
3 mirval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 mirval.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
5 mirval.s ⊢ 𝑆 = ( pInvG ‘ 𝐺 )
6 mirval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
7 mirval.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
8 mirfv.m ⊢ 𝑀 = ( 𝑆 ‘ 𝐴 )
9 miriso.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
10 miriso.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
11 mirbtwnb.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
12 6 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝐺 ∈ TarskiG )
13 7 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝐴 ∈ 𝑃 )
14 9 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑋 ∈ 𝑃 )
15 10 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑌 ∈ 𝑃 )
16 11 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑍 ∈ 𝑃 )
17 simpr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) )
18 1 2 3 4 5 12 13 8 14 15 16 17 mirbtwni ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → ( 𝑀 ‘ 𝑌 ) ∈ ( ( 𝑀 ‘ 𝑋 ) 𝐼 ( 𝑀 ‘ 𝑍 ) ) )
19 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑌 ) ∈ ( ( 𝑀 ‘ 𝑋 ) 𝐼 ( 𝑀 ‘ 𝑍 ) ) ) → 𝐺 ∈ TarskiG )
20 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑌 ) ∈ ( ( 𝑀 ‘ 𝑋 ) 𝐼 ( 𝑀 ‘ 𝑍 ) ) ) → 𝐴 ∈ 𝑃 )
21 1 2 3 4 5 19 20 8 mirf ⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑌 ) ∈ ( ( 𝑀 ‘ 𝑋 ) 𝐼 ( 𝑀 ‘ 𝑍 ) ) ) → 𝑀 : 𝑃 ⟶ 𝑃 )
22 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑌 ) ∈ ( ( 𝑀 ‘ 𝑋 ) 𝐼 ( 𝑀 ‘ 𝑍 ) ) ) → 𝑋 ∈ 𝑃 )
23 21 22 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑌 ) ∈ ( ( 𝑀 ‘ 𝑋 ) 𝐼 ( 𝑀 ‘ 𝑍 ) ) ) → ( 𝑀 ‘ 𝑋 ) ∈ 𝑃 )
24 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑌 ) ∈ ( ( 𝑀 ‘ 𝑋 ) 𝐼 ( 𝑀 ‘ 𝑍 ) ) ) → 𝑌 ∈ 𝑃 )
25 21 24 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑌 ) ∈ ( ( 𝑀 ‘ 𝑋 ) 𝐼 ( 𝑀 ‘ 𝑍 ) ) ) → ( 𝑀 ‘ 𝑌 ) ∈ 𝑃 )
26 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑌 ) ∈ ( ( 𝑀 ‘ 𝑋 ) 𝐼 ( 𝑀 ‘ 𝑍 ) ) ) → 𝑍 ∈ 𝑃 )
27 21 26 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑌 ) ∈ ( ( 𝑀 ‘ 𝑋 ) 𝐼 ( 𝑀 ‘ 𝑍 ) ) ) → ( 𝑀 ‘ 𝑍 ) ∈ 𝑃 )
28 simpr ⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑌 ) ∈ ( ( 𝑀 ‘ 𝑋 ) 𝐼 ( 𝑀 ‘ 𝑍 ) ) ) → ( 𝑀 ‘ 𝑌 ) ∈ ( ( 𝑀 ‘ 𝑋 ) 𝐼 ( 𝑀 ‘ 𝑍 ) ) )
29 1 2 3 4 5 19 20 8 23 25 27 28 mirbtwni ⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑌 ) ∈ ( ( 𝑀 ‘ 𝑋 ) 𝐼 ( 𝑀 ‘ 𝑍 ) ) ) → ( 𝑀 ‘ ( 𝑀 ‘ 𝑌 ) ) ∈ ( ( 𝑀 ‘ ( 𝑀 ‘ 𝑋 ) ) 𝐼 ( 𝑀 ‘ ( 𝑀 ‘ 𝑍 ) ) ) )
30 1 2 3 4 5 6 7 8 10 mirmir ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑀 ‘ 𝑌 ) ) = 𝑌 )
31 1 2 3 4 5 6 7 8 9 mirmir ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑀 ‘ 𝑋 ) ) = 𝑋 )
32 1 2 3 4 5 6 7 8 11 mirmir ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑀 ‘ 𝑍 ) ) = 𝑍 )
33 31 32 oveq12d ⊢ ( 𝜑 → ( ( 𝑀 ‘ ( 𝑀 ‘ 𝑋 ) ) 𝐼 ( 𝑀 ‘ ( 𝑀 ‘ 𝑍 ) ) ) = ( 𝑋 𝐼 𝑍 ) )
34 30 33 eleq12d ⊢ ( 𝜑 → ( ( 𝑀 ‘ ( 𝑀 ‘ 𝑌 ) ) ∈ ( ( 𝑀 ‘ ( 𝑀 ‘ 𝑋 ) ) 𝐼 ( 𝑀 ‘ ( 𝑀 ‘ 𝑍 ) ) ) ↔ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) )
35 34 adantr ⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑌 ) ∈ ( ( 𝑀 ‘ 𝑋 ) 𝐼 ( 𝑀 ‘ 𝑍 ) ) ) → ( ( 𝑀 ‘ ( 𝑀 ‘ 𝑌 ) ) ∈ ( ( 𝑀 ‘ ( 𝑀 ‘ 𝑋 ) ) 𝐼 ( 𝑀 ‘ ( 𝑀 ‘ 𝑍 ) ) ) ↔ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) )
36 29 35 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑌 ) ∈ ( ( 𝑀 ‘ 𝑋 ) 𝐼 ( 𝑀 ‘ 𝑍 ) ) ) → 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) )
37 18 36 impbida ⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ↔ ( 𝑀 ‘ 𝑌 ) ∈ ( ( 𝑀 ‘ 𝑋 ) 𝐼 ( 𝑀 ‘ 𝑍 ) ) ) )