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	⊢ 𝑃 = ( Base ‘ 𝐺 )
	tgbtwncgr.m	⊢ − = ( dist ‘ 𝐺 )
	tgbtwncgr.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tgbtwncgr.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tgbtwncgr.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	tgbtwncgr.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	tgbtwncgr.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	tgbtwncgr.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
	tgcgrsub.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
	tgcgrsub.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
	tgcgrsub.1	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
	tgcgrsub.2	⊢ ( 𝜑 → 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) )
	tgcgrsub.3	⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) = ( 𝐷 − 𝐹 ) )
	tgcgrsub.4	⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) )
Assertion	tgcgrsub	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		tgbtwncgr.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		tgbtwncgr.m	⊢ − = ( dist ‘ 𝐺 )
3		tgbtwncgr.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		tgbtwncgr.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		tgbtwncgr.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6		tgbtwncgr.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7		tgbtwncgr.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8		tgbtwncgr.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
9		tgcgrsub.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
10		tgcgrsub.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
11		tgcgrsub.1	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
12		tgcgrsub.2	⊢ ( 𝜑 → 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) )
13		tgcgrsub.3	⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) = ( 𝐷 − 𝐹 ) )
14		tgcgrsub.4	⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) )
15	1 2 3 4 5 8	tgcgrtriv	⊢ ( 𝜑 → ( 𝐴 − 𝐴 ) = ( 𝐷 − 𝐷 ) )
16	1 2 3 4 5 7 8 10 13	tgcgrcomlr	⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) = ( 𝐹 − 𝐷 ) )
17	1 2 3 4 5 6 7 5 8 9 10 8 11 12 13 14 15 16	tgifscgr	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) = ( 𝐸 − 𝐷 ) )
18	1 2 3 4 6 5 9 8 17	tgcgrcomlr	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )