Theorem lnrot1 28368

Description: Rotating the points defining a line. Part of Theorem 4.11 of [Schwabhauser] p. 34. (Contributed by Thierry Arnoux, 3-Apr-2019.)

Hypotheses

Ref	Expression
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

Ref	Expression
lnrot1	⊢ (𝜑 → 𝑍 ∈ (𝑋𝐿𝑌))

Proof of Theorem lnrot1

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

Syntax hints:   → wi 4   ↔ wb 205   ∨ w3o 1083   = wceq 1533   ∈ wcel 2098   ≠ wne 2932  ‘cfv 6534  (class class class)co 7402  Basecbs 17149  distcds 17211  TarskiGcstrkg 28172  Itvcitv 28178  LineGclng 28179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5290  ax-nul 5297  ax-pr 5418

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-sbc 3771  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-br 5140  df-opab 5202  df-id 5565  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-iota 6486  df-fun 6536  df-fv 6542  df-ov 7405  df-oprab 7406  df-mpo 7407  df-trkgc 28193  df-trkgb 28194  df-trkgcb 28195  df-trkg 28198

This theorem is referenced by:  tglineelsb2  28377  tglineneq  28389  coltr3  28393  hlperpnel  28470  opphllem4  28495  lmieu  28529