Metamath Proof Explorer

Theorem tgsegconeu

Description: The point constructed in axtgsegcon is unique. (Contributed by Thierry Arnoux, 23-Aug-2026)

Ref Expression
Hypotheses tkgeom.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
tkgeom.d ⊢ − = ( dist ‘ 𝐺 )
tkgeom.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tkgeom.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tgsegconeu.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
tgsegconeu.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
tgsegconeu.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
tgsegconeu.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
tgsegconeu.1 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
Assertion tgsegconeu ( 𝜑 → ∃! 𝑧 ∈ 𝑃 ( 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ∧ ( 𝑌 − 𝑧 ) = ( 𝐴 − 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 tkgeom.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tkgeom.d ⊢ − = ( dist ‘ 𝐺 )
3 tkgeom.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 tkgeom.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 tgsegconeu.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
6 tgsegconeu.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
7 tgsegconeu.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
8 tgsegconeu.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
9 tgsegconeu.1 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
10 1 2 3 4 5 6 7 8 axtgsegcon ⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑃 ( 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ∧ ( 𝑌 − 𝑧 ) = ( 𝐴 − 𝐵 ) ) )
11 4 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝐴 − 𝐵 ) ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ∧ ( 𝑌 − 𝑧 ) = ( 𝐴 − 𝐵 ) ) → 𝐺 ∈ TarskiG )
12 6 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝐴 − 𝐵 ) ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ∧ ( 𝑌 − 𝑧 ) = ( 𝐴 − 𝐵 ) ) → 𝑌 ∈ 𝑃 )
13 7 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝐴 − 𝐵 ) ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ∧ ( 𝑌 − 𝑧 ) = ( 𝐴 − 𝐵 ) ) → 𝐴 ∈ 𝑃 )
14 8 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝐴 − 𝐵 ) ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ∧ ( 𝑌 − 𝑧 ) = ( 𝐴 − 𝐵 ) ) → 𝐵 ∈ 𝑃 )
15 5 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝐴 − 𝐵 ) ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ∧ ( 𝑌 − 𝑧 ) = ( 𝐴 − 𝐵 ) ) → 𝑋 ∈ 𝑃 )
16 simp-6r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝐴 − 𝐵 ) ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ∧ ( 𝑌 − 𝑧 ) = ( 𝐴 − 𝐵 ) ) → 𝑧 ∈ 𝑃 )
17 simp-5r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝐴 − 𝐵 ) ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ∧ ( 𝑌 − 𝑧 ) = ( 𝐴 − 𝐵 ) ) → 𝑠 ∈ 𝑃 )
18 9 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝐴 − 𝐵 ) ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ∧ ( 𝑌 − 𝑧 ) = ( 𝐴 − 𝐵 ) ) → 𝑋 ≠ 𝑌 )
19 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝐴 − 𝐵 ) ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ∧ ( 𝑌 − 𝑧 ) = ( 𝐴 − 𝐵 ) ) → 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) )
20 simpllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝐴 − 𝐵 ) ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ∧ ( 𝑌 − 𝑧 ) = ( 𝐴 − 𝐵 ) ) → 𝑌 ∈ ( 𝑋 𝐼 𝑠 ) )
21 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝐴 − 𝐵 ) ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ∧ ( 𝑌 − 𝑧 ) = ( 𝐴 − 𝐵 ) ) → ( 𝑌 − 𝑧 ) = ( 𝐴 − 𝐵 ) )
22 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝐴 − 𝐵 ) ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ∧ ( 𝑌 − 𝑧 ) = ( 𝐴 − 𝐵 ) ) → ( 𝑌 − 𝑠 ) = ( 𝐴 − 𝐵 ) )
23 1 2 3 11 12 13 14 15 16 17 18 19 20 21 22 tgsegconeq ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝐴 − 𝐵 ) ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ∧ ( 𝑌 − 𝑧 ) = ( 𝐴 − 𝐵 ) ) → 𝑧 = 𝑠 )
24 23 anasss ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝐴 − 𝐵 ) ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ∧ ( 𝑌 − 𝑧 ) = ( 𝐴 − 𝐵 ) ) ) → 𝑧 = 𝑠 )
25 24 an42ds ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ∧ ( 𝑌 − 𝑧 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ ( 𝑌 − 𝑠 ) = ( 𝐴 − 𝐵 ) ) → 𝑧 = 𝑠 )
26 25 anasss ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ∧ ( 𝑌 − 𝑧 ) = ( 𝐴 − 𝐵 ) ) ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑠 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝐴 − 𝐵 ) ) ) → 𝑧 = 𝑠 )
27 26 expl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) → ( ( ( 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ∧ ( 𝑌 − 𝑧 ) = ( 𝐴 − 𝐵 ) ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑠 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝐴 − 𝐵 ) ) ) → 𝑧 = 𝑠 ) )
28 27 anasss ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑃 ∧ 𝑠 ∈ 𝑃 ) ) → ( ( ( 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ∧ ( 𝑌 − 𝑧 ) = ( 𝐴 − 𝐵 ) ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑠 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝐴 − 𝐵 ) ) ) → 𝑧 = 𝑠 ) )
29 28 ralrimivva ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑃 ∀ 𝑠 ∈ 𝑃 ( ( ( 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ∧ ( 𝑌 − 𝑧 ) = ( 𝐴 − 𝐵 ) ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑠 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝐴 − 𝐵 ) ) ) → 𝑧 = 𝑠 ) )
30 oveq2 ⊢ ( 𝑧 = 𝑠 → ( 𝑋 𝐼 𝑧 ) = ( 𝑋 𝐼 𝑠 ) )
31 30 eleq2d ⊢ ( 𝑧 = 𝑠 → ( 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ↔ 𝑌 ∈ ( 𝑋 𝐼 𝑠 ) ) )
32 oveq2 ⊢ ( 𝑧 = 𝑠 → ( 𝑌 − 𝑧 ) = ( 𝑌 − 𝑠 ) )
33 32 eqeq1d ⊢ ( 𝑧 = 𝑠 → ( ( 𝑌 − 𝑧 ) = ( 𝐴 − 𝐵 ) ↔ ( 𝑌 − 𝑠 ) = ( 𝐴 − 𝐵 ) ) )
34 31 33 anbi12d ⊢ ( 𝑧 = 𝑠 → ( ( 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ∧ ( 𝑌 − 𝑧 ) = ( 𝐴 − 𝐵 ) ) ↔ ( 𝑌 ∈ ( 𝑋 𝐼 𝑠 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝐴 − 𝐵 ) ) ) )
35 34 reu4 ⊢ ( ∃! 𝑧 ∈ 𝑃 ( 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ∧ ( 𝑌 − 𝑧 ) = ( 𝐴 − 𝐵 ) ) ↔ ( ∃ 𝑧 ∈ 𝑃 ( 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ∧ ( 𝑌 − 𝑧 ) = ( 𝐴 − 𝐵 ) ) ∧ ∀ 𝑧 ∈ 𝑃 ∀ 𝑠 ∈ 𝑃 ( ( ( 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ∧ ( 𝑌 − 𝑧 ) = ( 𝐴 − 𝐵 ) ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑠 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝐴 − 𝐵 ) ) ) → 𝑧 = 𝑠 ) ) )
36 10 29 35 sylanbrc ⊢ ( 𝜑 → ∃! 𝑧 ∈ 𝑃 ( 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ∧ ( 𝑌 − 𝑧 ) = ( 𝐴 − 𝐵 ) ) )