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 
|- P = ( Base ` G )
tkgeom.d 
|- .- = ( dist ` G )
tkgeom.i 
|- I = ( Itv ` G )
tkgeom.g 
|- ( ph -> G e. TarskiG )
tgsegconeu.x 
|- ( ph -> X e. P )
tgsegconeu.y 
|- ( ph -> Y e. P )
tgsegconeu.a 
|- ( ph -> A e. P )
tgsegconeu.b 
|- ( ph -> B e. P )
tgsegconeu.1 
|- ( ph -> X =/= Y )
Assertion tgsegconeu 
|- ( ph -> E! z e. P ( Y e. ( X I z ) /\ ( Y .- z ) = ( A .- B ) ) )

Proof

Step Hyp Ref Expression
1 tkgeom.p 
 |-  P = ( Base ` G )
2 tkgeom.d 
 |-  .- = ( dist ` G )
3 tkgeom.i 
 |-  I = ( Itv ` G )
4 tkgeom.g 
 |-  ( ph -> G e. TarskiG )
5 tgsegconeu.x 
 |-  ( ph -> X e. P )
6 tgsegconeu.y 
 |-  ( ph -> Y e. P )
7 tgsegconeu.a 
 |-  ( ph -> A e. P )
8 tgsegconeu.b 
 |-  ( ph -> B e. P )
9 tgsegconeu.1 
 |-  ( ph -> X =/= Y )
10 1 2 3 4 5 6 7 8 axtgsegcon 
 |-  ( ph -> E. z e. P ( Y e. ( X I z ) /\ ( Y .- z ) = ( A .- B ) ) )
11 4 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ z e. P ) /\ s e. P ) /\ ( Y .- s ) = ( A .- B ) ) /\ Y e. ( X I s ) ) /\ Y e. ( X I z ) ) /\ ( Y .- z ) = ( A .- B ) ) -> G e. TarskiG )
12 6 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ z e. P ) /\ s e. P ) /\ ( Y .- s ) = ( A .- B ) ) /\ Y e. ( X I s ) ) /\ Y e. ( X I z ) ) /\ ( Y .- z ) = ( A .- B ) ) -> Y e. P )
13 7 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ z e. P ) /\ s e. P ) /\ ( Y .- s ) = ( A .- B ) ) /\ Y e. ( X I s ) ) /\ Y e. ( X I z ) ) /\ ( Y .- z ) = ( A .- B ) ) -> A e. P )
14 8 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ z e. P ) /\ s e. P ) /\ ( Y .- s ) = ( A .- B ) ) /\ Y e. ( X I s ) ) /\ Y e. ( X I z ) ) /\ ( Y .- z ) = ( A .- B ) ) -> B e. P )
15 5 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ z e. P ) /\ s e. P ) /\ ( Y .- s ) = ( A .- B ) ) /\ Y e. ( X I s ) ) /\ Y e. ( X I z ) ) /\ ( Y .- z ) = ( A .- B ) ) -> X e. P )
16 simp-6r 
 |-  ( ( ( ( ( ( ( ph /\ z e. P ) /\ s e. P ) /\ ( Y .- s ) = ( A .- B ) ) /\ Y e. ( X I s ) ) /\ Y e. ( X I z ) ) /\ ( Y .- z ) = ( A .- B ) ) -> z e. P )
17 simp-5r 
 |-  ( ( ( ( ( ( ( ph /\ z e. P ) /\ s e. P ) /\ ( Y .- s ) = ( A .- B ) ) /\ Y e. ( X I s ) ) /\ Y e. ( X I z ) ) /\ ( Y .- z ) = ( A .- B ) ) -> s e. P )
18 9 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ z e. P ) /\ s e. P ) /\ ( Y .- s ) = ( A .- B ) ) /\ Y e. ( X I s ) ) /\ Y e. ( X I z ) ) /\ ( Y .- z ) = ( A .- B ) ) -> X =/= Y )
19 simplr 
 |-  ( ( ( ( ( ( ( ph /\ z e. P ) /\ s e. P ) /\ ( Y .- s ) = ( A .- B ) ) /\ Y e. ( X I s ) ) /\ Y e. ( X I z ) ) /\ ( Y .- z ) = ( A .- B ) ) -> Y e. ( X I z ) )
