Metamath Proof Explorer

Theorem tgellng

Description: Property of lying on the line going through points X and Y . Definition 4.10 of Schwabhauser p. 36. We choose the notation Z e. ( X ( LineGG ) Y ) instead of "colinear" because LineG is a common structure slot for other axiomatizations of geometry. (Contributed by Thierry Arnoux, 28-Mar-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
tglngval.z ⊢ φ → X ≠ Y
tgellng.z ⊢ φ → Z ∈ P
Assertion tgellng ⊢ φ → Z ∈ X L Y ↔ Z ∈ X I Y ∨ X ∈ Z I Y ∨ Y ∈ X I 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 tglngval.z ⊢ φ → X ≠ Y
8 tgellng.z ⊢ φ → Z ∈ P
9 1 2 3 4 5 6 7 tglngval ⊢ φ → X L Y = z ∈ P | z ∈ X I Y ∨ X ∈ z I Y ∨ Y ∈ X I z
10 9 eleq2d ⊢ φ → Z ∈ X L Y ↔ Z ∈ z ∈ P | z ∈ X I Y ∨ X ∈ z I Y ∨ Y ∈ X I z
11 eleq1 ⊢ z = Z → z ∈ X I Y ↔ Z ∈ X I Y
12 oveq1 ⊢ z = Z → z I Y = Z I Y
13 12 eleq2d ⊢ z = Z → X ∈ z I Y ↔ X ∈ Z I Y
14 oveq2 ⊢ z = Z → X I z = X I Z
15 14 eleq2d ⊢ z = Z → Y ∈ X I z ↔ Y ∈ X I Z
16 11 13 15 3orbi123d ⊢ z = Z → z ∈ X I Y ∨ X ∈ z I Y ∨ Y ∈ X I z ↔ Z ∈ X I Y ∨ X ∈ Z I Y ∨ Y ∈ X I Z
17 16 elrab ⊢ Z ∈ z ∈ P | z ∈ X I Y ∨ X ∈ z I Y ∨ Y ∈ X I z ↔ Z ∈ P ∧ Z ∈ X I Y ∨ X ∈ Z I Y ∨ Y ∈ X I Z
18 10 17 syl6bb ⊢ φ → Z ∈ X L Y ↔ Z ∈ P ∧ Z ∈ X I Y ∨ X ∈ Z I Y ∨ Y ∈ X I Z
19 8 18 mpbirand ⊢ φ → Z ∈ X L Y ↔ Z ∈ X I Y ∨ X ∈ Z I Y ∨ Y ∈ X I Z