Metamath Proof Explorer

Theorem angmndaddov2lem

Description: Lemma for angmndaddov2 . (Contributed by Thierry Arnoux, 23-Aug-2026)

Ref Expression
Hypotheses angmndadd.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
angmndadd.a ⊢ 𝐴 = { 𝑑 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) }
angmndadd.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
angmndadd.d ⊢ − = ( dist ‘ 𝐺 )
angmndadd.c ⊢ ∼ = ( cgrA ‘ 𝐺 )
angmndadd.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
angmndadd.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
angmndaddov.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
angmndaddov.v ⊢ ( 𝜑 → 𝑉 ∈ 𝑃 )
angmndaddov.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
angmndaddov.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
angmndaddov.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
angmndaddov.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
angmndaddeu.1 ⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
angmndaddeu.2 ⊢ ( 𝜑 → 𝑉 ≠ 𝑊 )
angmndaddeu.3 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
angmndaddeu.4 ⊢ ( 𝜑 → 𝑌 ≠ 𝑍 )
angmndaddov2lem.1 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) )
Assertion angmndaddov2lem ( 𝜑 → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 angmndadd.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 angmndadd.a ⊢ 𝐴 = { 𝑑 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) }
3 angmndadd.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 angmndadd.d ⊢ − = ( dist ‘ 𝐺 )
5 angmndadd.c ⊢ ∼ = ( cgrA ‘ 𝐺 )
6 angmndadd.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
7 angmndadd.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
8 angmndaddov.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
9 angmndaddov.v ⊢ ( 𝜑 → 𝑉 ∈ 𝑃 )
10 angmndaddov.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
11 angmndaddov.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
12 angmndaddov.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
13 angmndaddov.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
14 angmndaddeu.1 ⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
15 angmndaddeu.2 ⊢ ( 𝜑 → 𝑉 ≠ 𝑊 )
16 angmndaddeu.3 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
17 angmndaddeu.4 ⊢ ( 𝜑 → 𝑌 ≠ 𝑍 )
18 angmndaddov2lem.1 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) )
19 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝐺 ∈ TarskiG )
20 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑋 ∈ 𝑃 )
21 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑌 ∈ 𝑃 )
22 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑍 ∈ 𝑃 )
23 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑈 ∈ 𝑃 )
24 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑉 ∈ 𝑃 )
25 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑊 ∈ 𝑃 )
26 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑋 ≠ 𝑌 )
27 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑌 ≠ 𝑍 )
28 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑈 ≠ 𝑉 )
29 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑉 ≠ 𝑊 )
30 simpr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 )
31 simplr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 )
32 1 2 3 4 5 6 19 20 21 22 23 24 25 26 27 28 29 30 31 angmndaddeu4 ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) )
33 32 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) )
34 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝐺 ∈ TarskiG )
35 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑋 ∈ 𝑃 )
36 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑌 ∈ 𝑃 )
37 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑍 ∈ 𝑃 )
38 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑈 ∈ 𝑃 )
39 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑉 ∈ 𝑃 )
40 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑊 ∈ 𝑃 )
41 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑋 ≠ 𝑌 )
42 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑌 ≠ 𝑍 )
43 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑈 ≠ 𝑉 )
44 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑉 ≠ 𝑊 )
45 simpr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) )
46 1 4 3 34 40 39 38 45 tgbtwncom ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑉 ∈ ( 𝑈 𝐼 𝑊 ) )
47 simplr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 )
48 1 2 3 4 5 6 34 35 36 37 38 39 40 41 42 43 44 46 47 angmndaddeu6 ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) )
49 48 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) )
50 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
51 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑊 ∈ 𝑃 )
52 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑉 ∈ 𝑃 )
53 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑈 ∈ 𝑃 )
54 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝐺 ∈ TarskiG )
55 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑋 ∈ 𝑃 )
56 15 necomd ⊢ ( 𝜑 → 𝑊 ≠ 𝑉 )
57 56 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑊 ≠ 𝑉 )
58 simpr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) )
59 1 3 6 54 51 52 53 57 58 lncom ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑈 ∈ ( 𝑊 𝐿 𝑉 ) )
60 1 3 50 51 52 53 54 55 6 59 lnhl ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → ( 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ∨ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) )
61 33 49 60 mpjaodan ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) )
62 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝐺 ∈ TarskiG )
63 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑋 ∈ 𝑃 )
64 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑌 ∈ 𝑃 )
65 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑍 ∈ 𝑃 )
66 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑈 ∈ 𝑃 )
67 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑉 ∈ 𝑃 )
68 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑊 ∈ 𝑃 )
69 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑋 ≠ 𝑌 )
70 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑌 ≠ 𝑍 )
71 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑈 ≠ 𝑉 )
72 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑉 ≠ 𝑊 )
73 simpr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) )
74 simplr ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 )
75 1 2 3 4 5 6 62 63 64 65 66 67 68 69 70 71 72 73 74 angmndaddeu2 ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ∧ ( ( 𝑉 𝐿 𝑊 ) ∩ ( 𝑠 𝐼 𝑈 ) ) ≠ ∅ ) )
76 simpllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) ∧ ( ( 𝑉 𝐿 𝑊 ) ∩ ( 𝑠 𝐼 𝑈 ) ) ≠ ∅ ) → ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
77 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) ∧ ( ( 𝑉 𝐿 𝑊 ) ∩ ( 𝑠 𝐼 𝑈 ) ) ≠ ∅ ) → ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) )
78 76 77 jca ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) ∧ ( ( 𝑉 𝐿 𝑊 ) ∩ ( 𝑠 𝐼 𝑈 ) ) ≠ ∅ ) → ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) )
79 78 3anasss ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ∧ ( ( 𝑉 𝐿 𝑊 ) ∩ ( 𝑠 𝐼 𝑈 ) ) ≠ ∅ ) ) → ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) )
80 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
81 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) )
82 62 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝐺 ∈ TarskiG )
83 67 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝑉 ∈ 𝑃 )
84 68 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝑊 ∈ 𝑃 )
85 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝑠 ∈ 𝑃 )
86 72 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝑉 ≠ 𝑊 )
87 63 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝑋 ∈ 𝑃 )
88 64 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝑌 ∈ 𝑃 )
89 65 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝑍 ∈ 𝑃 )
90 5 a1i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → ∼ = ( cgrA ‘ 𝐺 ) )
91 90 80 breqdi ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → ⟨“ 𝑊 𝑉 𝑠 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
92 1 3 82 50 84 83 85 87 88 89 91 cgracom ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑊 𝑉 𝑠 ”⟩ )
93 74 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 )
94 1 3 4 82 87 88 89 84 83 85 92 50 93 cgrahl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝑊 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑠 )
95 1 3 50 84 85 83 82 6 94 hlln ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝑊 ∈ ( 𝑠 𝐿 𝑉 ) )
96 81 eqcomd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → ( 𝑌 − 𝑋 ) = ( 𝑉 − 𝑠 ) )
97 16 necomd ⊢ ( 𝜑 → 𝑌 ≠ 𝑋 )
98 97 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝑌 ≠ 𝑋 )
99 1 4 3 82 88 87 83 85 96 98 tgcgrneq ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝑉 ≠ 𝑠 )
100 99 necomd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝑠 ≠ 𝑉 )
101 1 3 6 82 83 84 85 86 95 100 lnrot1 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝑠 ∈ ( 𝑉 𝐿 𝑊 ) )
102 66 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝑈 ∈ 𝑃 )
103 1 4 3 82 85 102 tgbtwntriv1 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝑠 ∈ ( 𝑠 𝐼 𝑈 ) )
104 101 103 elind ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝑠 ∈ ( ( 𝑉 𝐿 𝑊 ) ∩ ( 𝑠 𝐼 𝑈 ) ) )
105 104 ne0d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → ( ( 𝑉 𝐿 𝑊 ) ∩ ( 𝑠 𝐼 𝑈 ) ) ≠ ∅ )
106 80 81 105 3jca ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ∧ ( ( 𝑉 𝐿 𝑊 ) ∩ ( 𝑠 𝐼 𝑈 ) ) ≠ ∅ ) )
107 106 anasss ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) ) → ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ∧ ( ( 𝑉 𝐿 𝑊 ) ∩ ( 𝑠 𝐼 𝑈 ) ) ≠ ∅ ) )
108 79 107 impbida ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) → ( ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ∧ ( ( 𝑉 𝐿 𝑊 ) ∩ ( 𝑠 𝐼 𝑈 ) ) ≠ ∅ ) ↔ ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) ) )
109 108 reubidva ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → ( ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ∧ ( ( 𝑉 𝐿 𝑊 ) ∩ ( 𝑠 𝐼 𝑈 ) ) ≠ ∅ ) ↔ ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) ) )
110 75 109 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) )
111 exmidd ⊢ ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) → ( 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ∨ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) )
112 61 110 111 mpjaodan ⊢ ( ( 𝜑 ∧ 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) )
113 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝐺 ∈ TarskiG )
114 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑋 ∈ 𝑃 )
115 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑌 ∈ 𝑃 )
116 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑍 ∈ 𝑃 )
117 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑈 ∈ 𝑃 )
118 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑉 ∈ 𝑃 )
119 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑊 ∈ 𝑃 )
120 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑋 ≠ 𝑌 )
121 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑌 ≠ 𝑍 )
122 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑈 ≠ 𝑉 )
123 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑉 ≠ 𝑊 )
124 simpr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 )
125 simplr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) )
126 1 4 3 113 116 115 114 125 tgbtwncom ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) )
127 1 2 3 4 5 6 113 114 115 116 117 118 119 120 121 122 123 124 126 angmndaddeu5 ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) )
128 127 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) )
129 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝐺 ∈ TarskiG )
130 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑋 ∈ 𝑃 )
131 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑌 ∈ 𝑃 )
132 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑍 ∈ 𝑃 )
133 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑈 ∈ 𝑃 )
134 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑉 ∈ 𝑃 )
135 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑊 ∈ 𝑃 )
136 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑋 ≠ 𝑌 )
137 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑌 ≠ 𝑍 )
138 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑈 ≠ 𝑉 )
139 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑉 ≠ 𝑊 )
140 simpr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) )
141 1 4 3 129 135 134 133 140 tgbtwncom ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑉 ∈ ( 𝑈 𝐼 𝑊 ) )
142 simplr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) )
143 1 4 3 129 132 131 130 142 tgbtwncom ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) )
144 1 2 3 4 5 6 129 130 131 132 133 134 135 136 137 138 139 141 143 angmndaddeu7 ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) )
145 144 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) )
146 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑊 ∈ 𝑃 )
147 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑉 ∈ 𝑃 )
148 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑈 ∈ 𝑃 )
149 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝐺 ∈ TarskiG )
150 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑋 ∈ 𝑃 )
151 56 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑊 ≠ 𝑉 )
152 simpr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) )
153 1 3 6 149 146 147 148 151 152 lncom ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑈 ∈ ( 𝑊 𝐿 𝑉 ) )
154 1 3 50 146 147 148 149 150 6 153 lnhl ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → ( 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ∨ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) )
155 128 145 154 mpjaodan ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) )
156 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝐺 ∈ TarskiG )
157 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑋 ∈ 𝑃 )
158 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑌 ∈ 𝑃 )
159 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑍 ∈ 𝑃 )
160 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑈 ∈ 𝑃 )
161 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑉 ∈ 𝑃 )
162 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑊 ∈ 𝑃 )
163 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑋 ≠ 𝑌 )
164 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑌 ≠ 𝑍 )
165 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑈 ≠ 𝑉 )
166 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑉 ≠ 𝑊 )
167 simpr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) )
168 simplr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) )
169 1 4 3 156 159 158 157 168 tgbtwncom ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) )
170 1 2 3 4 5 6 156 157 158 159 160 161 162 163 164 165 166 167 169 angmndaddeu3 ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ∧ ( ( 𝑉 𝐿 𝑊 ) ∩ ( 𝑠 𝐼 𝑈 ) ) ≠ ∅ ) )
171 simpllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) ∧ ( ( 𝑉 𝐿 𝑊 ) ∩ ( 𝑠 𝐼 𝑈 ) ) ≠ ∅ ) → ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
172 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) ∧ ( ( 𝑉 𝐿 𝑊 ) ∩ ( 𝑠 𝐼 𝑈 ) ) ≠ ∅ ) → ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) )
173 171 172 jca ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) ∧ ( ( 𝑉 𝐿 𝑊 ) ∩ ( 𝑠 𝐼 𝑈 ) ) ≠ ∅ ) → ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) )
174 173 3anasss ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ∧ ( ( 𝑉 𝐿 𝑊 ) ∩ ( 𝑠 𝐼 𝑈 ) ) ≠ ∅ ) ) → ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) )
175 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
176 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) )
177 156 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝐺 ∈ TarskiG )
178 161 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝑉 ∈ 𝑃 )
179 162 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝑊 ∈ 𝑃 )
180 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝑠 ∈ 𝑃 )
181 166 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝑉 ≠ 𝑊 )
182 56 neneqd ⊢ ( 𝜑 → ¬ 𝑊 = 𝑉 )
183 182 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → ¬ 𝑊 = 𝑉 )
184 177 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) ∧ 𝑊 = 𝑠 ) → 𝐺 ∈ TarskiG )
185 179 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) ∧ 𝑊 = 𝑠 ) → 𝑊 ∈ 𝑃 )
186 178 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) ∧ 𝑊 = 𝑠 ) → 𝑉 ∈ 𝑃 )
187 157 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝑋 ∈ 𝑃 )
188 158 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝑌 ∈ 𝑃 )
189 159 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝑍 ∈ 𝑃 )
190 5 a1i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → ∼ = ( cgrA ‘ 𝐺 ) )
191 190 175 breqdi ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → ⟨“ 𝑊 𝑉 𝑠 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
192 1 3 177 50 179 178 180 187 188 189 191 cgracom ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑊 𝑉 𝑠 ”⟩ )
193 169 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) )
194 1 3 4 177 187 188 189 179 178 180 192 193 cgrabtwn ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝑉 ∈ ( 𝑊 𝐼 𝑠 ) )
195 194 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) ∧ 𝑊 = 𝑠 ) → 𝑉 ∈ ( 𝑊 𝐼 𝑠 ) )
196 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) ∧ 𝑊 = 𝑠 ) → 𝑊 = 𝑠 )
197 196 oveq2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) ∧ 𝑊 = 𝑠 ) → ( 𝑊 𝐼 𝑊 ) = ( 𝑊 𝐼 𝑠 ) )
198 195 197 eleqtrrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) ∧ 𝑊 = 𝑠 ) → 𝑉 ∈ ( 𝑊 𝐼 𝑊 ) )
199 1 4 3 184 185 186 198 axtgbtwnid ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) ∧ 𝑊 = 𝑠 ) → 𝑊 = 𝑉 )
200 183 199 mtand ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → ¬ 𝑊 = 𝑠 )
201 200 neqned ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝑊 ≠ 𝑠 )
202 1 3 6 177 179 180 178 201 194 btwnlng1 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝑉 ∈ ( 𝑊 𝐿 𝑠 ) )
203 1 3 6 177 178 179 180 181 202 201 lnrot2 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝑠 ∈ ( 𝑉 𝐿 𝑊 ) )
204 160 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝑈 ∈ 𝑃 )
205 1 4 3 177 180 204 tgbtwntriv1 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝑠 ∈ ( 𝑠 𝐼 𝑈 ) )
206 203 205 elind ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → 𝑠 ∈ ( ( 𝑉 𝐿 𝑊 ) ∩ ( 𝑠 𝐼 𝑈 ) ) )
207 206 ne0d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → ( ( 𝑉 𝐿 𝑊 ) ∩ ( 𝑠 𝐼 𝑈 ) ) ≠ ∅ )
208 175 176 207 3jca ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) → ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ∧ ( ( 𝑉 𝐿 𝑊 ) ∩ ( 𝑠 𝐼 𝑈 ) ) ≠ ∅ ) )
209 208 anasss ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) ) → ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ∧ ( ( 𝑉 𝐿 𝑊 ) ∩ ( 𝑠 𝐼 𝑈 ) ) ≠ ∅ ) )
210 174 209 impbida ⊢ ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑠 ∈ 𝑃 ) → ( ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ∧ ( ( 𝑉 𝐿 𝑊 ) ∩ ( 𝑠 𝐼 𝑈 ) ) ≠ ∅ ) ↔ ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) ) )
211 210 reubidva ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → ( ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ∧ ( ( 𝑉 𝐿 𝑊 ) ∩ ( 𝑠 𝐼 𝑈 ) ) ≠ ∅ ) ↔ ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) ) )
212 170 211 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) )
213 exmidd ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) → ( 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ∨ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) )
214 155 212 213 mpjaodan ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) )
215 17 necomd ⊢ ( 𝜑 → 𝑍 ≠ 𝑌 )
216 1 3 6 7 13 12 11 215 18 lncom ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑍 𝐿 𝑌 ) )
217 1 3 50 13 12 11 7 11 6 216 lnhl ⊢ ( 𝜑 → ( 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ∨ 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) ) )
218 112 214 217 mpjaodan ⊢ ( 𝜑 → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) )