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 = ( LineG ` G )
	tglngval.i	|- I = ( Itv ` G )
	tglngval.g	|- ( ph -> G e. TarskiG )
	tglngval.x	|- ( ph -> X e. P )
	tglngval.y	|- ( ph -> Y e. P )
	tglngval.z	|- ( ph -> X =/= Y )
	tgellng.z	|- ( ph -> Z e. P )
Assertion	tgellng	|- ( ph -> ( Z e. ( X L Y ) <-> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		tglngval.p	|- P = ( Base ` G )
2		tglngval.l	|- L = ( LineG ` G )
3		tglngval.i	|- I = ( Itv ` G )
4		tglngval.g	|- ( ph -> G e. TarskiG )
5		tglngval.x	|- ( ph -> X e. P )
6		tglngval.y	|- ( ph -> Y e. P )
7		tglngval.z	|- ( ph -> X =/= Y )
8		tgellng.z	|- ( ph -> Z e. P )
9	1 2 3 4 5 6 7	tglngval	|- ( ph -> ( X L Y ) = { z e. P | ( z e. ( X I Y ) \/ X e. ( z I Y ) \/ Y e. ( X I z ) ) } )
10	9	eleq2d	|- ( ph -> ( Z e. ( X L Y ) <-> Z e. { z e. P | ( z e. ( X I Y ) \/ X e. ( z I Y ) \/ Y e. ( X I z ) ) } ) )
11		eleq1	|- ( z = Z -> ( z e. ( X I Y ) <-> Z e. ( X I Y ) ) )
12		oveq1	|- ( z = Z -> ( z I Y ) = ( Z I Y ) )
13	12	eleq2d	|- ( z = Z -> ( X e. ( z I Y ) <-> X e. ( Z I Y ) ) )
14		oveq2	|- ( z = Z -> ( X I z ) = ( X I Z ) )
15	14	eleq2d	|- ( z = Z -> ( Y e. ( X I z ) <-> Y e. ( X I Z ) ) )
16	11 13 15	3orbi123d	|- ( z = Z -> ( ( z e. ( X I Y ) \/ X e. ( z I Y ) \/ Y e. ( X I z ) ) <-> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) )
17	16	elrab	|- ( Z e. { z e. P | ( z e. ( X I Y ) \/ X e. ( z I Y ) \/ Y e. ( X I z ) ) } <-> ( Z e. P /\ ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) )
18	10 17	bitrdi	|- ( ph -> ( Z e. ( X L Y ) <-> ( Z e. P /\ ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) ) )
19	8 18	mpbirand	|- ( ph -> ( Z e. ( X L Y ) <-> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) )