Metamath Proof Explorer

Theorem lnrot1

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 )
lnrot1.1 
|- ( ph -> Y e. ( Z L X ) )
lnrot1.2 
|- ( ph -> Z =/= X )
Assertion lnrot1 
|- ( 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 lnrot1.1 
 |-  ( ph -> Y e. ( Z L X ) )
10 lnrot1.2 
 |-  ( ph -> Z =/= X )
11 eqid 
 |-  ( dist ` G ) = ( dist ` G )
12 1 11 2 4 6 7 5 tgbtwncomb 
 |-  ( ph -> ( Z e. ( Y I X ) <-> Z e. ( X I Y ) ) )
13 biidd 
 |-  ( ph -> ( X e. ( Z I Y ) <-> X e. ( Z I Y ) ) )
14 1 11 2 4 7 6 5 tgbtwncomb 
 |-  ( ph -> ( Y e. ( Z I X ) <-> Y e. ( X I Z ) ) )
15 12 13 14 3orbi123d 
 |-  ( ph -> ( ( Z e. ( Y I X ) \/ X e. ( Z I Y ) \/ Y e. ( Z I X ) ) <-> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) )
16 3orrot 
 |-  ( ( Y e. ( Z I X ) \/ Z e. ( Y I X ) \/ X e. ( Z I Y ) ) <-> ( Z e. ( Y I X ) \/ X e. ( Z I Y ) \/ Y e. ( Z I X ) ) )
17 16 a1i 
 |-  ( ph -> ( ( Y e. ( Z I X ) \/ Z e. ( Y I X ) \/ X e. ( Z I Y ) ) <-> ( Z e. ( Y I X ) \/ X e. ( Z I Y ) \/ Y e. ( Z I X ) ) ) )
18 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 ) ) ) )
19 15 17 18 3bitr4rd 
 |-  ( ph -> ( Z e. ( X L Y ) <-> ( Y e. ( Z I X ) \/ Z e. ( Y I X ) \/ X e. ( Z I Y ) ) ) )
20 1 3 2 4 7 5 10 6 tgellng 
 |-  ( ph -> ( Y e. ( Z L X ) <-> ( Y e. ( Z I X ) \/ Z e. ( Y I X ) \/ X e. ( Z I Y ) ) ) )
21 19 20 bitr4d 
 |-  ( ph -> ( Z e. ( X L Y ) <-> Y e. ( Z L X ) ) )
22 9 21 mpbird 
 |-  ( ph -> Z e. ( X L Y ) )