Metamath Proof Explorer

Theorem tgaltai

Description: Parallelism implies alternate angles congruence: if a line ( X L Z ) crosses two parallel lines ( X L Y ) and ( Z L W ) , then the alternate angles are congruent. First direction of Theorem 12.21 of Schwabhauser p. 126. This is also Proposition 1.29 of Euclid's Elements . (Contributed by Thierry Arnoux, 20-Jul-2026)

Ref Expression
Hypotheses tgaltai.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
tgaltai.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tgaltai.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
tgaltai.r ⊢ ∥ = ( parlnG ‘ 𝐺 )
tgaltai.o ⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑍 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
tgaltai.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tgaltai.1 ⊢ ( 𝜑 → 𝐺 ∈ TarskiGE )
tgaltai.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
tgaltai.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
tgaltai.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
tgaltai.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
tgaltai.2 ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ∥ ( 𝑍 𝐿 𝑊 ) )
tgaltai.3 ⊢ ( 𝜑 → 𝑌 𝑂 𝑊 )
tgaltai.4 ⊢ ( 𝜑 → 𝑋 ≠ 𝑍 )
Assertion tgaltai ( 𝜑 → ⟨“ 𝑌 𝑋 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑊 𝑍 𝑋 ”⟩ )

Proof

Step Hyp Ref Expression
1 tgaltai.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tgaltai.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 tgaltai.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
4 tgaltai.r ⊢ ∥ = ( parlnG ‘ 𝐺 )
5 tgaltai.o ⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑍 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
6 tgaltai.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
7 tgaltai.1 ⊢ ( 𝜑 → 𝐺 ∈ TarskiGE )
8 tgaltai.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
9 tgaltai.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
10 tgaltai.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
11 tgaltai.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
12 tgaltai.2 ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ∥ ( 𝑍 𝐿 𝑊 ) )
13 tgaltai.3 ⊢ ( 𝜑 → 𝑌 𝑂 𝑊 )
14 tgaltai.4 ⊢ ( 𝜑 → 𝑋 ≠ 𝑍 )
15 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
16 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝐺 ∈ TarskiG )
17 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝑌 ∈ 𝑃 )
18 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝑋 ∈ 𝑃 )
19 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝑍 ∈ 𝑃 )
20 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝑊 ∈ 𝑃 )
21 simplr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝑡 ∈ 𝑃 )
22 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
23 eqid ⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
24 simprr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) )
25 24 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) = ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) )
26 1 22 2 16 18 17 19 21 25 tgcgrcomlr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝑡 ( dist ‘ 𝐺 ) 𝑍 ) )
27 1 22 2 16 18 19 axtgcgrrflx ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → ( 𝑋 ( dist ‘ 𝐺 ) 𝑍 ) = ( 𝑍 ( dist ‘ 𝐺 ) 𝑋 ) )
28 eleq1w ⊢ ( 𝑡 = 𝑠 → ( 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ↔ 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) )
29 28 cbvrexvw ⊢ ( ∃ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ↔ ∃ 𝑠 ∈ ( 𝑋 𝐿 𝑍 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) )
30 29 anbi2i ⊢ ( ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑍 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) ↔ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑍 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑋 𝐿 𝑍 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) )
31 30 opabbii ⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑍 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑍 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑋 𝐿 𝑍 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) }
32 5 31 eqtri ⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑍 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑋 𝐿 𝑍 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) }
33 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝐺 ∈ TarskiGE )
34 1 2 3 6 8 10 14 tgelrnln ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑍 ) ∈ ran 𝐿 )
35 1 22 2 5 3 34 6 9 11 13 oppne1 ⊢ ( 𝜑 → ¬ 𝑌 ∈ ( 𝑋 𝐿 𝑍 ) )
36 14 neneqd ⊢ ( 𝜑 → ¬ 𝑋 = 𝑍 )
37 ioran ⊢ ( ¬ ( 𝑌 ∈ ( 𝑋 𝐿 𝑍 ) ∨ 𝑋 = 𝑍 ) ↔ ( ¬ 𝑌 ∈ ( 𝑋 𝐿 𝑍 ) ∧ ¬ 𝑋 = 𝑍 ) )
38 35 36 37 sylanbrc ⊢ ( 𝜑 → ¬ ( 𝑌 ∈ ( 𝑋 𝐿 𝑍 ) ∨ 𝑋 = 𝑍 ) )
39 1 3 2 6 8 10 9 38 ncolcom ⊢ ( 𝜑 → ¬ ( 𝑌 ∈ ( 𝑍 𝐿 𝑋 ) ∨ 𝑍 = 𝑋 ) )
40 1 3 2 6 10 8 9 39 ncolrot2 ⊢ ( 𝜑 → ¬ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) )
41 40 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → ¬ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) )
42 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → ( 𝑋 𝐿 𝑌 ) ∥ ( 𝑍 𝐿 𝑊 ) )
43 simprl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 )
44 1 2 15 21 20 19 16 43 hlne1 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝑡 ≠ 𝑍 )
45 44 necomd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝑍 ≠ 𝑡 )
46 3 4 6 12 prlngrcl2 ⊢ ( 𝜑 → ( 𝑍 𝐿 𝑊 ) ∈ ran 𝐿 )
47 46 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → ( 𝑍 𝐿 𝑊 ) ∈ ran 𝐿 )
48 1 2 3 6 10 11 46 tglnne ⊢ ( 𝜑 → 𝑍 ≠ 𝑊 )
49 1 2 3 6 10 11 48 tglinerflx1 ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑍 𝐿 𝑊 ) )
50 49 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝑍 ∈ ( 𝑍 𝐿 𝑊 ) )
51 1 2 15 21 20 19 16 3 43 hlln ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝑡 ∈ ( 𝑊 𝐿 𝑍 ) )
52 48 necomd ⊢ ( 𝜑 → 𝑊 ≠ 𝑍 )
53 1 2 3 6 11 10 52 tglinecom ⊢ ( 𝜑 → ( 𝑊 𝐿 𝑍 ) = ( 𝑍 𝐿 𝑊 ) )
54 53 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → ( 𝑊 𝐿 𝑍 ) = ( 𝑍 𝐿 𝑊 ) )
55 51 54 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝑡 ∈ ( 𝑍 𝐿 𝑊 ) )
56 1 2 3 16 19 21 45 45 47 50 55 tglinethru ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → ( 𝑍 𝐿 𝑊 ) = ( 𝑍 𝐿 𝑡 ) )
57 42 56 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → ( 𝑋 𝐿 𝑌 ) ∥ ( 𝑍 𝐿 𝑡 ) )
58 34 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → ( 𝑋 𝐿 𝑍 ) ∈ ran 𝐿 )
59 1 22 2 32 3 34 6 9 11 13 oppcom ⊢ ( 𝜑 → 𝑊 𝑂 𝑌 )
60 59 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝑊 𝑂 𝑌 )
61 1 2 3 6 8 10 14 tglinerflx2 ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑋 𝐿 𝑍 ) )
62 61 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝑍 ∈ ( 𝑋 𝐿 𝑍 ) )
63 1 2 15 21 20 19 16 43 hlcomd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝑊 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑡 )
64 1 22 2 32 3 58 16 15 20 21 17 60 62 63 opphl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝑡 𝑂 𝑌 )
65 1 22 2 32 3 58 16 21 17 64 oppcom ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝑌 𝑂 𝑡 )
66 1 22 2 3 4 32 16 33 18 17 19 21 41 57 25 65 quadcgrprlng ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → ( ( 𝑌 𝐿 𝑍 ) ∥ ( 𝑡 𝐿 𝑋 ) ∧ ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) = ( 𝑡 ( dist ‘ 𝐺 ) 𝑋 ) ) )
67 66 simprd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) = ( 𝑡 ( dist ‘ 𝐺 ) 𝑋 ) )
68 1 22 2 16 17 19 21 18 67 tgcgrcomlr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → ( 𝑍 ( dist ‘ 𝐺 ) 𝑌 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑡 ) )
69 1 22 23 16 17 18 19 21 19 18 26 27 68 trgcgr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → ⟨“ 𝑌 𝑋 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑡 𝑍 𝑋 ”⟩ )
70 1 2 15 8 8 10 6 14 hlid ⊢ ( 𝜑 → 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑋 )
71 70 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑋 )
72 1 2 15 16 17 18 19 20 19 18 21 18 69 43 71 iscgrad ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → ⟨“ 𝑌 𝑋 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑊 𝑍 𝑋 ”⟩ )
73 3 4 6 12 prlngrcl1 ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ∈ ran 𝐿 )
74 1 2 3 6 8 9 73 tglnne ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
75 1 2 15 10 8 9 6 11 22 52 74 hlcgrex ⊢ ( 𝜑 → ∃ 𝑡 ∈ 𝑃 ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 ∧ ( 𝑍 ( dist ‘ 𝐺 ) 𝑡 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) )
76 72 75 r19.29a ⊢ ( 𝜑 → ⟨“ 𝑌 𝑋 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑊 𝑍 𝑋 ”⟩ )