Theorem hlne1

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	hlne1	|- ( ph -> A =/= 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	simp1d	|- ( ph -> A =/= C )