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 = Base G
ishlg.i ⊢ I = Itv ⁡ G
ishlg.k ⊢ K = hl 𝒢 ⁡ G
ishlg.a ⊢ φ → A ∈ P
ishlg.b ⊢ φ → B ∈ P
ishlg.c ⊢ φ → C ∈ P
ishlg.g ⊢ φ → G ∈ V
Assertion hlcomb ⊢ φ → 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 = hl 𝒢 ⁡ G
4 ishlg.a ⊢ φ → A ∈ P
5 ishlg.b ⊢ φ → B ∈ P
6 ishlg.c ⊢ φ → C ∈ P
7 ishlg.g ⊢ φ → G ∈ V
8 3ancoma ⊢ A ≠ C ∧ B ≠ C ∧ A ∈ C I B ∨ B ∈ C I A ↔ B ≠ C ∧ A ≠ C ∧ A ∈ C I B ∨ B ∈ C I A
9 orcom ⊢ A ∈ C I B ∨ B ∈ C I A ↔ B ∈ C I A ∨ A ∈ C I B
10 9 a1i ⊢ φ → A ∈ C I B ∨ B ∈ C I A ↔ B ∈ C I A ∨ A ∈ C I B
11 10 3anbi3d ⊢ φ → B ≠ C ∧ A ≠ C ∧ A ∈ C I B ∨ B ∈ C I A ↔ B ≠ C ∧ A ≠ C ∧ B ∈ C I A ∨ A ∈ C I B
12 8 11 syl5bb ⊢ φ → A ≠ C ∧ B ≠ C ∧ A ∈ C I B ∨ B ∈ C I A ↔ B ≠ C ∧ A ≠ C ∧ B ∈ C I A ∨ A ∈ C I B
13 1 2 3 4 5 6 7 ishlg ⊢ φ → A K ⁡ C B ↔ A ≠ C ∧ B ≠ C ∧ A ∈ C I B ∨ B ∈ C I A
14 1 2 3 5 4 6 7 ishlg ⊢ φ → B K ⁡ C A ↔ B ≠ C ∧ A ≠ C ∧ B ∈ C I A ∨ A ∈ C I B
15 12 13 14 3bitr4d ⊢ φ → A K ⁡ C B ↔ B K ⁡ C A