# Metamath Proof Explorer

## Theorem cgrsub

Description: Removing identical parts from the end of a line segment preserves congruence. Theorem 4.3 of Schwabhauser p. 35. (Contributed by Scott Fenton, 4-Oct-2013)

Ref Expression
Assertion cgrsub ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\to \left(\left(\left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {E}\mathrm{Btwn}⟨{D},{F}⟩\right)\wedge \left(⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to ⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\right)$

### Proof

Step Hyp Ref Expression
1 simprl ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {E}\mathrm{Btwn}⟨{D},{F}⟩\right)\wedge \left(⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\right)\to \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {E}\mathrm{Btwn}⟨{D},{F}⟩\right)$
2 simprr ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {E}\mathrm{Btwn}⟨{D},{F}⟩\right)\wedge \left(⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\right)\to \left(⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)$
3 simpl1 ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {E}\mathrm{Btwn}⟨{D},{F}⟩\right)\wedge \left(⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\right)\to {N}\in ℕ$
4 simpl21 ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {E}\mathrm{Btwn}⟨{D},{F}⟩\right)\wedge \left(⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\right)\to {A}\in 𝔼\left({N}\right)$
5 simpl31 ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {E}\mathrm{Btwn}⟨{D},{F}⟩\right)\wedge \left(⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\right)\to {D}\in 𝔼\left({N}\right)$
6 cgrtriv ${⊢}\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\to ⟨{A},{A}⟩\mathrm{Cgr}⟨{D},{D}⟩$
7 3 4 5 6 syl3anc ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {E}\mathrm{Btwn}⟨{D},{F}⟩\right)\wedge \left(⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\right)\to ⟨{A},{A}⟩\mathrm{Cgr}⟨{D},{D}⟩$
8 simprrl ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {E}\mathrm{Btwn}⟨{D},{F}⟩\right)\wedge \left(⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\right)\to ⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩$
9 simpl23 ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {E}\mathrm{Btwn}⟨{D},{F}⟩\right)\wedge \left(⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\right)\to {C}\in 𝔼\left({N}\right)$
10 simpl33 ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {E}\mathrm{Btwn}⟨{D},{F}⟩\right)\wedge \left(⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\right)\to {F}\in 𝔼\left({N}\right)$
11 cgrcomlr ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩↔⟨{C},{A}⟩\mathrm{Cgr}⟨{F},{D}⟩\right)$
12 3 4 9 5 10 11 syl122anc ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {E}\mathrm{Btwn}⟨{D},{F}⟩\right)\wedge \left(⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\right)\to \left(⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩↔⟨{C},{A}⟩\mathrm{Cgr}⟨{F},{D}⟩\right)$
13 8 12 mpbid ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {E}\mathrm{Btwn}⟨{D},{F}⟩\right)\wedge \left(⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\right)\to ⟨{C},{A}⟩\mathrm{Cgr}⟨{F},{D}⟩$
14 7 13 jca ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {E}\mathrm{Btwn}⟨{D},{F}⟩\right)\wedge \left(⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\right)\to \left(⟨{A},{A}⟩\mathrm{Cgr}⟨{D},{D}⟩\wedge ⟨{C},{A}⟩\mathrm{Cgr}⟨{F},{D}⟩\right)$
15 simpl22 ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {E}\mathrm{Btwn}⟨{D},{F}⟩\right)\wedge \left(⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\right)\to {B}\in 𝔼\left({N}\right)$
16 simpl32 ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {E}\mathrm{Btwn}⟨{D},{F}⟩\right)\wedge \left(⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\right)\to {E}\in 𝔼\left({N}\right)$
17 brifs ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {A}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\wedge \left({E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨⟨{A},{B}⟩,⟨{C},{A}⟩⟩\mathrm{InnerFiveSeg}⟨⟨{D},{E}⟩,⟨{F},{D}⟩⟩↔\left(\left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {E}\mathrm{Btwn}⟨{D},{F}⟩\right)\wedge \left(⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\wedge \left(⟨{A},{A}⟩\mathrm{Cgr}⟨{D},{D}⟩\wedge ⟨{C},{A}⟩\mathrm{Cgr}⟨{F},{D}⟩\right)\right)\right)$
18 ifscgr ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {A}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\wedge \left({E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨⟨{A},{B}⟩,⟨{C},{A}⟩⟩\mathrm{InnerFiveSeg}⟨⟨{D},{E}⟩,⟨{F},{D}⟩⟩\to ⟨{B},{A}⟩\mathrm{Cgr}⟨{E},{D}⟩\right)$
19 17 18 sylbird ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {A}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\wedge \left({E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\to \left(\left(\left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {E}\mathrm{Btwn}⟨{D},{F}⟩\right)\wedge \left(⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\wedge \left(⟨{A},{A}⟩\mathrm{Cgr}⟨{D},{D}⟩\wedge ⟨{C},{A}⟩\mathrm{Cgr}⟨{F},{D}⟩\right)\right)\to ⟨{B},{A}⟩\mathrm{Cgr}⟨{E},{D}⟩\right)$
20 3 4 15 9 4 5 16 10 5 19 syl333anc ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {E}\mathrm{Btwn}⟨{D},{F}⟩\right)\wedge \left(⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\right)\to \left(\left(\left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {E}\mathrm{Btwn}⟨{D},{F}⟩\right)\wedge \left(⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\wedge \left(⟨{A},{A}⟩\mathrm{Cgr}⟨{D},{D}⟩\wedge ⟨{C},{A}⟩\mathrm{Cgr}⟨{F},{D}⟩\right)\right)\to ⟨{B},{A}⟩\mathrm{Cgr}⟨{E},{D}⟩\right)$
21 1 2 14 20 mp3and ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {E}\mathrm{Btwn}⟨{D},{F}⟩\right)\wedge \left(⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\right)\to ⟨{B},{A}⟩\mathrm{Cgr}⟨{E},{D}⟩$
22 cgrcomlr ${⊢}\left({N}\in ℕ\wedge \left({B}\in 𝔼\left({N}\right)\wedge {A}\in 𝔼\left({N}\right)\right)\wedge \left({E}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{B},{A}⟩\mathrm{Cgr}⟨{E},{D}⟩↔⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\right)$
23 3 15 4 16 5 22 syl122anc ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {E}\mathrm{Btwn}⟨{D},{F}⟩\right)\wedge \left(⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\right)\to \left(⟨{B},{A}⟩\mathrm{Cgr}⟨{E},{D}⟩↔⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\right)$
24 21 23 mpbid ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {E}\mathrm{Btwn}⟨{D},{F}⟩\right)\wedge \left(⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\right)\to ⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩$
25 24 ex ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\to \left(\left(\left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {E}\mathrm{Btwn}⟨{D},{F}⟩\right)\wedge \left(⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)\to ⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\right)$