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