Theorem tgcgrsub

Description: Removing identical parts from the end of a line segment preserves congruence. Theorem 4.3 of Schwabhauser p. 35. (Contributed by Thierry Arnoux, 3-Apr-2019)

	Ref	Expression
Hypotheses	tgbtwncgr.p	$$⊢P={\mathrm{Base}}_G$$
	tgbtwncgr.m	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	tgbtwncgr.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	tgbtwncgr.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	tgbtwncgr.a	$$⊢\phi \to A\in P$$
	tgbtwncgr.b	$$⊢\phi \to B\in P$$
	tgbtwncgr.c	$$⊢\phi \to C\in P$$
	tgbtwncgr.d	$$⊢\phi \to D\in P$$
	tgcgrsub.e	$$⊢\phi \to E\in P$$
	tgcgrsub.f	$$⊢\phi \to F\in P$$
	tgcgrsub.1	$$⊢\phi \to B\in \left(AIC\right)$$
	tgcgrsub.2	$$⊢\phi \to E\in \left(DIF\right)$$
	tgcgrsub.3	$$⊢\phi \to A\underset{\dot{}}{-}C=D\underset{\dot{}}{-}F$$
	tgcgrsub.4	$$⊢\phi \to B\underset{\dot{}}{-}C=E\underset{\dot{}}{-}F$$
Assertion	tgcgrsub	$$⊢\phi \to A\underset{\dot{}}{-}B=D\underset{\dot{}}{-}E$$

Proof

Step	Hyp	Ref	Expression
1		tgbtwncgr.p	$$⊢P={\mathrm{Base}}_G$$
2		tgbtwncgr.m	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		tgbtwncgr.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		tgbtwncgr.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
5		tgbtwncgr.a	$$⊢\phi \to A\in P$$
6		tgbtwncgr.b	$$⊢\phi \to B\in P$$
7		tgbtwncgr.c	$$⊢\phi \to C\in P$$
8		tgbtwncgr.d	$$⊢\phi \to D\in P$$
9		tgcgrsub.e	$$⊢\phi \to E\in P$$
10		tgcgrsub.f	$$⊢\phi \to F\in P$$
11		tgcgrsub.1	$$⊢\phi \to B\in \left(AIC\right)$$
12		tgcgrsub.2	$$⊢\phi \to E\in \left(DIF\right)$$
13		tgcgrsub.3	$$⊢\phi \to A\underset{\dot{}}{-}C=D\underset{\dot{}}{-}F$$
14		tgcgrsub.4	$$⊢\phi \to B\underset{\dot{}}{-}C=E\underset{\dot{}}{-}F$$
15	1 2 3 4 5 8	tgcgrtriv	$$⊢\phi \to A\underset{\dot{}}{-}A=D\underset{\dot{}}{-}D$$
16	1 2 3 4 5 7 8 10 13	tgcgrcomlr	$$⊢\phi \to C\underset{\dot{}}{-}A=F\underset{\dot{}}{-}D$$
17	1 2 3 4 5 6 7 5 8 9 10 8 11 12 13 14 15 16	tgifscgr	$$⊢\phi \to B\underset{\dot{}}{-}A=E\underset{\dot{}}{-}D$$
18	1 2 3 4 6 5 9 8 17	tgcgrcomlr	$$⊢\phi \to A\underset{\dot{}}{-}B=D\underset{\dot{}}{-}E$$