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=BaseG
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∈XLY↔Z∈XIY∨X∈ZIY∨Y∈XIZ

Proof

Step Hyp Ref Expression
1 tglngval.p ⊢P=BaseG
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 ⊢φ→XLY=z∈P|z∈XIY∨X∈zIY∨Y∈XIz
10 9 eleq2d ⊢φ→Z∈XLY↔Z∈z∈P|z∈XIY∨X∈zIY∨Y∈XIz
11 eleq1 ⊢z=Z→z∈XIY↔Z∈XIY
12 oveq1 ⊢z=Z→zIY=ZIY
13 12 eleq2d ⊢z=Z→X∈zIY↔X∈ZIY
14 oveq2 ⊢z=Z→XIz=XIZ
15 14 eleq2d ⊢z=Z→Y∈XIz↔Y∈XIZ
16 11 13 15 3orbi123d ⊢z=Z→z∈XIY∨X∈zIY∨Y∈XIz↔Z∈XIY∨X∈ZIY∨Y∈XIZ
17 16 elrab ⊢Z∈z∈P|z∈XIY∨X∈zIY∨Y∈XIz↔Z∈P∧Z∈XIY∨X∈ZIY∨Y∈XIZ
18 10 17 bitrdi ⊢φ→Z∈XLY↔Z∈P∧Z∈XIY∨X∈ZIY∨Y∈XIZ
19 8 18 mpbirand ⊢φ→Z∈XLY↔Z∈XIY∨X∈ZIY∨Y∈XIZ