# 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}={\mathrm{Base}}_{{G}}$
btwnlng1.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
btwnlng1.l ${⊢}{L}={Line}_{𝒢}\left({G}\right)$
btwnlng1.g ${⊢}{\phi }\to {G}\in {𝒢}_{\mathrm{Tarski}}$
btwnlng1.x ${⊢}{\phi }\to {X}\in {P}$
btwnlng1.y ${⊢}{\phi }\to {Y}\in {P}$
btwnlng1.z ${⊢}{\phi }\to {Z}\in {P}$
btwnlng1.d ${⊢}{\phi }\to {X}\ne {Y}$
lnrot1.1 ${⊢}{\phi }\to {Y}\in \left({Z}{L}{X}\right)$
lnrot1.2 ${⊢}{\phi }\to {Z}\ne {X}$
Assertion lnrot1 ${⊢}{\phi }\to {Z}\in \left({X}{L}{Y}\right)$

### Proof

Step Hyp Ref Expression
1 btwnlng1.p ${⊢}{P}={\mathrm{Base}}_{{G}}$
2 btwnlng1.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
3 btwnlng1.l ${⊢}{L}={Line}_{𝒢}\left({G}\right)$
4 btwnlng1.g ${⊢}{\phi }\to {G}\in {𝒢}_{\mathrm{Tarski}}$
5 btwnlng1.x ${⊢}{\phi }\to {X}\in {P}$
6 btwnlng1.y ${⊢}{\phi }\to {Y}\in {P}$
7 btwnlng1.z ${⊢}{\phi }\to {Z}\in {P}$
8 btwnlng1.d ${⊢}{\phi }\to {X}\ne {Y}$
9 lnrot1.1 ${⊢}{\phi }\to {Y}\in \left({Z}{L}{X}\right)$
10 lnrot1.2 ${⊢}{\phi }\to {Z}\ne {X}$
11 eqid ${⊢}\mathrm{dist}\left({G}\right)=\mathrm{dist}\left({G}\right)$
12 1 11 2 4 6 7 5 tgbtwncomb ${⊢}{\phi }\to \left({Z}\in \left({Y}{I}{X}\right)↔{Z}\in \left({X}{I}{Y}\right)\right)$
13 biidd ${⊢}{\phi }\to \left({X}\in \left({Z}{I}{Y}\right)↔{X}\in \left({Z}{I}{Y}\right)\right)$
14 1 11 2 4 7 6 5 tgbtwncomb ${⊢}{\phi }\to \left({Y}\in \left({Z}{I}{X}\right)↔{Y}\in \left({X}{I}{Z}\right)\right)$
15 12 13 14 3orbi123d ${⊢}{\phi }\to \left(\left({Z}\in \left({Y}{I}{X}\right)\vee {X}\in \left({Z}{I}{Y}\right)\vee {Y}\in \left({Z}{I}{X}\right)\right)↔\left({Z}\in \left({X}{I}{Y}\right)\vee {X}\in \left({Z}{I}{Y}\right)\vee {Y}\in \left({X}{I}{Z}\right)\right)\right)$
16 3orrot ${⊢}\left({Y}\in \left({Z}{I}{X}\right)\vee {Z}\in \left({Y}{I}{X}\right)\vee {X}\in \left({Z}{I}{Y}\right)\right)↔\left({Z}\in \left({Y}{I}{X}\right)\vee {X}\in \left({Z}{I}{Y}\right)\vee {Y}\in \left({Z}{I}{X}\right)\right)$
17 16 a1i ${⊢}{\phi }\to \left(\left({Y}\in \left({Z}{I}{X}\right)\vee {Z}\in \left({Y}{I}{X}\right)\vee {X}\in \left({Z}{I}{Y}\right)\right)↔\left({Z}\in \left({Y}{I}{X}\right)\vee {X}\in \left({Z}{I}{Y}\right)\vee {Y}\in \left({Z}{I}{X}\right)\right)\right)$
18 1 3 2 4 5 6 8 7 tgellng ${⊢}{\phi }\to \left({Z}\in \left({X}{L}{Y}\right)↔\left({Z}\in \left({X}{I}{Y}\right)\vee {X}\in \left({Z}{I}{Y}\right)\vee {Y}\in \left({X}{I}{Z}\right)\right)\right)$
19 15 17 18 3bitr4rd ${⊢}{\phi }\to \left({Z}\in \left({X}{L}{Y}\right)↔\left({Y}\in \left({Z}{I}{X}\right)\vee {Z}\in \left({Y}{I}{X}\right)\vee {X}\in \left({Z}{I}{Y}\right)\right)\right)$
20 1 3 2 4 7 5 10 6 tgellng ${⊢}{\phi }\to \left({Y}\in \left({Z}{L}{X}\right)↔\left({Y}\in \left({Z}{I}{X}\right)\vee {Z}\in \left({Y}{I}{X}\right)\vee {X}\in \left({Z}{I}{Y}\right)\right)\right)$
21 19 20 bitr4d ${⊢}{\phi }\to \left({Z}\in \left({X}{L}{Y}\right)↔{Y}\in \left({Z}{L}{X}\right)\right)$
22 9 21 mpbird ${⊢}{\phi }\to {Z}\in \left({X}{L}{Y}\right)$