Metamath Proof Explorer


Theorem tgsegconeq

Description: Two points that satisfy the conclusion of axtgsegcon are identical. Uniqueness portion of Theorem 2.12 of Schwabhauser p. 29. (Contributed by Thierry Arnoux, 23-Mar-2019)

Ref Expression
Hypotheses tkgeom.p 𝑃 = ( Base ‘ 𝐺 )
tkgeom.d = ( dist ‘ 𝐺 )
tkgeom.i 𝐼 = ( Itv ‘ 𝐺 )
tkgeom.g ( 𝜑𝐺 ∈ TarskiG )
tgcgrextend.a ( 𝜑𝐴𝑃 )
tgcgrextend.b ( 𝜑𝐵𝑃 )
tgcgrextend.c ( 𝜑𝐶𝑃 )
tgcgrextend.d ( 𝜑𝐷𝑃 )
tgcgrextend.e ( 𝜑𝐸𝑃 )
tgcgrextend.f ( 𝜑𝐹𝑃 )
tgsegconeq.1 ( 𝜑𝐷𝐴 )
tgsegconeq.2 ( 𝜑𝐴 ∈ ( 𝐷 𝐼 𝐸 ) )
tgsegconeq.3 ( 𝜑𝐴 ∈ ( 𝐷 𝐼 𝐹 ) )
tgsegconeq.4 ( 𝜑 → ( 𝐴 𝐸 ) = ( 𝐵 𝐶 ) )
tgsegconeq.5 ( 𝜑 → ( 𝐴 𝐹 ) = ( 𝐵 𝐶 ) )
Assertion tgsegconeq ( 𝜑𝐸 = 𝐹 )

Proof

Step Hyp Ref Expression
1 tkgeom.p 𝑃 = ( Base ‘ 𝐺 )
2 tkgeom.d = ( dist ‘ 𝐺 )
3 tkgeom.i 𝐼 = ( Itv ‘ 𝐺 )
4 tkgeom.g ( 𝜑𝐺 ∈ TarskiG )
5 tgcgrextend.a ( 𝜑𝐴𝑃 )
6 tgcgrextend.b ( 𝜑𝐵𝑃 )
7 tgcgrextend.c ( 𝜑𝐶𝑃 )
8 tgcgrextend.d ( 𝜑𝐷𝑃 )
9 tgcgrextend.e ( 𝜑𝐸𝑃 )
10 tgcgrextend.f ( 𝜑𝐹𝑃 )
11 tgsegconeq.1 ( 𝜑𝐷𝐴 )
12 tgsegconeq.2 ( 𝜑𝐴 ∈ ( 𝐷 𝐼 𝐸 ) )
13 tgsegconeq.3 ( 𝜑𝐴 ∈ ( 𝐷 𝐼 𝐹 ) )
14 tgsegconeq.4 ( 𝜑 → ( 𝐴 𝐸 ) = ( 𝐵 𝐶 ) )
15 tgsegconeq.5 ( 𝜑 → ( 𝐴 𝐹 ) = ( 𝐵 𝐶 ) )
16 eqidd ( 𝜑 → ( 𝐷 𝐴 ) = ( 𝐷 𝐴 ) )
17 eqidd ( 𝜑 → ( 𝐴 𝐸 ) = ( 𝐴 𝐸 ) )
18 14 15 eqtr4d ( 𝜑 → ( 𝐴 𝐸 ) = ( 𝐴 𝐹 ) )
19 1 2 3 4 8 5 9 8 5 10 12 13 16 18 tgcgrextend ( 𝜑 → ( 𝐷 𝐸 ) = ( 𝐷 𝐹 ) )
20 1 2 3 4 8 5 9 8 5 9 9 10 11 12 12 16 17 19 18 axtg5seg ( 𝜑 → ( 𝐸 𝐸 ) = ( 𝐸 𝐹 ) )
21 20 eqcomd ( 𝜑 → ( 𝐸 𝐹 ) = ( 𝐸 𝐸 ) )
22 1 2 3 4 9 10 9 21 axtgcgrid ( 𝜑𝐸 = 𝐹 )