Metamath Proof Explorer


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=BaseG
ishlg.i I=ItvG
ishlg.k K=hl𝒢G
ishlg.a φAP
ishlg.b φBP
ishlg.c φCP
ishlg.g φGV
hlcomd.1 φAKCB
Assertion hlcomd φBKCA

Proof

Step Hyp Ref Expression
1 ishlg.p P=BaseG
2 ishlg.i I=ItvG
3 ishlg.k K=hl𝒢G
4 ishlg.a φAP
5 ishlg.b φBP
6 ishlg.c φCP
7 ishlg.g φGV
8 hlcomd.1 φAKCB
9 1 2 3 4 5 6 7 hlcomb φAKCBBKCA
10 8 9 mpbid φBKCA