Metamath Proof Explorer


Theorem colrot1

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