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={\mathrm{Base}}_G$$
	tgbtwndiff.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	tgbtwndiff.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	tgbtwndiff.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	tgbtwndiff.a	$$⊢\phi \to A\in P$$
	tgbtwndiff.b	$$⊢\phi \to B\in P$$
	tgldim0itv.c	$$⊢\phi \to C\in P$$
	tgldim0itv.p	$$⊢\phi \to \left|P\right|=1$$
	tgldim0itv.d	$$⊢\phi \to D\in P$$
Assertion	tgldim0cgr	$$⊢\phi \to A\underset{\dot{}}{-}B=C\underset{\dot{}}{-}D$$

Proof

Step	Hyp	Ref	Expression
1		tgbtwndiff.p	$$⊢P={\mathrm{Base}}_G$$
2		tgbtwndiff.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		tgbtwndiff.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		tgbtwndiff.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
5		tgbtwndiff.a	$$⊢\phi \to A\in P$$
6		tgbtwndiff.b	$$⊢\phi \to B\in P$$
7		tgldim0itv.c	$$⊢\phi \to C\in P$$
8		tgldim0itv.p	$$⊢\phi \to \left|P\right|=1$$
9		tgldim0itv.d	$$⊢\phi \to D\in P$$
10	1 8 5 7	tgldim0eq	$$⊢\phi \to A=C$$
11	1 8 6 9	tgldim0eq	$$⊢\phi \to B=D$$
12	10 11	oveq12d	$$⊢\phi \to A\underset{\dot{}}{-}B=C\underset{\dot{}}{-}D$$