Metamath Proof Explorer


Theorem ncolcom

Description: Swapping non-colinear points. (Contributed by Thierry Arnoux, 19-Oct-2019)

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

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 ncolrot ( 𝜑 → ¬ ( 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ∨ 𝑋 = 𝑌 ) )
9 4 adantr ( ( 𝜑 ∧ ( 𝑍 ∈ ( 𝑌 𝐿 𝑋 ) ∨ 𝑌 = 𝑋 ) ) → 𝐺 ∈ TarskiG )
10 6 adantr ( ( 𝜑 ∧ ( 𝑍 ∈ ( 𝑌 𝐿 𝑋 ) ∨ 𝑌 = 𝑋 ) ) → 𝑌𝑃 )
11 5 adantr ( ( 𝜑 ∧ ( 𝑍 ∈ ( 𝑌 𝐿 𝑋 ) ∨ 𝑌 = 𝑋 ) ) → 𝑋𝑃 )
12 7 adantr ( ( 𝜑 ∧ ( 𝑍 ∈ ( 𝑌 𝐿 𝑋 ) ∨ 𝑌 = 𝑋 ) ) → 𝑍𝑃 )
13 simpr ( ( 𝜑 ∧ ( 𝑍 ∈ ( 𝑌 𝐿 𝑋 ) ∨ 𝑌 = 𝑋 ) ) → ( 𝑍 ∈ ( 𝑌 𝐿 𝑋 ) ∨ 𝑌 = 𝑋 ) )
14 1 2 3 9 10 11 12 13 colcom ( ( 𝜑 ∧ ( 𝑍 ∈ ( 𝑌 𝐿 𝑋 ) ∨ 𝑌 = 𝑋 ) ) → ( 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ∨ 𝑋 = 𝑌 ) )
15 8 14 mtand ( 𝜑 → ¬ ( 𝑍 ∈ ( 𝑌 𝐿 𝑋 ) ∨ 𝑌 = 𝑋 ) )