Metamath Proof Explorer


Theorem btwncolg2

Description: Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019)

Ref Expression
Hypotheses tglngval.p 𝑃 = ( Base ‘ 𝐺 )
tglngval.l 𝐿 = ( LineG ‘ 𝐺 )
tglngval.i 𝐼 = ( Itv ‘ 𝐺 )
tglngval.g ( 𝜑𝐺 ∈ TarskiG )
tglngval.x ( 𝜑𝑋𝑃 )
tglngval.y ( 𝜑𝑌𝑃 )
tgcolg.z ( 𝜑𝑍𝑃 )
btwncolg2.z ( 𝜑𝑋 ∈ ( 𝑍 𝐼 𝑌 ) )
Assertion btwncolg2 ( 𝜑 → ( 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ∨ 𝑋 = 𝑌 ) )

Proof

Step Hyp Ref Expression
1 tglngval.p 𝑃 = ( Base ‘ 𝐺 )
2 tglngval.l 𝐿 = ( LineG ‘ 𝐺 )
3 tglngval.i 𝐼 = ( Itv ‘ 𝐺 )
4 tglngval.g ( 𝜑𝐺 ∈ TarskiG )
5 tglngval.x ( 𝜑𝑋𝑃 )
6 tglngval.y ( 𝜑𝑌𝑃 )
7 tgcolg.z ( 𝜑𝑍𝑃 )
8 btwncolg2.z ( 𝜑𝑋 ∈ ( 𝑍 𝐼 𝑌 ) )
9 8 3mix2d ( 𝜑 → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) )
10 1 2 3 4 5 6 7 tgcolg ( 𝜑 → ( ( 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ∨ 𝑋 = 𝑌 ) ↔ ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) )
11 9 10 mpbird ( 𝜑 → ( 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ∨ 𝑋 = 𝑌 ) )