Metamath Proof Explorer

Theorem tghlsub

Description: Removing identical parts from the end of a ray segment preserves congruence. (Contributed by Thierry Arnoux, 23-Aug-2026)

Ref Expression
Hypotheses tghlsub.p ⊢ P = Base G
tghlsub.d ⊢ - ˙ = dist ⁡ G
tghlsub.k ⊢ K = hl 𝒢 ⁡ G
tghlsub.h ⊢ φ → G ∈ 𝒢 Tarski
tghlsub.1 ⊢ φ → B ∈ P
tghlsub.2 ⊢ φ → E ∈ P
tghlsub.3 ⊢ φ → A K ⁡ B C
tghlsub.4 ⊢ φ → D K ⁡ E F
tghlsub.5 ⊢ φ → B - ˙ C = E - ˙ F
tghlsub.6 ⊢ φ → B - ˙ A = E - ˙ D
Assertion tghlsub ⊢ φ → C - ˙ A = F - ˙ D

Proof

Step Hyp Ref Expression
1 tghlsub.p ⊢ P = Base G
2 tghlsub.d ⊢ - ˙ = dist ⁡ G
3 tghlsub.k ⊢ K = hl 𝒢 ⁡ G
4 tghlsub.h ⊢ φ → G ∈ 𝒢 Tarski
5 tghlsub.1 ⊢ φ → B ∈ P
6 tghlsub.2 ⊢ φ → E ∈ P
7 tghlsub.3 ⊢ φ → A K ⁡ B C
8 tghlsub.4 ⊢ φ → D K ⁡ E F
9 tghlsub.5 ⊢ φ → B - ˙ C = E - ˙ F
10 tghlsub.6 ⊢ φ → B - ˙ A = E - ˙ D
11 eqid ⊢ Itv ⁡ G = Itv ⁡ G
12 eqid ⊢ ≤ 𝒢 ⁡ G = ≤ 𝒢 ⁡ G
13 1 11 3 4 5 7 hlgrcl2 ⊢ φ → C ∈ P
14 1 11 3 4 5 7 hlgrcl1 ⊢ φ → A ∈ P
15 1 11 3 4 6 8 hlgrcl2 ⊢ φ → F ∈ P
16 1 11 3 4 6 8 hlgrcl1 ⊢ φ → D ∈ P
17 1 11 3 14 13 5 4 ishlg ⊢ φ → A K ⁡ B C ↔ A ≠ B ∧ C ≠ B ∧ A ∈ B Itv ⁡ G C ∨ C ∈ B Itv ⁡ G A
18 7 17 mpbid ⊢ φ → A ≠ B ∧ C ≠ B ∧ A ∈ B Itv ⁡ G C ∨ C ∈ B Itv ⁡ G A
19 18 simp3d ⊢ φ → A ∈ B Itv ⁡ G C ∨ C ∈ B Itv ⁡ G A
20 19 orcomd ⊢ φ → C ∈ B Itv ⁡ G A ∨ A ∈ B Itv ⁡ G C
21 1 11 3 16 15 6 4 ishlg ⊢ φ → D K ⁡ E F ↔ D ≠ E ∧ F ≠ E ∧ D ∈ E Itv ⁡ G F ∨ F ∈ E Itv ⁡ G D
22 8 21 mpbid ⊢ φ → D ≠ E ∧ F ≠ E ∧ D ∈ E Itv ⁡ G F ∨ F ∈ E Itv ⁡ G D
23 22 simp3d ⊢ φ → D ∈ E Itv ⁡ G F ∨ F ∈ E Itv ⁡ G D
24 23 orcomd ⊢ φ → F ∈ E Itv ⁡ G D ∨ D ∈ E Itv ⁡ G F
25 1 2 11 12 4 5 13 14 6 6 15 16 20 24 9 10 tgcgrsub2 ⊢ φ → C - ˙ A = F - ˙ D