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 = ( Base ` G )
	tgbtwncgr.m	|- .- = ( dist ` G )
	tgbtwncgr.i	|- I = ( Itv ` G )
	tgbtwncgr.g	|- ( ph -> G e. TarskiG )
	tgbtwncgr.a	|- ( ph -> A e. P )
	tgbtwncgr.b	|- ( ph -> B e. P )
	tgbtwncgr.c	|- ( ph -> C e. P )
	tgbtwncgr.d	|- ( ph -> D e. P )
	tgcgrsub.e	|- ( ph -> E e. P )
	tgcgrsub.f	|- ( ph -> F e. P )
	tgcgrsub.1	|- ( ph -> B e. ( A I C ) )
	tgcgrsub.2	|- ( ph -> E e. ( D I F ) )
	tgcgrsub.3	|- ( ph -> ( A .- C ) = ( D .- F ) )
	tgcgrsub.4	|- ( ph -> ( B .- C ) = ( E .- F ) )
Assertion	tgcgrsub	|- ( ph -> ( A .- B ) = ( D .- E ) )

Proof

Step	Hyp	Ref	Expression
1		tgbtwncgr.p	|- P = ( Base ` G )
2		tgbtwncgr.m	|- .- = ( dist ` G )
3		tgbtwncgr.i	|- I = ( Itv ` G )
4		tgbtwncgr.g	|- ( ph -> G e. TarskiG )
5		tgbtwncgr.a	|- ( ph -> A e. P )
6		tgbtwncgr.b	|- ( ph -> B e. P )
7		tgbtwncgr.c	|- ( ph -> C e. P )
8		tgbtwncgr.d	|- ( ph -> D e. P )
9		tgcgrsub.e	|- ( ph -> E e. P )
10		tgcgrsub.f	|- ( ph -> F e. P )
11		tgcgrsub.1	|- ( ph -> B e. ( A I C ) )
12		tgcgrsub.2	|- ( ph -> E e. ( D I F ) )
13		tgcgrsub.3	|- ( ph -> ( A .- C ) = ( D .- F ) )
14		tgcgrsub.4	|- ( ph -> ( B .- C ) = ( E .- F ) )
15	1 2 3 4 5 8	tgcgrtriv	|- ( ph -> ( A .- A ) = ( D .- D ) )
16	1 2 3 4 5 7 8 10 13	tgcgrcomlr	|- ( ph -> ( C .- A ) = ( F .- D ) )
17	1 2 3 4 5 6 7 5 8 9 10 8 11 12 13 14 15 16	tgifscgr	|- ( ph -> ( B .- A ) = ( E .- D ) )
18	1 2 3 4 6 5 9 8 17	tgcgrcomlr	|- ( ph -> ( A .- B ) = ( D .- E ) )