Theorem colcom

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	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 )
	tgcolg.z	|- ( ph -> Z e. P )
	colrot	|- ( ph -> ( Z e. ( X L Y ) \/ X = Y ) )
Assertion	colcom	|- ( ph -> ( Z e. ( Y L X ) \/ Y = X ) )

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		tgcolg.z	|- ( ph -> Z e. P )
8		colrot	|- ( ph -> ( Z e. ( X L Y ) \/ X = Y ) )
9		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 ) ) )
10		eqid	|- ( dist ` G ) = ( dist ` G )
11	1 10 3 4 5 7 6	tgbtwncomb	|- ( ph -> ( Z e. ( X I Y ) <-> Z e. ( Y I X ) ) )
12	1 10 3 4 5 6 7	tgbtwncomb	|- ( ph -> ( Y e. ( X I Z ) <-> Y e. ( Z I X ) ) )
13	1 10 3 4 7 5 6	tgbtwncomb	|- ( ph -> ( X e. ( Z I Y ) <-> X e. ( Y I Z ) ) )
14	11 12 13	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 ) ) ) )
15	9 14	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 ) ) ) )
16	1 2 3 4 5 6 7	tgcolg	|- ( ph -> ( ( Z e. ( X L Y ) \/ X = Y ) <-> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) )
17	1 2 3 4 6 5 7	tgcolg	|- ( ph -> ( ( Z e. ( Y L X ) \/ Y = X ) <-> ( Z e. ( Y I X ) \/ Y e. ( Z I X ) \/ X e. ( Y I Z ) ) ) )
18	15 16 17	3bitr4d	|- ( ph -> ( ( Z e. ( X L Y ) \/ X = Y ) <-> ( Z e. ( Y L X ) \/ Y = X ) ) )
19	8 18	mpbid	|- ( ph -> ( Z e. ( Y L X ) \/ Y = X ) )