Metamath Proof Explorer

Theorem tgaaddcpbl

Description: The angular addition is compatible with angle congruence: by adding congruent angles together, we obtain congruent angles. Theorem 11.22 of Schwabhauser p. 99. The angles <" X Y S "> and <" S Y Z "> are added to result in <" X Y Z "> , and <" U V T "> and <" T V W "> are added to result in <" U V W "> . (Contributed by Thierry Arnoux, 2-Aug-2026)

Ref Expression
Hypotheses tgaaddcpbl.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
tgaaddcpbl.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tgaaddcpbl.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
tgaaddcpbl.c ⊢ ∼ = ( cgrA ‘ 𝐺 )
tgaaddcpbl.o ⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) }
tgaaddcpbl.q ⊢ 𝑄 = { ⟨ 𝑐 , 𝑑 ⟩ ∣ ( ( 𝑐 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ∧ 𝑑 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑉 𝐿 𝑇 ) 𝑡 ∈ ( 𝑐 𝐼 𝑑 ) ) }
tgaaddcpbl.1 ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tgaaddcpbl.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑃 )
tgaaddcpbl.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
tgaaddcpbl.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
tgaaddcpbl.v ⊢ ( 𝜑 → 𝑉 ∈ 𝑃 )
tgaaddcpbl.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
tgaaddcpbl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
tgaaddcpbl.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
tgaaddcpbl.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
tgaaddcpbl.2 ⊢ ( 𝜑 → 𝑌 ≠ 𝑆 )
tgaaddcpbl.3 ⊢ ( 𝜑 → 𝑉 ≠ 𝑇 )
tgaaddcpbl.4 ⊢ ( 𝜑 → 𝑋 𝑂 𝑍 )
tgaaddcpbl.5 ⊢ ( 𝜑 → 𝑈 𝑄 𝑊 )
tgaaddcpbl.6 ⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑆 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑇 ”⟩ )
tgaaddcpbl.7 ⊢ ( 𝜑 → ⟨“ 𝑆 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝑇 𝑉 𝑊 ”⟩ )
Assertion tgaaddcpbl ( 𝜑 → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ )

Proof

