Metamath Proof Explorer

Theorem angmndaddeu3

Description: Existence of a unique point for building angle addition. Case where the second angle is a flat angle. (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 ⊢ ( 𝜑 → 𝑌 ≠ 𝑍 )
angmndaddeu3.1 ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) )
angmndaddeu3.2 ⊢ ( 𝜑 → 𝑉 ∈ ( 𝑈 𝐼 𝑊 ) )
Assertion angmndaddeu3 ( 𝜑 → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) )

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 angmndaddeu3.1 ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) )
19 angmndaddeu3.2 ⊢ ( 𝜑 → 𝑉 ∈ ( 𝑈 𝐼 𝑊 ) )
20 17 necomd ⊢ ( 𝜑 → 𝑍 ≠ 𝑌 )
21 1 4 3 7 13 12 9 8 20 tgsegconeu ⊢ ( 𝜑 → ∃! 𝑠 ∈ 𝑃 ( 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) )
22 5 eqcomi ⊢ ( cgrA ‘ 𝐺 ) = ∼
23 22 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → ( cgrA ‘ 𝐺 ) = ∼ )
24 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝐺 ∈ TarskiG )
25 13 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑍 ∈ 𝑃 )
26 12 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑌 ∈ 𝑃 )
27 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑠 ∈ 𝑃 )
28 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑈 ∈ 𝑃 )
29 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑉 ∈ 𝑃 )
30 10 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑊 ∈ 𝑃 )
31 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) )
32 19 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑉 ∈ ( 𝑈 𝐼 𝑊 ) )
33 20 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑍 ≠ 𝑌 )
34 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) )
35 34 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → ( 𝑉 − 𝑈 ) = ( 𝑌 − 𝑠 ) )
36 14 necomd ⊢ ( 𝜑 → 𝑉 ≠ 𝑈 )
37 36 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑉 ≠ 𝑈 )
38 1 4 3 24 29 28 26 27 35 37 tgcgrneq ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑌 ≠ 𝑠 )
39 38 necomd ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑠 ≠ 𝑌 )
40 14 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑈 ≠ 𝑉 )
41 15 necomd ⊢ ( 𝜑 → 𝑊 ≠ 𝑉 )
42 41 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑊 ≠ 𝑉 )
43 1 3 4 24 25 26 27 28 29 30 31 32 33 39 40 42 flatcgra ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → ⟨“ 𝑍 𝑌 𝑠 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
44 23 43 breqdi ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
45 17 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑌 ≠ 𝑍 )
46 24 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ 𝑍 = 𝑠 ) → 𝐺 ∈ TarskiG )
47 25 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ 𝑍 = 𝑠 ) → 𝑍 ∈ 𝑃 )
48 26 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ 𝑍 = 𝑠 ) → 𝑌 ∈ 𝑃 )
49 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ 𝑍 = 𝑠 ) → 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) )
50 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ 𝑍 = 𝑠 ) → 𝑍 = 𝑠 )
51 50 oveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ 𝑍 = 𝑠 ) → ( 𝑍 𝐼 𝑍 ) = ( 𝑍 𝐼 𝑠 ) )
52 49 51 eleqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ 𝑍 = 𝑠 ) → 𝑌 ∈ ( 𝑍 𝐼 𝑍 ) )
53 1 4 3 46 47 48 52 axtgbtwnid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ 𝑍 = 𝑠 ) → 𝑍 = 𝑌 )
54 53 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ 𝑍 = 𝑠 ) → 𝑌 = 𝑍 )
55 45 54 mteqand ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑍 ≠ 𝑠 )
56 1 3 6 24 25 27 26 55 31 btwnlng1 ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑌 ∈ ( 𝑍 𝐿 𝑠 ) )
57 1 3 6 24 26 25 27 45 56 55 lnrot2 ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑠 ∈ ( 𝑌 𝐿 𝑍 ) )
58 11 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑋 ∈ 𝑃 )
59 1 4 3 24 27 58 tgbtwntriv1 ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑠 ∈ ( 𝑠 𝐼 𝑋 ) )
60 57 59 elind ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑠 ∈ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) )
61 60 ne0d ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ )
62 44 34 61 3jca ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) )
63 62 anasss ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ) → ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) )
64 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝐺 ∈ TarskiG )
65 8 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑈 ∈ 𝑃 )
66 9 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑉 ∈ 𝑃 )
67 10 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑊 ∈ 𝑃 )
68 13 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑍 ∈ 𝑃 )
69 12 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑌 ∈ 𝑃 )
70 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑠 ∈ 𝑃 )
71 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
72 5 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ∼ = ( cgrA ‘ 𝐺 ) )
73 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
74 72 73 breqdi ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ⟨“ 𝑍 𝑌 𝑠 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
75 1 3 64 71 68 69 70 65 66 67 74 cgracom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ⟨“ 𝑈 𝑉 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ )
76 19 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑉 ∈ ( 𝑈 𝐼 𝑊 ) )
77 1 3 4 64 65 66 67 68 69 70 75 76 cgrabtwn ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) )
78 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) )
79 77 78 jca ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ( 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) )
80 79 3anasss ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) ) → ( 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) )
81 63 80 impbida ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) → ( ( 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ↔ ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) ) )
82 81 reubidva ⊢ ( 𝜑 → ( ∃! 𝑠 ∈ 𝑃 ( 𝑌 ∈ ( 𝑍 𝐼 𝑠 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ↔ ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) ) )
83 21 82 mpbid ⊢ ( 𝜑 → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) )