Metamath Proof Explorer


Theorem hlne1

Description: The half-line relation implies inequality. (Contributed by Thierry Arnoux, 22-Feb-2020)

Ref Expression
Hypotheses ishlg.p 𝑃 = ( Base ‘ 𝐺 )
ishlg.i 𝐼 = ( Itv ‘ 𝐺 )
ishlg.k 𝐾 = ( hlG ‘ 𝐺 )
ishlg.a ( 𝜑𝐴𝑃 )
ishlg.b ( 𝜑𝐵𝑃 )
ishlg.c ( 𝜑𝐶𝑃 )
ishlg.g ( 𝜑𝐺𝑉 )
hlcomd.1 ( 𝜑𝐴 ( 𝐾𝐶 ) 𝐵 )
Assertion hlne1 ( 𝜑𝐴𝐶 )

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 ishlg.g ( 𝜑𝐺𝑉 )
8 hlcomd.1 ( 𝜑𝐴 ( 𝐾𝐶 ) 𝐵 )
9 1 2 3 4 5 6 7 ishlg ( 𝜑 → ( 𝐴 ( 𝐾𝐶 ) 𝐵 ↔ ( 𝐴𝐶𝐵𝐶 ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) ) ) )
10 8 9 mpbid ( 𝜑 → ( 𝐴𝐶𝐵𝐶 ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) ) )
11 10 simp1d ( 𝜑𝐴𝐶 )