Metamath Proof Explorer


Theorem hlne2

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

Ref Expression
Hypotheses ishlg.p
|- P = ( Base ` G )
ishlg.i
|- I = ( Itv ` G )
ishlg.k
|- K = ( hlG ` G )
ishlg.a
|- ( ph -> A e. P )
ishlg.b
|- ( ph -> B e. P )
ishlg.c
|- ( ph -> C e. P )
ishlg.g
|- ( ph -> G e. V )
hlcomd.1
|- ( ph -> A ( K ` C ) B )
Assertion hlne2
|- ( ph -> B =/= C )

Proof

Step Hyp Ref Expression
1 ishlg.p
 |-  P = ( Base ` G )
2 ishlg.i
 |-  I = ( Itv ` G )
3 ishlg.k
 |-  K = ( hlG ` G )
4 ishlg.a
 |-  ( ph -> A e. P )
5 ishlg.b
 |-  ( ph -> B e. P )
6 ishlg.c
 |-  ( ph -> C e. P )
7 ishlg.g
 |-  ( ph -> G e. V )
8 hlcomd.1
 |-  ( ph -> A ( K ` C ) B )
9 1 2 3 4 5 6 7 ishlg
 |-  ( ph -> ( A ( K ` C ) B <-> ( A =/= C /\ B =/= C /\ ( A e. ( C I B ) \/ B e. ( C I A ) ) ) ) )
10 8 9 mpbid
 |-  ( ph -> ( A =/= C /\ B =/= C /\ ( A e. ( C I B ) \/ B e. ( C I A ) ) ) )
11 10 simp2d
 |-  ( ph -> B =/= C )