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 𝑃 = ( Base ‘ 𝐺 )
ishlg.i 𝐼 = ( Itv ‘ 𝐺 )
ishlg.k 𝐾 = ( hlG ‘ 𝐺 )
ishlg.a ( 𝜑𝐴𝑃 )
ishlg.b ( 𝜑𝐵𝑃 )
ishlg.c ( 𝜑𝐶𝑃 )
ishlg.g ( 𝜑𝐺𝑉 )
Assertion hlcomb ( 𝜑 → ( 𝐴 ( 𝐾𝐶 ) 𝐵𝐵 ( 𝐾𝐶 ) 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ishlg.p 𝑃 = ( Base ‘ 𝐺 )
2 ishlg.i 𝐼 = ( Itv ‘ 𝐺 )
3 ishlg.k 𝐾 = ( hlG ‘ 𝐺 )
4 ishlg.a ( 𝜑𝐴𝑃 )
5 ishlg.b ( 𝜑𝐵𝑃 )
6 ishlg.c ( 𝜑𝐶𝑃 )
7 ishlg.g ( 𝜑𝐺𝑉 )
8 3ancoma ( ( 𝐴𝐶𝐵𝐶 ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) ) ↔ ( 𝐵𝐶𝐴𝐶 ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) ) )
9 orcom ( ( 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) ↔ ( 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) )
10 9 a1i ( 𝜑 → ( ( 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) ↔ ( 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ) )
11 10 3anbi3d ( 𝜑 → ( ( 𝐵𝐶𝐴𝐶 ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) ) ↔ ( 𝐵𝐶𝐴𝐶 ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ) ) )
12 8 11 syl5bb ( 𝜑 → ( ( 𝐴𝐶𝐵𝐶 ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) ) ↔ ( 𝐵𝐶𝐴𝐶 ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ) ) )
13 1 2 3 4 5 6 7 ishlg ( 𝜑 → ( 𝐴 ( 𝐾𝐶 ) 𝐵 ↔ ( 𝐴𝐶𝐵𝐶 ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) ) ) )
14 1 2 3 5 4 6 7 ishlg ( 𝜑 → ( 𝐵 ( 𝐾𝐶 ) 𝐴 ↔ ( 𝐵𝐶𝐴𝐶 ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ) ) )
15 12 13 14 3bitr4d ( 𝜑 → ( 𝐴 ( 𝐾𝐶 ) 𝐵𝐵 ( 𝐾𝐶 ) 𝐴 ) )