Metamath Proof Explorer

Theorem angmgmaddeu2

Description: Existence of a unique point for building angle addition. Case where the second angle is a zero angle. (Contributed by Thierry Arnoux, 23-Aug-2026)

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

Proof

Step Hyp Ref Expression
1 angmgmadd.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 angmgmadd.a ⊢ 𝐴 = { 𝑑 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) }
3 angmgmadd.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 angmgmadd.d ⊢ − = ( dist ‘ 𝐺 )
5 angmgmadd.c ⊢ ∼ = ( cgrA ‘ 𝐺 )
6 angmgmadd.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
7 angmgmadd.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
8 angmgmaddov.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
9 angmgmaddov.v ⊢ ( 𝜑 → 𝑉 ∈ 𝑃 )
10 angmgmaddov.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
11 angmgmaddov.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
12 angmgmaddov.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
13 angmgmaddov.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
14 angmgmaddeu.1 ⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
15 angmgmaddeu.2 ⊢ ( 𝜑 → 𝑉 ≠ 𝑊 )
16 angmgmaddeu.3 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
17 angmgmaddeu.4 ⊢ ( 𝜑 → 𝑌 ≠ 𝑍 )
18 angmgmaddeu2.1 ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) )
19 angmgmaddeu2.2 ⊢ ( 𝜑 → 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 )
20 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
21 17 necomd ⊢ ( 𝜑 → 𝑍 ≠ 𝑌 )
22 14 necomd ⊢ ( 𝜑 → 𝑉 ≠ 𝑈 )
23 1 3 20 12 9 8 7 13 4 21 22 hlcgreu ⊢ ( 𝜑 → ∃! 𝑠 ∈ 𝑃 ( 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) )
24 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝐺 ∈ TarskiG )
25 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑠 ∈ 𝑃 )
26 13 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑍 ∈ 𝑃 )
27 12 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑌 ∈ 𝑃 )
28 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 )
29 1 3 20 25 26 27 24 28 hlcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑍 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑠 )
30 19 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 )
31 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑉 ∈ 𝑃 )
32 1 5 20 24 29 30 27 31 zerocgra ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
33 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) )
34 17 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑌 ≠ 𝑍 )
35 1 3 20 26 25 27 24 6 29 hlln ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑍 ∈ ( 𝑠 𝐿 𝑌 ) )
36 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑈 ∈ 𝑃 )
37 33 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → ( 𝑉 − 𝑈 ) = ( 𝑌 − 𝑠 ) )
38 22 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑉 ≠ 𝑈 )
39 1 4 3 24 31 36 27 25 37 38 tgcgrneq ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑌 ≠ 𝑠 )
40 39 necomd ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑠 ≠ 𝑌 )
41 1 3 6 24 27 26 25 34 35 40 lnrot1 ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑠 ∈ ( 𝑌 𝐿 𝑍 ) )
42 11 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑋 ∈ 𝑃 )
43 1 4 3 24 25 42 tgbtwntriv1 ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑠 ∈ ( 𝑠 𝐼 𝑋 ) )
44 41 43 elind ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑠 ∈ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) )
45 44 ne0d ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ )
46 32 33 45 3jca ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) )
47 46 anasss ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ) → ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) )
48 13 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑍 ∈ 𝑃 )
49 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑠 ∈ 𝑃 )
50 12 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑌 ∈ 𝑃 )
51 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝐺 ∈ TarskiG )
52 8 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑈 ∈ 𝑃 )
53 9 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑉 ∈ 𝑃 )
54 10 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑊 ∈ 𝑃 )
55 5 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ∼ = ( cgrA ‘ 𝐺 ) )
56 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
57 55 56 breqdi ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ⟨“ 𝑍 𝑌 𝑠 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
58 1 3 51 20 48 50 49 52 53 54 57 cgracom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ⟨“ 𝑈 𝑉 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ )
59 19 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 )
60 1 3 4 51 52 53 54 48 50 49 58 20 59 cgrahl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑍 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑠 )
61 1 3 20 48 49 50 51 60 hlcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 )
62 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) )
63 61 62 jca ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ( 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) )
64 63 3anasss ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) ) → ( 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) )
65 47 64 impbida ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) → ( ( 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ↔ ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) ) )
66 65 reubidva ⊢ ( 𝜑 → ( ∃! 𝑠 ∈ 𝑃 ( 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ↔ ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) ) )
67 23 66 mpbid ⊢ ( 𝜑 → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) )