Metamath Proof Explorer


Theorem ncolrot2

Description: Rotating non-colinear points. (Contributed by Thierry Arnoux, 19-Oct-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 )
ncolrot
|- ( ph -> -. ( Z e. ( X L Y ) \/ X = Y ) )
Assertion ncolrot2
|- ( ph -> -. ( Y e. ( Z L X ) \/ Z = 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 ncolrot
 |-  ( ph -> -. ( Z e. ( X L Y ) \/ X = Y ) )
9 4 adantr
 |-  ( ( ph /\ ( Y e. ( Z L X ) \/ Z = X ) ) -> G e. TarskiG )
10 7 adantr
 |-  ( ( ph /\ ( Y e. ( Z L X ) \/ Z = X ) ) -> Z e. P )
11 5 adantr
 |-  ( ( ph /\ ( Y e. ( Z L X ) \/ Z = X ) ) -> X e. P )
12 6 adantr
 |-  ( ( ph /\ ( Y e. ( Z L X ) \/ Z = X ) ) -> Y e. P )
13 simpr
 |-  ( ( ph /\ ( Y e. ( Z L X ) \/ Z = X ) ) -> ( Y e. ( Z L X ) \/ Z = X ) )
14 1 2 3 9 10 11 12 13 colrot1
 |-  ( ( ph /\ ( Y e. ( Z L X ) \/ Z = X ) ) -> ( Z e. ( X L Y ) \/ X = Y ) )
15 8 14 mtand
 |-  ( ph -> -. ( Y e. ( Z L X ) \/ Z = X ) )