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 𝑃 = ( Base ‘ 𝐺 )
btwnlng1.i 𝐼 = ( Itv ‘ 𝐺 )
btwnlng1.l 𝐿 = ( LineG ‘ 𝐺 )
btwnlng1.g ( 𝜑𝐺 ∈ TarskiG )
btwnlng1.x ( 𝜑𝑋𝑃 )
btwnlng1.y ( 𝜑𝑌𝑃 )
btwnlng1.z ( 𝜑𝑍𝑃 )
btwnlng1.d ( 𝜑𝑋𝑌 )
lnrot1.1 ( 𝜑𝑌 ∈ ( 𝑍 𝐿 𝑋 ) )
lnrot1.2 ( 𝜑𝑍𝑋 )
Assertion lnrot1 ( 𝜑𝑍 ∈ ( 𝑋 𝐿 𝑌 ) )

Proof

Step Hyp Ref Expression
1 btwnlng1.p 𝑃 = ( Base ‘ 𝐺 )
2 btwnlng1.i 𝐼 = ( Itv ‘ 𝐺 )
3 btwnlng1.l 𝐿 = ( LineG ‘ 𝐺 )
4 btwnlng1.g ( 𝜑𝐺 ∈ TarskiG )
5 btwnlng1.x ( 𝜑𝑋𝑃 )
6 btwnlng1.y ( 𝜑𝑌𝑃 )
7 btwnlng1.z ( 𝜑𝑍𝑃 )
8 btwnlng1.d ( 𝜑𝑋𝑌 )
9 lnrot1.1 ( 𝜑𝑌 ∈ ( 𝑍 𝐿 𝑋 ) )
10 lnrot1.2 ( 𝜑𝑍𝑋 )
11 eqid ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
12 1 11 2 4 6 7 5 tgbtwncomb ( 𝜑 → ( 𝑍 ∈ ( 𝑌 𝐼 𝑋 ) ↔ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) )
13 biidd ( 𝜑 → ( 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ↔ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ) )
14 1 11 2 4 7 6 5 tgbtwncomb ( 𝜑 → ( 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ↔ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) )
15 12 13 14 3orbi123d ( 𝜑 → ( ( 𝑍 ∈ ( 𝑌 𝐼 𝑋 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ↔ ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) )
16 3orrot ( ( 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ∨ 𝑍 ∈ ( 𝑌 𝐼 𝑋 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ) ↔ ( 𝑍 ∈ ( 𝑌 𝐼 𝑋 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) )
17 16 a1i ( 𝜑 → ( ( 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ∨ 𝑍 ∈ ( 𝑌 𝐼 𝑋 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ) ↔ ( 𝑍 ∈ ( 𝑌 𝐼 𝑋 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ) )
18 1 3 2 4 5 6 8 7 tgellng ( 𝜑 → ( 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ↔ ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) )
19 15 17 18 3bitr4rd ( 𝜑 → ( 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ↔ ( 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ∨ 𝑍 ∈ ( 𝑌 𝐼 𝑋 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ) ) )
20 1 3 2 4 7 5 10 6 tgellng ( 𝜑 → ( 𝑌 ∈ ( 𝑍 𝐿 𝑋 ) ↔ ( 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ∨ 𝑍 ∈ ( 𝑌 𝐼 𝑋 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ) ) )
21 19 20 bitr4d ( 𝜑 → ( 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ↔ 𝑌 ∈ ( 𝑍 𝐿 𝑋 ) ) )
22 9 21 mpbird ( 𝜑𝑍 ∈ ( 𝑋 𝐿 𝑌 ) )