Metamath Proof Explorer

Theorem mirhl2

Description: Deduce half-line relation from mirror point. (Contributed by Thierry Arnoux, 8-Aug-2020)

Ref Expression
Hypotheses mirval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
mirval.d ⊢ − = ( dist ‘ 𝐺 )
mirval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
mirval.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
mirval.s ⊢ 𝑆 = ( pInvG ‘ 𝐺 )
mirval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
mirhl.m ⊢ 𝑀 = ( 𝑆 ‘ 𝐴 )
mirhl.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
mirhl.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
mirhl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
mirhl.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
mirhl.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
mirhl2.1 ⊢ ( 𝜑 → 𝑋 ≠ 𝐴 )
mirhl2.2 ⊢ ( 𝜑 → 𝑌 ≠ 𝐴 )
mirhl2.3 ⊢ ( 𝜑 → 𝐴 ∈ ( 𝑋 𝐼 ( 𝑀 ‘ 𝑌 ) ) )
Assertion mirhl2 ( 𝜑 → 𝑋 ( 𝐾 ‘ 𝐴 ) 𝑌 )

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 mirhl.m ⊢ 𝑀 = ( 𝑆 ‘ 𝐴 )
8 mirhl.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
9 mirhl.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
10 mirhl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
11 mirhl.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
12 mirhl.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
13 mirhl2.1 ⊢ ( 𝜑 → 𝑋 ≠ 𝐴 )
14 mirhl2.2 ⊢ ( 𝜑 → 𝑌 ≠ 𝐴 )
15 mirhl2.3 ⊢ ( 𝜑 → 𝐴 ∈ ( 𝑋 𝐼 ( 𝑀 ‘ 𝑌 ) ) )
16 1 2 3 4 5 6 9 7 11 mircl ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑌 ) ∈ 𝑃 )
17 1 2 3 4 5 6 9 7 11 14 mirne ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑌 ) ≠ 𝐴 )
18 1 2 3 6 10 9 16 15 tgbtwncom ⊢ ( 𝜑 → 𝐴 ∈ ( ( 𝑀 ‘ 𝑌 ) 𝐼 𝑋 ) )
19 1 2 3 4 5 6 9 7 11 mirbtwn ⊢ ( 𝜑 → 𝐴 ∈ ( ( 𝑀 ‘ 𝑌 ) 𝐼 𝑌 ) )
20 1 3 6 16 9 10 11 17 18 19 tgbtwnconn2 ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐴 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝐴 𝐼 𝑋 ) ) )
21 1 3 8 10 11 9 6 ishlg ⊢ ( 𝜑 → ( 𝑋 ( 𝐾 ‘ 𝐴 ) 𝑌 ↔ ( 𝑋 ≠ 𝐴 ∧ 𝑌 ≠ 𝐴 ∧ ( 𝑋 ∈ ( 𝐴 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝐴 𝐼 𝑋 ) ) ) ) )
22 13 14 20 21 mpbir3and ⊢ ( 𝜑 → 𝑋 ( 𝐾 ‘ 𝐴 ) 𝑌 )