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}={\mathrm{Base}}_{{G}}$
tglngval.l ${⊢}{L}={Line}_{𝒢}\left({G}\right)$
tglngval.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
tglngval.g ${⊢}{\phi }\to {G}\in {𝒢}_{\mathrm{Tarski}}$
tglngval.x ${⊢}{\phi }\to {X}\in {P}$
tglngval.y ${⊢}{\phi }\to {Y}\in {P}$
tglngval.z ${⊢}{\phi }\to {X}\ne {Y}$
tgellng.z ${⊢}{\phi }\to {Z}\in {P}$
Assertion tgellng ${⊢}{\phi }\to \left({Z}\in \left({X}{L}{Y}\right)↔\left({Z}\in \left({X}{I}{Y}\right)\vee {X}\in \left({Z}{I}{Y}\right)\vee {Y}\in \left({X}{I}{Z}\right)\right)\right)$

Proof

Step Hyp Ref Expression
1 tglngval.p ${⊢}{P}={\mathrm{Base}}_{{G}}$
2 tglngval.l ${⊢}{L}={Line}_{𝒢}\left({G}\right)$
3 tglngval.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
4 tglngval.g ${⊢}{\phi }\to {G}\in {𝒢}_{\mathrm{Tarski}}$
5 tglngval.x ${⊢}{\phi }\to {X}\in {P}$
6 tglngval.y ${⊢}{\phi }\to {Y}\in {P}$
7 tglngval.z ${⊢}{\phi }\to {X}\ne {Y}$
8 tgellng.z ${⊢}{\phi }\to {Z}\in {P}$
9 1 2 3 4 5 6 7 tglngval ${⊢}{\phi }\to {X}{L}{Y}=\left\{{z}\in {P}|\left({z}\in \left({X}{I}{Y}\right)\vee {X}\in \left({z}{I}{Y}\right)\vee {Y}\in \left({X}{I}{z}\right)\right)\right\}$
10 9 eleq2d ${⊢}{\phi }\to \left({Z}\in \left({X}{L}{Y}\right)↔{Z}\in \left\{{z}\in {P}|\left({z}\in \left({X}{I}{Y}\right)\vee {X}\in \left({z}{I}{Y}\right)\vee {Y}\in \left({X}{I}{z}\right)\right)\right\}\right)$
11 eleq1 ${⊢}{z}={Z}\to \left({z}\in \left({X}{I}{Y}\right)↔{Z}\in \left({X}{I}{Y}\right)\right)$
12 oveq1 ${⊢}{z}={Z}\to {z}{I}{Y}={Z}{I}{Y}$
13 12 eleq2d ${⊢}{z}={Z}\to \left({X}\in \left({z}{I}{Y}\right)↔{X}\in \left({Z}{I}{Y}\right)\right)$
14 oveq2 ${⊢}{z}={Z}\to {X}{I}{z}={X}{I}{Z}$
15 14 eleq2d ${⊢}{z}={Z}\to \left({Y}\in \left({X}{I}{z}\right)↔{Y}\in \left({X}{I}{Z}\right)\right)$
16 11 13 15 3orbi123d ${⊢}{z}={Z}\to \left(\left({z}\in \left({X}{I}{Y}\right)\vee {X}\in \left({z}{I}{Y}\right)\vee {Y}\in \left({X}{I}{z}\right)\right)↔\left({Z}\in \left({X}{I}{Y}\right)\vee {X}\in \left({Z}{I}{Y}\right)\vee {Y}\in \left({X}{I}{Z}\right)\right)\right)$
17 16 elrab ${⊢}{Z}\in \left\{{z}\in {P}|\left({z}\in \left({X}{I}{Y}\right)\vee {X}\in \left({z}{I}{Y}\right)\vee {Y}\in \left({X}{I}{z}\right)\right)\right\}↔\left({Z}\in {P}\wedge \left({Z}\in \left({X}{I}{Y}\right)\vee {X}\in \left({Z}{I}{Y}\right)\vee {Y}\in \left({X}{I}{Z}\right)\right)\right)$
18 10 17 syl6bb ${⊢}{\phi }\to \left({Z}\in \left({X}{L}{Y}\right)↔\left({Z}\in {P}\wedge \left({Z}\in \left({X}{I}{Y}\right)\vee {X}\in \left({Z}{I}{Y}\right)\vee {Y}\in \left({X}{I}{Z}\right)\right)\right)\right)$
19 8 18 mpbirand ${⊢}{\phi }\to \left({Z}\in \left({X}{L}{Y}\right)↔\left({Z}\in \left({X}{I}{Y}\right)\vee {X}\in \left({Z}{I}{Y}\right)\vee {Y}\in \left({X}{I}{Z}\right)\right)\right)$