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 ⊢ 𝑃 = ( Base ‘ 𝐺 )
tghlsub.d ⊢ − = ( dist ‘ 𝐺 )
tghlsub.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
tghlsub.h ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tghlsub.1 ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
tghlsub.2 ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
tghlsub.3 ⊢ ( 𝜑 → 𝐴 ( 𝐾 ‘ 𝐵 ) 𝐶 )
tghlsub.4 ⊢ ( 𝜑 → 𝐷 ( 𝐾 ‘ 𝐸 ) 𝐹 )
tghlsub.5 ⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) )
tghlsub.6 ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) = ( 𝐸 − 𝐷 ) )
Assertion tghlsub ( 𝜑 → ( 𝐶 − 𝐴 ) = ( 𝐹 − 𝐷 ) )

Proof

Step Hyp Ref Expression
1 tghlsub.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tghlsub.d ⊢ − = ( dist ‘ 𝐺 )
3 tghlsub.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
4 tghlsub.h ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 tghlsub.1 ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
6 tghlsub.2 ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
7 tghlsub.3 ⊢ ( 𝜑 → 𝐴 ( 𝐾 ‘ 𝐵 ) 𝐶 )
8 tghlsub.4 ⊢ ( 𝜑 → 𝐷 ( 𝐾 ‘ 𝐸 ) 𝐹 )
9 tghlsub.5 ⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) )
10 tghlsub.6 ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) = ( 𝐸 − 𝐷 ) )
11 eqid ⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
12 eqid ⊢ ( ≤G ‘ 𝐺 ) = ( ≤G ‘ 𝐺 )
13 1 11 3 4 5 7 hlgrcl2 ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
14 1 11 3 4 5 7 hlgrcl1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
15 1 11 3 4 6 8 hlgrcl2 ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
16 1 11 3 4 6 8 hlgrcl1 ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
17 1 11 3 14 13 5 4 ishlg ⊢ ( 𝜑 → ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝐶 ↔ ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ ( 𝐴 ∈ ( 𝐵 ( Itv ‘ 𝐺 ) 𝐶 ) ∨ 𝐶 ∈ ( 𝐵 ( Itv ‘ 𝐺 ) 𝐴 ) ) ) ) )
18 7 17 mpbid ⊢ ( 𝜑 → ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ ( 𝐴 ∈ ( 𝐵 ( Itv ‘ 𝐺 ) 𝐶 ) ∨ 𝐶 ∈ ( 𝐵 ( Itv ‘ 𝐺 ) 𝐴 ) ) ) )
19 18 simp3d ⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐵 ( Itv ‘ 𝐺 ) 𝐶 ) ∨ 𝐶 ∈ ( 𝐵 ( Itv ‘ 𝐺 ) 𝐴 ) ) )
20 19 orcomd ⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐵 ( Itv ‘ 𝐺 ) 𝐴 ) ∨ 𝐴 ∈ ( 𝐵 ( Itv ‘ 𝐺 ) 𝐶 ) ) )
21 1 11 3 16 15 6 4 ishlg ⊢ ( 𝜑 → ( 𝐷 ( 𝐾 ‘ 𝐸 ) 𝐹 ↔ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ∧ ( 𝐷 ∈ ( 𝐸 ( Itv ‘ 𝐺 ) 𝐹 ) ∨ 𝐹 ∈ ( 𝐸 ( Itv ‘ 𝐺 ) 𝐷 ) ) ) ) )
22 8 21 mpbid ⊢ ( 𝜑 → ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ∧ ( 𝐷 ∈ ( 𝐸 ( Itv ‘ 𝐺 ) 𝐹 ) ∨ 𝐹 ∈ ( 𝐸 ( Itv ‘ 𝐺 ) 𝐷 ) ) ) )
23 22 simp3d ⊢ ( 𝜑 → ( 𝐷 ∈ ( 𝐸 ( Itv ‘ 𝐺 ) 𝐹 ) ∨ 𝐹 ∈ ( 𝐸 ( Itv ‘ 𝐺 ) 𝐷 ) ) )
24 23 orcomd ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐸 ( Itv ‘ 𝐺 ) 𝐷 ) ∨ 𝐷 ∈ ( 𝐸 ( Itv ‘ 𝐺 ) 𝐹 ) ) )
25 1 2 11 12 4 5 13 14 6 6 15 16 20 24 9 10 tgcgrsub2 ⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) = ( 𝐹 − 𝐷 ) )