# 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 ) )`