20 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ z e. P ) /\ s e. P ) /\ ( Y .- s ) = ( A .- B ) ) /\ Y e. ( X I s ) ) /\ Y e. ( X I z ) ) /\ ( Y .- z ) = ( A .- B ) ) -> Y e. ( X I s ) )
21 simpr 
 |-  ( ( ( ( ( ( ( ph /\ z e. P ) /\ s e. P ) /\ ( Y .- s ) = ( A .- B ) ) /\ Y e. ( X I s ) ) /\ Y e. ( X I z ) ) /\ ( Y .- z ) = ( A .- B ) ) -> ( Y .- z ) = ( A .- B ) )
22 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ z e. P ) /\ s e. P ) /\ ( Y .- s ) = ( A .- B ) ) /\ Y e. ( X I s ) ) /\ Y e. ( X I z ) ) /\ ( Y .- z ) = ( A .- B ) ) -> ( Y .- s ) = ( A .- B ) )
23 1 2 3 11 12 13 14 15 16 17 18 19 20 21 22 tgsegconeq 
 |-  ( ( ( ( ( ( ( ph /\ z e. P ) /\ s e. P ) /\ ( Y .- s ) = ( A .- B ) ) /\ Y e. ( X I s ) ) /\ Y e. ( X I z ) ) /\ ( Y .- z ) = ( A .- B ) ) -> z = s )
24 23 anasss 
 |-  ( ( ( ( ( ( ph /\ z e. P ) /\ s e. P ) /\ ( Y .- s ) = ( A .- B ) ) /\ Y e. ( X I s ) ) /\ ( Y e. ( X I z ) /\ ( Y .- z ) = ( A .- B ) ) ) -> z = s )
25 24 an42ds 
 |-  ( ( ( ( ( ( ph /\ z e. P ) /\ s e. P ) /\ ( Y e. ( X I z ) /\ ( Y .- z ) = ( A .- B ) ) ) /\ Y e. ( X I s ) ) /\ ( Y .- s ) = ( A .- B ) ) -> z = s )
26 25 anasss 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ s e. P ) /\ ( Y e. ( X I z ) /\ ( Y .- z ) = ( A .- B ) ) ) /\ ( Y e. ( X I s ) /\ ( Y .- s ) = ( A .- B ) ) ) -> z = s )
27 26 expl 
 |-  ( ( ( ph /\ z e. P ) /\ s e. P ) -> ( ( ( Y e. ( X I z ) /\ ( Y .- z ) = ( A .- B ) ) /\ ( Y e. ( X I s ) /\ ( Y .- s ) = ( A .- B ) ) ) -> z = s ) )
28 27 anasss 
 |-  ( ( ph /\ ( z e. P /\ s e. P ) ) -> ( ( ( Y e. ( X I z ) /\ ( Y .- z ) = ( A .- B ) ) /\ ( Y e. ( X I s ) /\ ( Y .- s ) = ( A .- B ) ) ) -> z = s ) )
29 28 ralrimivva 
 |-  ( ph -> A. z e. P A. s e. P ( ( ( Y e. ( X I z ) /\ ( Y .- z ) = ( A .- B ) ) /\ ( Y e. ( X I s ) /\ ( Y .- s ) = ( A .- B ) ) ) -> z = s ) )
30 oveq2 
 |-  ( z = s -> ( X I z ) = ( X I s ) )
31 30 eleq2d 
 |-  ( z = s -> ( Y e. ( X I z ) <-> Y e. ( X I s ) ) )
32 oveq2 
 |-  ( z = s -> ( Y .- z ) = ( Y .- s ) )
33 32 eqeq1d 
 |-  ( z = s -> ( ( Y .- z ) = ( A .- B ) <-> ( Y .- s ) = ( A .- B ) ) )
34 31 33 anbi12d 
 |-  ( z = s -> ( ( Y e. ( X I z ) /\ ( Y .- z ) = ( A .- B ) ) <-> ( Y e. ( X I s ) /\ ( Y .- s ) = ( A .- B ) ) ) )
35 34 reu4 
 |-  ( E! z e. P ( Y e. ( X I z ) /\ ( Y .- z ) = ( A .- B ) ) <-> ( E. z e. P ( Y e. ( X I z ) /\ ( Y .- z ) = ( A .- B ) ) /\ A. z e. P A. s e. P ( ( ( Y e. ( X I z ) /\ ( Y .- z ) = ( A .- B ) ) /\ ( Y e. ( X I s ) /\ ( Y .- s ) = ( A .- B ) ) ) -> z = s ) ) )
36 10 29 35 sylanbrc 
 |-  ( ph -> E! z e. P ( Y e. ( X I z ) /\ ( Y .- z ) = ( A .- B ) ) )