Metamath Proof Explorer

Theorem lnrot2

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}$
lnrot2.1 ${⊢}{\phi }\to {X}\in \left({Y}{L}{Z}\right)$
lnrot2.2 ${⊢}{\phi }\to {Y}\ne {Z}$
Assertion lnrot2 ${⊢}{\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 lnrot2.1 ${⊢}{\phi }\to {X}\in \left({Y}{L}{Z}\right)$
10 lnrot2.2 ${⊢}{\phi }\to {Y}\ne {Z}$
11 eqid ${⊢}\mathrm{dist}\left({G}\right)=\mathrm{dist}\left({G}\right)$
12 1 11 2 4 6 5 7 tgbtwncomb ${⊢}{\phi }\to \left({X}\in \left({Y}{I}{Z}\right)↔{X}\in \left({Z}{I}{Y}\right)\right)$
13 biidd ${⊢}{\phi }\to \left({Y}\in \left({X}{I}{Z}\right)↔{Y}\in \left({X}{I}{Z}\right)\right)$
14 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)$
15 12 13 14 3orbi123d ${⊢}{\phi }\to \left(\left({X}\in \left({Y}{I}{Z}\right)\vee {Y}\in \left({X}{I}{Z}\right)\vee {Z}\in \left({Y}{I}{X}\right)\right)↔\left({X}\in \left({Z}{I}{Y}\right)\vee {Y}\in \left({X}{I}{Z}\right)\vee {Z}\in \left({X}{I}{Y}\right)\right)\right)$
16 3orrot ${⊢}\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)↔\left({X}\in \left({Z}{I}{Y}\right)\vee {Y}\in \left({X}{I}{Z}\right)\vee {Z}\in \left({X}{I}{Y}\right)\right)$
17 15 16 syl6bbr ${⊢}{\phi }\to \left(\left({X}\in \left({Y}{I}{Z}\right)\vee {Y}\in \left({X}{I}{Z}\right)\vee {Z}\in \left({Y}{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)$
18 1 3 2 4 6 7 10 5 tgellng ${⊢}{\phi }\to \left({X}\in \left({Y}{L}{Z}\right)↔\left({X}\in \left({Y}{I}{Z}\right)\vee {Y}\in \left({X}{I}{Z}\right)\vee {Z}\in \left({Y}{I}{X}\right)\right)\right)$
19 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)$
20 17 18 19 3bitr4d ${⊢}{\phi }\to \left({X}\in \left({Y}{L}{Z}\right)↔{Z}\in \left({X}{L}{Y}\right)\right)$
21 9 20 mpbid ${⊢}{\phi }\to {Z}\in \left({X}{L}{Y}\right)$