Metamath Proof Explorer

Theorem ncolrot1

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

Ref Expression
Hypotheses tglngval.p ⊢ P = Base G
tglngval.l ⊢ L = Line 𝒢 ⁡ G
tglngval.i ⊢ I = Itv ⁡ G
tglngval.g ⊢ φ → G ∈ 𝒢 Tarski
tglngval.x ⊢ φ → X ∈ P
tglngval.y ⊢ φ → Y ∈ P
tgcolg.z ⊢ φ → Z ∈ P
ncolrot ⊢ φ → ¬ Z ∈ X L Y ∨ X = Y
Assertion ncolrot1 ⊢ φ → ¬ X ∈ Y L Z ∨ Y = Z

Proof

Step Hyp Ref Expression
1 tglngval.p ⊢ P = Base G
2 tglngval.l ⊢ L = Line 𝒢 ⁡ G
3 tglngval.i ⊢ I = Itv ⁡ G
4 tglngval.g ⊢ φ → G ∈ 𝒢 Tarski
5 tglngval.x ⊢ φ → X ∈ P
6 tglngval.y ⊢ φ → Y ∈ P
7 tgcolg.z ⊢ φ → Z ∈ P
8 ncolrot ⊢ φ → ¬ Z ∈ X L Y ∨ X = Y
9 4 adantr ⊢ φ ∧ X ∈ Y L Z ∨ Y = Z → G ∈ 𝒢 Tarski
10 6 adantr ⊢ φ ∧ X ∈ Y L Z ∨ Y = Z → Y ∈ P
11 7 adantr ⊢ φ ∧ X ∈ Y L Z ∨ Y = Z → Z ∈ P
12 5 adantr ⊢ φ ∧ X ∈ Y L Z ∨ Y = Z → X ∈ P
13 simpr ⊢ φ ∧ X ∈ Y L Z ∨ Y = Z → X ∈ Y L Z ∨ Y = Z
14 1 2 3 9 10 11 12 13 colrot2 ⊢ φ ∧ X ∈ Y L Z ∨ Y = Z → Z ∈ X L Y ∨ X = Y
15 8 14 mtand ⊢ φ → ¬ X ∈ Y L Z ∨ Y = Z