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=ItvG
tglngval.g φG𝒢Tarski
tglngval.x φXP
tglngval.y φYP
tglngval.z φXY
tgellng.z φZP
Assertion tgellng φZXLYZXIYXZIYYXIZ

Proof

Step Hyp Ref Expression
1 tglngval.p P=BaseG
2 tglngval.l L=Line𝒢G
3 tglngval.i I=ItvG
4 tglngval.g φG𝒢Tarski
5 tglngval.x φXP
6 tglngval.y φYP
7 tglngval.z φXY
8 tgellng.z φZP
9 1 2 3 4 5 6 7 tglngval φXLY=zP|zXIYXzIYYXIz
10 9 eleq2d φZXLYZzP|zXIYXzIYYXIz
11 eleq1 z=ZzXIYZXIY
12 oveq1 z=ZzIY=ZIY
13 12 eleq2d z=ZXzIYXZIY
14 oveq2 z=ZXIz=XIZ
15 14 eleq2d z=ZYXIzYXIZ
16 11 13 15 3orbi123d z=ZzXIYXzIYYXIzZXIYXZIYYXIZ
17 16 elrab ZzP|zXIYXzIYYXIzZPZXIYXZIYYXIZ
18 10 17 bitrdi φZXLYZPZXIYXZIYYXIZ
19 8 18 mpbirand φZXLYZXIYXZIYYXIZ