Metamath Proof Explorer


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 ( 𝜑 → ( 𝐴 𝐵 ) = ( 𝐷 𝐸 ) )