Theorem lnrot2

Description: Rotating the points defining a line. 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 )
	lnrot2.1	|- ( ph -> X e. ( Y L Z ) )
	lnrot2.2	|- ( ph -> Y =/= Z )
Assertion	lnrot2	|- ( 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		lnrot2.1	|- ( ph -> X e. ( Y L Z ) )
10		lnrot2.2	|- ( ph -> Y =/= Z )
11		eqid	|- ( dist ` G ) = ( dist ` G )
12	1 11 2 4 6 5 7	tgbtwncomb	|- ( ph -> ( X e. ( Y I Z ) <-> X e. ( Z I Y ) ) )
13		biidd	|- ( ph -> ( Y e. ( X I Z ) <-> Y e. ( X I Z ) ) )
14	1 11 2 4 6 7 5	tgbtwncomb	|- ( ph -> ( Z e. ( Y I X ) <-> Z e. ( X I Y ) ) )
15	12 13 14	3orbi123d	|- ( ph -> ( ( X e. ( Y I Z ) \/ Y e. ( X I Z ) \/ Z e. ( Y I X ) ) <-> ( X e. ( Z I Y ) \/ Y e. ( X I Z ) \/ Z e. ( X I Y ) ) ) )
16		3orrot	|- ( ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) <-> ( X e. ( Z I Y ) \/ Y e. ( X I Z ) \/ Z e. ( X I Y ) ) )
17	15 16	bitr4di	|- ( ph -> ( ( X e. ( Y I Z ) \/ Y e. ( X I Z ) \/ Z e. ( Y I X ) ) <-> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) )
18	1 3 2 4 6 7 10 5	tgellng	|- ( ph -> ( X e. ( Y L Z ) <-> ( X e. ( Y I Z ) \/ Y e. ( X I Z ) \/ Z e. ( Y I X ) ) ) )
19	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 ) ) ) )
20	17 18 19	3bitr4d	|- ( ph -> ( X e. ( Y L Z ) <-> Z e. ( X L Y ) ) )
21	9 20	mpbid	|- ( ph -> Z e. ( X L Y ) )