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	|- P = ( Base ` G )
	tgbtwndiff.d	|- .- = ( dist ` G )
	tgbtwndiff.i	|- I = ( Itv ` G )
	tgbtwndiff.g	|- ( ph -> G e. TarskiG )
	tgbtwndiff.a	|- ( ph -> A e. P )
	tgbtwndiff.b	|- ( ph -> B e. P )
	tgldim0itv.c	|- ( ph -> C e. P )
	tgldim0itv.p	|- ( ph -> ( # ` P ) = 1 )
	tgldim0itv.d	|- ( ph -> D e. P )
Assertion	tgldim0cgr	|- ( ph -> ( A .- B ) = ( C .- D ) )

Proof

Step	Hyp	Ref	Expression
1		tgbtwndiff.p	|- P = ( Base ` G )
2		tgbtwndiff.d	|- .- = ( dist ` G )
3		tgbtwndiff.i	|- I = ( Itv ` G )
4		tgbtwndiff.g	|- ( ph -> G e. TarskiG )
5		tgbtwndiff.a	|- ( ph -> A e. P )
6		tgbtwndiff.b	|- ( ph -> B e. P )
7		tgldim0itv.c	|- ( ph -> C e. P )
8		tgldim0itv.p	|- ( ph -> ( # ` P ) = 1 )
9		tgldim0itv.d	|- ( ph -> D e. P )
10	1 8 5 7	tgldim0eq	|- ( ph -> A = C )
11	1 8 6 9	tgldim0eq	|- ( ph -> B = D )
12	10 11	oveq12d	|- ( ph -> ( A .- B ) = ( C .- D ) )