Metamath Proof Explorer


Theorem tgldim0cgr

Description: In dimension zero, any two pairs of points are congruent. (Contributed by Thierry Arnoux, 12-Apr-2019)

Ref Expression
Hypotheses tgbtwndiff.p 𝑃 = ( Base ‘ 𝐺 )
tgbtwndiff.d = ( dist ‘ 𝐺 )
tgbtwndiff.i 𝐼 = ( Itv ‘ 𝐺 )
tgbtwndiff.g ( 𝜑𝐺 ∈ TarskiG )
tgbtwndiff.a ( 𝜑𝐴𝑃 )
tgbtwndiff.b ( 𝜑𝐵𝑃 )
tgldim0itv.c ( 𝜑𝐶𝑃 )
tgldim0itv.p ( 𝜑 → ( ♯ ‘ 𝑃 ) = 1 )
tgldim0itv.d ( 𝜑𝐷𝑃 )
Assertion tgldim0cgr ( 𝜑 → ( 𝐴 𝐵 ) = ( 𝐶 𝐷 ) )

Proof

Step Hyp Ref Expression
1 tgbtwndiff.p 𝑃 = ( Base ‘ 𝐺 )
2 tgbtwndiff.d = ( dist ‘ 𝐺 )
3 tgbtwndiff.i 𝐼 = ( Itv ‘ 𝐺 )
4 tgbtwndiff.g ( 𝜑𝐺 ∈ TarskiG )
5 tgbtwndiff.a ( 𝜑𝐴𝑃 )
6 tgbtwndiff.b ( 𝜑𝐵𝑃 )
7 tgldim0itv.c ( 𝜑𝐶𝑃 )
8 tgldim0itv.p ( 𝜑 → ( ♯ ‘ 𝑃 ) = 1 )
9 tgldim0itv.d ( 𝜑𝐷𝑃 )
10 1 8 5 7 tgldim0eq ( 𝜑𝐴 = 𝐶 )
11 1 8 6 9 tgldim0eq ( 𝜑𝐵 = 𝐷 )
12 10 11 oveq12d ( 𝜑 → ( 𝐴 𝐵 ) = ( 𝐶 𝐷 ) )