Metamath Proof Explorer

Theorem hlid

Description: The half-line relation is reflexive. Theorem 6.5 of Schwabhauser p. 44. (Contributed by Thierry Arnoux, 21-Feb-2020)

Ref Expression
Hypotheses ishlg.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
ishlg.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
ishlg.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
ishlg.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
ishlg.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
ishlg.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
hlln.1 ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
hlid.1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
Assertion hlid ( 𝜑 → 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐴 )

Proof

Step Hyp Ref Expression
1 ishlg.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 ishlg.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 ishlg.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
4 ishlg.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
5 ishlg.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
6 ishlg.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
7 hlln.1 ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
8 hlid.1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
9 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
10 1 9 2 7 6 4 tgbtwntriv2 ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐶 𝐼 𝐴 ) )
11 10 olcd ⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐶 𝐼 𝐴 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐴 ) ) )
12 1 2 3 4 4 6 7 ishlg ⊢ ( 𝜑 → ( 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐴 ↔ ( 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶 ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝐴 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐴 ) ) ) ) )
13 8 8 11 12 mpbir3and ⊢ ( 𝜑 → 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐴 )