Theorem lncom

Description: Swapping the points defining a line keeps it unchanged. Part of Theorem 4.11 of Schwabhauser p. 34. (Contributed by Thierry Arnoux, 3-Apr-2019)

	Ref	Expression
Hypotheses	btwnlng1.p	|- P = ( Base ` G )
	btwnlng1.i	|- I = ( Itv ` G )
	btwnlng1.l	|- L = ( LineG ` G )
	btwnlng1.g	|- ( ph -> G e. TarskiG )
	btwnlng1.x	|- ( ph -> X e. P )
	btwnlng1.y	|- ( ph -> Y e. P )
	btwnlng1.z	|- ( ph -> Z e. P )
	btwnlng1.d	|- ( ph -> X =/= Y )
	lncom.1	|- ( ph -> Z e. ( Y L X ) )
Assertion	lncom	|- ( ph -> Z e. ( X L Y ) )

Proof

Step	Hyp	Ref	Expression
1		btwnlng1.p	|- P = ( Base ` G )
2		btwnlng1.i	|- I = ( Itv ` G )
3		btwnlng1.l	|- L = ( LineG ` G )
4		btwnlng1.g	|- ( ph -> G e. TarskiG )
5		btwnlng1.x	|- ( ph -> X e. P )
6		btwnlng1.y	|- ( ph -> Y e. P )
7		btwnlng1.z	|- ( ph -> Z e. P )
8		btwnlng1.d	|- ( ph -> X =/= Y )
9		lncom.1	|- ( ph -> Z e. ( Y L X ) )
10		3orcomb	|- ( ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) <-> ( Z e. ( X I Y ) \/ Y e. ( X I Z ) \/ X e. ( Z I Y ) ) )
11		eqid	|- ( dist ` G ) = ( dist ` G )
12	1 11 2 4 5 7 6	tgbtwncomb	|- ( ph -> ( Z e. ( X I Y ) <-> Z e. ( Y I X ) ) )
13	1 11 2 4 5 6 7	tgbtwncomb	|- ( ph -> ( Y e. ( X I Z ) <-> Y e. ( Z I X ) ) )
14	1 11 2 4 7 5 6	tgbtwncomb	|- ( ph -> ( X e. ( Z I Y ) <-> X e. ( Y I Z ) ) )
15	12 13 14	3orbi123d	|- ( ph -> ( ( Z e. ( X I Y ) \/ Y e. ( X I Z ) \/ X e. ( Z I Y ) ) <-> ( Z e. ( Y I X ) \/ Y e. ( Z I X ) \/ X e. ( Y I Z ) ) ) )
16	10 15	syl5bb	|- ( ph -> ( ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) <-> ( Z e. ( Y I X ) \/ Y e. ( Z I X ) \/ X e. ( Y I Z ) ) ) )
17	1 3 2 4 5 6 8 7	tgellng	|- ( ph -> ( Z e. ( X L Y ) <-> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) )
18	8	necomd	|- ( ph -> Y =/= X )
19	1 3 2 4 6 5 18 7	tgellng	|- ( ph -> ( Z e. ( Y L X ) <-> ( Z e. ( Y I X ) \/ Y e. ( Z I X ) \/ X e. ( Y I Z ) ) ) )
20	16 17 19	3bitr4d	|- ( ph -> ( Z e. ( X L Y ) <-> Z e. ( Y L X ) ) )
21	9 20	mpbird	|- ( ph -> Z e. ( X L Y ) )