Theorem hlcomd

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 )
	hlcomd.1	|- ( ph -> A ( K ` C ) B )
Assertion	hlcomd	|- ( ph -> 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		hlcomd.1	|- ( ph -> A ( K ` C ) B )
9	1 2 3 4 5 6 7	hlcomb	|- ( ph -> ( A ( K ` C ) B <-> B ( K ` C ) A ) )
10	8 9	mpbid	|- ( ph -> B ( K ` C ) A )