Theorem hlcomb

Description: The half-line relation commutes. Theorem 6.6 of Schwabhauser p. 44. (Contributed by Thierry Arnoux, 21-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 )
Assertion	hlcomb	|- ( ph -> ( A ( K ` C ) B <-> B ( K ` C ) A ) )

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		3ancoma	|- ( ( A =/= C /\ B =/= C /\ ( A e. ( C I B ) \/ B e. ( C I A ) ) ) <-> ( B =/= C /\ A =/= C /\ ( A e. ( C I B ) \/ B e. ( C I A ) ) ) )
9		orcom	|- ( ( A e. ( C I B ) \/ B e. ( C I A ) ) <-> ( B e. ( C I A ) \/ A e. ( C I B ) ) )
10	9	a1i	|- ( ph -> ( ( A e. ( C I B ) \/ B e. ( C I A ) ) <-> ( B e. ( C I A ) \/ A e. ( C I B ) ) ) )
11	10	3anbi3d	|- ( ph -> ( ( B =/= C /\ A =/= C /\ ( A e. ( C I B ) \/ B e. ( C I A ) ) ) <-> ( B =/= C /\ A =/= C /\ ( B e. ( C I A ) \/ A e. ( C I B ) ) ) ) )
12	8 11	bitrid	|- ( ph -> ( ( A =/= C /\ B =/= C /\ ( A e. ( C I B ) \/ B e. ( C I A ) ) ) <-> ( B =/= C /\ A =/= C /\ ( B e. ( C I A ) \/ A e. ( C I B ) ) ) ) )
13	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 ) ) ) ) )
14	1 2 3 5 4 6 7	ishlg	|- ( ph -> ( B ( K ` C ) A <-> ( B =/= C /\ A =/= C /\ ( B e. ( C I A ) \/ A e. ( C I B ) ) ) ) )
15	12 13 14	3bitr4d	|- ( ph -> ( A ( K ` C ) B <-> B ( K ` C ) A ) )