Step Hyp Ref Expression
1 tgaaddcpbl.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tgaaddcpbl.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 tgaaddcpbl.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
4 tgaaddcpbl.c ⊢ ∼ = ( cgrA ‘ 𝐺 )
5 tgaaddcpbl.o ⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) }
6 tgaaddcpbl.q ⊢ 𝑄 = { ⟨ 𝑐 , 𝑑 ⟩ ∣ ( ( 𝑐 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ∧ 𝑑 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑉 𝐿 𝑇 ) 𝑡 ∈ ( 𝑐 𝐼 𝑑 ) ) }
7 tgaaddcpbl.1 ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
8 tgaaddcpbl.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑃 )
9 tgaaddcpbl.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
10 tgaaddcpbl.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
11 tgaaddcpbl.v ⊢ ( 𝜑 → 𝑉 ∈ 𝑃 )
12 tgaaddcpbl.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
13 tgaaddcpbl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
14 tgaaddcpbl.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
15 tgaaddcpbl.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
16 tgaaddcpbl.2 ⊢ ( 𝜑 → 𝑌 ≠ 𝑆 )
17 tgaaddcpbl.3 ⊢ ( 𝜑 → 𝑉 ≠ 𝑇 )
18 tgaaddcpbl.4 ⊢ ( 𝜑 → 𝑋 𝑂 𝑍 )
19 tgaaddcpbl.5 ⊢ ( 𝜑 → 𝑈 𝑄 𝑊 )
20 tgaaddcpbl.6 ⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑆 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑇 ”⟩ )
21 tgaaddcpbl.7 ⊢ ( 𝜑 → ⟨“ 𝑆 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝑇 𝑉 𝑊 ”⟩ )
22 4 a1i ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ∼ = ( cgrA ‘ 𝐺 ) )
23 22 eqcomd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ( cgrA ‘ 𝐺 ) = ∼ )
24 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
25 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) → 𝐺 ∈ TarskiG )
26 25 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝐺 ∈ TarskiG )
27 13 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑋 ∈ 𝑃 )
28 14 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) → 𝑌 ∈ 𝑃 )
29 28 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑌 ∈ 𝑃 )
30 15 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) → 𝑍 ∈ 𝑃 )
31 30 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑍 ∈ 𝑃 )
32 10 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑈 ∈ 𝑃 )
33 11 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) → 𝑉 ∈ 𝑃 )
34 33 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑉 ∈ 𝑃 )
35 simpllr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑤 ∈ 𝑃 )
36 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
37 simp-7r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) )
38 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) → 𝑢 ∈ 𝑃 )
39 38 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑢 ∈ 𝑃 )
40 simp-5r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 )
41 simplr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) )
42 1 2 24 39 32 35 26 34 40 41 btwnhl ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑉 ∈ ( 𝑈 𝐼 𝑤 ) )
43 1 2 3 7 14 8 16 tglinerflx1 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑌 𝐿 𝑆 ) )
44 1 2 3 7 14 8 16 tgelrnln ⊢ ( 𝜑 → ( 𝑌 𝐿 𝑆 ) ∈ ran 𝐿 )
45 1 36 2 5 3 44 7 13 15 18 oppne1 ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) )
46 nelne2 ⊢ ( ( 𝑌 ∈ ( 𝑌 𝐿 𝑆 ) ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝑌 ≠ 𝑋 )
47 43 45 46 syl2anc ⊢ ( 𝜑 → 𝑌 ≠ 𝑋 )
48 47 necomd ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
49 48 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑋 ≠ 𝑌 )
50 1 36 2 5 3 44 7 13 15 18 oppne2 ⊢ ( 𝜑 → ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) )
51 nelne2 ⊢ ( ( 𝑌 ∈ ( 𝑌 𝐿 𝑆 ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝑌 ≠ 𝑍 )
52 43 50 51 syl2anc ⊢ ( 𝜑 → 𝑌 ≠ 𝑍 )
53 52 necomd ⊢ ( 𝜑 → 𝑍 ≠ 𝑌 )
54 53 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑍 ≠ 𝑌 )
55 1 2 3 7 11 9 17 tglinerflx1 ⊢ ( 𝜑 → 𝑉 ∈ ( 𝑉 𝐿 𝑇 ) )
56 1 36 2 6 10 12 islnopp ⊢ ( 𝜑 → ( 𝑈 𝑄 𝑊 ↔ ( ( ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑇 ) ∧ ¬ 𝑊 ∈ ( 𝑉 𝐿 𝑇 ) ) ∧ ∃ 𝑡 ∈ ( 𝑉 𝐿 𝑇 ) 𝑡 ∈ ( 𝑈 𝐼 𝑊 ) ) ) )
57 19 56 mpbid ⊢ ( 𝜑 → ( ( ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑇 ) ∧ ¬ 𝑊 ∈ ( 𝑉 𝐿 𝑇 ) ) ∧ ∃ 𝑡 ∈ ( 𝑉 𝐿 𝑇 ) 𝑡 ∈ ( 𝑈 𝐼 𝑊 ) ) )
58 57 simplld ⊢ ( 𝜑 → ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑇 ) )
59 nelne2 ⊢ ( ( 𝑉 ∈ ( 𝑉 𝐿 𝑇 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑉 ≠ 𝑈 )
60 55 58 59 syl2anc ⊢ ( 𝜑 → 𝑉 ≠ 𝑈 )
61 60 necomd ⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
62 61 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑈 ≠ 𝑉 )
63 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) )
64 63 eqcomd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) = ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) )
65 52 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑌 ≠ 𝑍 )
66 1 36 2 26 29 31 34 35 64 65 tgcgrneq ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑉 ≠ 𝑤 )
67 66 necomd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑤 ≠ 𝑉 )
68 1 2 36 26 27 29 31 32 34 35 37 42 49 54 62 67 flatcgra ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑈 𝑉 𝑤 ”⟩ )
69 12 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑊 ∈ 𝑃 )
70 8 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑆 ∈ 𝑃 )
71 9 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑇 ∈ 𝑃 )
72 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
73 eqid ⊢ ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 )
74 1 36 2 3 72 7 9 73 10 mircl ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ∈ 𝑃 )
75 74 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ∈ 𝑃 )
76 7 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ∈ ( 𝑌 𝐿 𝑍 ) ) → 𝐺 ∈ TarskiG )
77 14 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ∈ ( 𝑌 𝐿 𝑍 ) ) → 𝑌 ∈ 𝑃 )
78 8 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ∈ ( 𝑌 𝐿 𝑍 ) ) → 𝑆 ∈ 𝑃 )
79 15 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ∈ ( 𝑌 𝐿 𝑍 ) ) → 𝑍 ∈ 𝑃 )
80 16 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ∈ ( 𝑌 𝐿 𝑍 ) ) → 𝑌 ≠ 𝑆 )
81 simpr ⊢ ( ( 𝜑 ∧ 𝑆 ∈ ( 𝑌 𝐿 𝑍 ) ) → 𝑆 ∈ ( 𝑌 𝐿 𝑍 ) )
82 52 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ∈ ( 𝑌 𝐿 𝑍 ) ) → 𝑌 ≠ 𝑍 )
83 1 2 3 76 77 79 82 tglinecom ⊢ ( ( 𝜑 ∧ 𝑆 ∈ ( 𝑌 𝐿 𝑍 ) ) → ( 𝑌 𝐿 𝑍 ) = ( 𝑍 𝐿 𝑌 ) )
84 81 83 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑆 ∈ ( 𝑌 𝐿 𝑍 ) ) → 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) )
85 53 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ∈ ( 𝑌 𝐿 𝑍 ) ) → 𝑍 ≠ 𝑌 )
86 1 2 3 76 77 78 79 80 84 85 lnrot1 ⊢ ( ( 𝜑 ∧ 𝑆 ∈ ( 𝑌 𝐿 𝑍 ) ) → 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) )
87 50 86 mtand ⊢ ( 𝜑 → ¬ 𝑆 ∈ ( 𝑌 𝐿 𝑍 ) )
88 52 neneqd ⊢ ( 𝜑 → ¬ 𝑌 = 𝑍 )
89 ioran ⊢ ( ¬ ( 𝑆 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) ↔ ( ¬ 𝑆 ∈ ( 𝑌 𝐿 𝑍 ) ∧ ¬ 𝑌 = 𝑍 ) )
90 87 88 89 sylanbrc ⊢ ( 𝜑 → ¬ ( 𝑆 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) )
91 90 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ¬ ( 𝑆 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) )
92 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑇 ∈ ( 𝑉 𝐿 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ∨ 𝑉 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ) → 𝐺 ∈ TarskiG )
93 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑇 ∈ ( 𝑉 𝐿 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ∨ 𝑉 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ) → 𝑇 ∈ 𝑃 )
94 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑇 ∈ ( 𝑉 𝐿 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ∨ 𝑉 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ) → 𝑈 ∈ 𝑃 )
95 1 36 2 3 72 92 93 73 94 mirmir ⊢ ( ( 𝜑 ∧ ( 𝑇 ∈ ( 𝑉 𝐿 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ∨ 𝑉 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) = 𝑈 )
96 1 2 3 7 11 9 17 tgelrnln ⊢ ( 𝜑 → ( 𝑉 𝐿 𝑇 ) ∈ ran 𝐿 )
97 96 adantr ⊢ ( ( 𝜑 ∧ ( 𝑇 ∈ ( 𝑉 𝐿 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ∨ 𝑉 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ) → ( 𝑉 𝐿 𝑇 ) ∈ ran 𝐿 )
98 1 2 3 7 11 9 17 tglinerflx2 ⊢ ( 𝜑 → 𝑇 ∈ ( 𝑉 𝐿 𝑇 ) )
99 98 adantr ⊢ ( ( 𝜑 ∧ ( 𝑇 ∈ ( 𝑉 𝐿 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ∨ 𝑉 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ) → 𝑇 ∈ ( 𝑉 𝐿 𝑇 ) )
100 74 adantr ⊢ ( ( 𝜑 ∧ ( 𝑇 ∈ ( 𝑉 𝐿 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ∨ 𝑉 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ∈ 𝑃 )
101 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝑇 ∈ ( 𝑉 𝐿 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ∨ 𝑉 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ) → 𝑉 ∈ 𝑃 )
102 simpr ⊢ ( ( 𝜑 ∧ ( 𝑇 ∈ ( 𝑉 𝐿 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ∨ 𝑉 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ) → ( 𝑇 ∈ ( 𝑉 𝐿 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ∨ 𝑉 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) )
103 1 3 2 92 101 100 93 102 colcom ⊢ ( ( 𝜑 ∧ ( 𝑇 ∈ ( 𝑉 𝐿 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ∨ 𝑉 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ) → ( 𝑇 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) 𝐿 𝑉 ) ∨ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) = 𝑉 ) )
104 1 3 2 92 100 101 93 103 colrot1 ⊢ ( ( 𝜑 ∧ ( 𝑇 ∈ ( 𝑉 𝐿 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ∨ 𝑉 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ) → ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ∈ ( 𝑉 𝐿 𝑇 ) ∨ 𝑉 = 𝑇 ) )
105 17 neneqd ⊢ ( 𝜑 → ¬ 𝑉 = 𝑇 )
106 105 adantr ⊢ ( ( 𝜑 ∧ ( 𝑇 ∈ ( 𝑉 𝐿 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ∨ 𝑉 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ) → ¬ 𝑉 = 𝑇 )
107 104 106 olcnd ⊢ ( ( 𝜑 ∧ ( 𝑇 ∈ ( 𝑉 𝐿 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ∨ 𝑉 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ∈ ( 𝑉 𝐿 𝑇 ) )
108 1 36 2 3 72 92 73 97 99 107 mirln ⊢ ( ( 𝜑 ∧ ( 𝑇 ∈ ( 𝑉 𝐿 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ∨ 𝑉 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ∈ ( 𝑉 𝐿 𝑇 ) )
109 95 108 eqeltrrd ⊢ ( ( 𝜑 ∧ ( 𝑇 ∈ ( 𝑉 𝐿 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ∨ 𝑉 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ) → 𝑈 ∈ ( 𝑉 𝐿 𝑇 ) )
110 58 109 mtand ⊢ ( 𝜑 → ¬ ( 𝑇 ∈ ( 𝑉 𝐿 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ∨ 𝑉 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) )
111 110 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ¬ ( 𝑇 ∈ ( 𝑉 𝐿 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) ∨ 𝑉 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) )
112 4 a1i ⊢ ( 𝜑 → ∼ = ( cgrA ‘ 𝐺 ) )
113 112 21 breqdi ⊢ ( 𝜑 → ⟨“ 𝑆 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑇 𝑉 𝑊 ”⟩ )
114 113 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ⟨“ 𝑆 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑇 𝑉 𝑊 ”⟩ )
115 112 20 breqdi ⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑆 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑈 𝑉 𝑇 ”⟩ )
116 1 2 7 24 13 14 8 10 11 9 115 cgracom ⊢ ( 𝜑 → ⟨“ 𝑈 𝑉 𝑇 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑆 ”⟩ )
117 116 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ⟨“ 𝑈 𝑉 𝑇 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑆 ”⟩ )
118 1 2 36 26 32 34 71 27 29 70 35 31 117 42 37 66 65 sacgr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ⟨“ 𝑤 𝑉 𝑇 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑆 ”⟩ )
119 1 2 36 26 35 34 71 31 29 70 118 cgraswaplr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ⟨“ 𝑇 𝑉 𝑤 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑍 ”⟩ )
120 1 2 26 24 71 34 35 70 29 31 119 cgracom ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ⟨“ 𝑆 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑇 𝑉 𝑤 ”⟩ )
121 1 2 3 7 11 9 17 tglinecom ⊢ ( 𝜑 → ( 𝑉 𝐿 𝑇 ) = ( 𝑇 𝐿 𝑉 ) )
122 121 fveq2d ⊢ ( 𝜑 → ( ( hpG ‘ 𝐺 ) ‘ ( 𝑉 𝐿 𝑇 ) ) = ( ( hpG ‘ 𝐺 ) ‘ ( 𝑇 𝐿 𝑉 ) ) )
123 10 58 eldifd ⊢ ( 𝜑 → 𝑈 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) )
124 1 2 72 73 6 7 96 98 123 3 oppmir ⊢ ( 𝜑 → 𝑈 𝑄 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) )
125 1 36 2 6 3 96 7 10 74 124 oppcom ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) 𝑄 𝑈 )
126 1 36 2 6 3 96 7 10 12 19 oppcom ⊢ ( 𝜑 → 𝑊 𝑄 𝑈 )
127 1 2 3 6 7 96 12 74 10 126 lnopp2hpgb ⊢ ( 𝜑 → ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) 𝑄 𝑈 ↔ 𝑊 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑉 𝐿 𝑇 ) ) ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) )
128 125 127 mpbid ⊢ ( 𝜑 → 𝑊 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑉 𝐿 𝑇 ) ) ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) )
129 122 128 breqdi ⊢ ( 𝜑 → 𝑊 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑇 𝐿 𝑉 ) ) ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) )
130 129 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑊 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑇 𝐿 𝑉 ) ) ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) )
131 122 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ( ( hpG ‘ 𝐺 ) ‘ ( 𝑉 𝐿 𝑇 ) ) = ( ( hpG ‘ 𝐺 ) ‘ ( 𝑇 𝐿 𝑉 ) ) )
132 125 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) 𝑄 𝑈 )
133 96 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ( 𝑉 𝐿 𝑇 ) ∈ ran 𝐿 )
134 55 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑉 ∈ ( 𝑉 𝐿 𝑇 ) )
135 25 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑢 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝐺 ∈ TarskiG )
136 33 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑢 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑉 ∈ 𝑃 )
137 9 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑢 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑇 ∈ 𝑃 )
138 10 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑢 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑈 ∈ 𝑃 )
139 17 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑢 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑉 ≠ 𝑇 )
140 38 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑢 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑢 ∈ 𝑃 )
141 13 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) → 𝑋 ∈ 𝑃 )
142 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) → ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) )
143 142 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) → ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) )
144 47 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) → 𝑌 ≠ 𝑋 )
145 1 36 2 25 28 141 33 38 143 144 tgcgrneq ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) → 𝑉 ≠ 𝑢 )
146 145 necomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) → 𝑢 ≠ 𝑉 )
147 146 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑢 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑢 ≠ 𝑉 )
148 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑢 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑢 ∈ ( 𝑉 𝐿 𝑇 ) )
149 1 2 3 135 140 136 137 147 148 139 lnrot2 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑢 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑇 ∈ ( 𝑢 𝐿 𝑉 ) )
150 61 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑢 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑈 ≠ 𝑉 )
151 1 2 3 135 140 136 147 tgelrnln ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑢 ∈ ( 𝑉 𝐿 𝑇 ) ) → ( 𝑢 𝐿 𝑉 ) ∈ ran 𝐿 )
152 10 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) → 𝑈 ∈ 𝑃 )
153 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) → 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 )
154 1 2 24 38 152 33 25 153 hlcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) → 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑢 )
155 1 2 24 152 38 33 25 3 154 hlln ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) → 𝑈 ∈ ( 𝑢 𝐿 𝑉 ) )
156 155 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑢 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑈 ∈ ( 𝑢 𝐿 𝑉 ) )
157 1 2 3 135 140 136 147 tglinerflx2 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑢 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑉 ∈ ( 𝑢 𝐿 𝑉 ) )
158 1 2 3 135 138 136 150 150 151 156 157 tglinethru ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑢 ∈ ( 𝑉 𝐿 𝑇 ) ) → ( 𝑢 𝐿 𝑉 ) = ( 𝑈 𝐿 𝑉 ) )
159 149 158 eleqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑢 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑇 ∈ ( 𝑈 𝐿 𝑉 ) )
160 1 2 3 135 136 137 138 139 159 150 lnrot1 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑢 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑈 ∈ ( 𝑉 𝐿 𝑇 ) )
161 58 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑢 ∈ ( 𝑉 𝐿 𝑇 ) ) → ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑇 ) )
162 160 161 pm2.65da ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) → ¬ 𝑢 ∈ ( 𝑉 𝐿 𝑇 ) )
163 162 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ¬ 𝑢 ∈ ( 𝑉 𝐿 𝑇 ) )
164 66 neneqd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ¬ 𝑉 = 𝑤 )
165 26 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) ∧ 𝑤 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝐺 ∈ TarskiG )
166 39 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) ∧ 𝑤 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑢 ∈ 𝑃 )
167 35 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) ∧ 𝑤 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑤 ∈ 𝑃 )
168 26 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) ∧ 𝑢 = 𝑤 ) → 𝐺 ∈ TarskiG )
169 35 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) ∧ 𝑢 = 𝑤 ) → 𝑤 ∈ 𝑃 )
170 34 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) ∧ 𝑢 = 𝑤 ) → 𝑉 ∈ 𝑃 )
171 simpllr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) ∧ 𝑢 = 𝑤 ) → 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) )
172 simpr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) ∧ 𝑢 = 𝑤 ) → 𝑢 = 𝑤 )
173 172 oveq1d ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) ∧ 𝑢 = 𝑤 ) → ( 𝑢 𝐼 𝑤 ) = ( 𝑤 𝐼 𝑤 ) )
174 171 173 eleqtrd ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) ∧ 𝑢 = 𝑤 ) → 𝑉 ∈ ( 𝑤 𝐼 𝑤 ) )
175 1 36 2 168 169 170 174 axtgbtwnid ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) ∧ 𝑢 = 𝑤 ) → 𝑤 = 𝑉 )
176 175 eqcomd ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) ∧ 𝑢 = 𝑤 ) → 𝑉 = 𝑤 )
177 66 176 mteqand ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑢 ≠ 𝑤 )
178 177 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) ∧ 𝑤 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑢 ≠ 𝑤 )
179 1 2 3 165 166 167 178 tgelrnln ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) ∧ 𝑤 ∈ ( 𝑉 𝐿 𝑇 ) ) → ( 𝑢 𝐿 𝑤 ) ∈ ran 𝐿 )
180 133 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) ∧ 𝑤 ∈ ( 𝑉 𝐿 𝑇 ) ) → ( 𝑉 𝐿 𝑇 ) ∈ ran 𝐿 )
181 1 2 3 165 166 167 178 tglinerflx1 ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) ∧ 𝑤 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑢 ∈ ( 𝑢 𝐿 𝑤 ) )
182 163 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) ∧ 𝑤 ∈ ( 𝑉 𝐿 𝑇 ) ) → ¬ 𝑢 ∈ ( 𝑉 𝐿 𝑇 ) )
183 nelne1 ⊢ ( ( 𝑢 ∈ ( 𝑢 𝐿 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑉 𝐿 𝑇 ) ) → ( 𝑢 𝐿 𝑤 ) ≠ ( 𝑉 𝐿 𝑇 ) )
184 181 182 183 syl2anc ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) ∧ 𝑤 ∈ ( 𝑉 𝐿 𝑇 ) ) → ( 𝑢 𝐿 𝑤 ) ≠ ( 𝑉 𝐿 𝑇 ) )
185 34 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) ∧ 𝑤 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑉 ∈ 𝑃 )
186 simpllr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) ∧ 𝑤 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) )
187 1 2 3 165 166 167 185 178 186 btwnlng1 ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) ∧ 𝑤 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑉 ∈ ( 𝑢 𝐿 𝑤 ) )
188 134 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) ∧ 𝑤 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑉 ∈ ( 𝑉 𝐿 𝑇 ) )
189 187 188 elind ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) ∧ 𝑤 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑉 ∈ ( ( 𝑢 𝐿 𝑤 ) ∩ ( 𝑉 𝐿 𝑇 ) ) )
190 1 2 3 165 166 167 178 tglinerflx2 ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) ∧ 𝑤 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑤 ∈ ( 𝑢 𝐿 𝑤 ) )
191 simpr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) ∧ 𝑤 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑤 ∈ ( 𝑉 𝐿 𝑇 ) )
192 190 191 elind ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) ∧ 𝑤 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑤 ∈ ( ( 𝑢 𝐿 𝑤 ) ∩ ( 𝑉 𝐿 𝑇 ) ) )
193 1 2 3 165 179 180 184 189 192 tglineineq ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) ∧ 𝑤 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑉 = 𝑤 )
194 164 193 mtand ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ¬ 𝑤 ∈ ( 𝑉 𝐿 𝑇 ) )
195 1 36 2 6 39 35 134 163 194 41 islnoppd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑢 𝑄 𝑤 )
196 1 36 2 6 3 133 26 24 39 32 35 195 134 40 opphl ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑈 𝑄 𝑤 )
197 1 36 2 6 3 133 26 32 35 196 oppcom ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑤 𝑄 𝑈 )
198 1 2 3 6 26 133 35 75 32 197 lnopp2hpgb ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) 𝑄 𝑈 ↔ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑉 𝐿 𝑇 ) ) ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) ) )
199 132 198 mpbid ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑉 𝐿 𝑇 ) ) ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) )
200 131 199 breqdi ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑇 𝐿 𝑉 ) ) ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑈 ) )
201 1 2 36 26 70 29 31 71 34 75 3 91 111 69 35 24 114 120 130 200 acopyeu ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑊 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑤 )
202 1 2 24 26 27 29 31 32 34 35 68 69 201 cgrahl2 ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
203 23 202 breqdi ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
204 203 anasss ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
205 1 36 2 25 38 33 28 30 axtgsegcon ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) → ∃ 𝑤 ∈ 𝑃 ( 𝑉 ∈ ( 𝑢 𝐼 𝑤 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑤 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) )
206 204 205 r19.29a ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ) ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
207 206 anasss ⊢ ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ ( 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
208 1 2 24 11 14 13 7 10 36 61 47 hlcgrex ⊢ ( 𝜑 → ∃ 𝑢 ∈ 𝑃 ( 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) )
209 208 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → ∃ 𝑢 ∈ 𝑃 ( 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 ∧ ( 𝑉 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) )
210 207 209 r19.29a ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
211 7 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝐺 ∈ TarskiG )
212 8 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑆 ∈ 𝑃 )
213 9 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑇 ∈ 𝑃 )
214 10 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑈 ∈ 𝑃 )
215 11 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑉 ∈ 𝑃 )
216 12 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑊 ∈ 𝑃 )
217 13 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑋 ∈ 𝑃 )
218 14 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑌 ∈ 𝑃 )
219 15 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑍 ∈ 𝑃 )
220 16 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑌 ≠ 𝑆 )
221 17 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑉 ≠ 𝑇 )
222 18 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑋 𝑂 𝑍 )
223 19 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑈 𝑄 𝑊 )
224 20 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → ⟨“ 𝑋 𝑌 𝑆 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑇 ”⟩ )
225 21 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → ⟨“ 𝑆 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝑇 𝑉 𝑊 ”⟩ )
226 simpr ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → ¬ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) )
227 1 2 3 4 5 6 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 tgaaddcpbllem3 ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
228 210 227 pm2.61dan ⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ )