Metamath Proof Explorer


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

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 3ancoma ACBCACIBBCIABCACACIBBCIA
9 orcom ACIBBCIABCIAACIB
10 9 a1i φACIBBCIABCIAACIB
11 10 3anbi3d φBCACACIBBCIABCACBCIAACIB
12 8 11 syl5bb φACBCACIBBCIABCACBCIAACIB
13 1 2 3 4 5 6 7 ishlg φAKCBACBCACIBBCIA
14 1 2 3 5 4 6 7 ishlg φBKCABCACBCIAACIB
15 12 13 14 3bitr4d φAKCBBKCA