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 = ( hlG ` G )
tghlsub.h 
|- ( ph -> G e. TarskiG )
tghlsub.1 
|- ( ph -> B e. P )
tghlsub.2 
|- ( ph -> E e. P )
tghlsub.3 
|- ( ph -> A ( K ` B ) C )
tghlsub.4 
|- ( ph -> D ( K ` E ) F )
tghlsub.5 
|- ( ph -> ( B .- C ) = ( E .- F ) )
tghlsub.6 
|- ( ph -> ( B .- A ) = ( E .- D ) )
Assertion tghlsub 
|- ( ph -> ( C .- A ) = ( F .- D ) )

Proof

Step Hyp Ref Expression
1 tghlsub.p 
 |-  P = ( Base ` G )
2 tghlsub.d 
 |-  .- = ( dist ` G )
3 tghlsub.k 
 |-  K = ( hlG ` G )
4 tghlsub.h 
 |-  ( ph -> G e. TarskiG )
5 tghlsub.1 
 |-  ( ph -> B e. P )
6 tghlsub.2 
 |-  ( ph -> E e. P )
7 tghlsub.3 
 |-  ( ph -> A ( K ` B ) C )
8 tghlsub.4 
 |-  ( ph -> D ( K ` E ) F )
9 tghlsub.5 
 |-  ( ph -> ( B .- C ) = ( E .- F ) )
10 tghlsub.6 
 |-  ( ph -> ( B .- A ) = ( E .- D ) )
11 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
12 eqid 
 |-  ( leG ` G ) = ( leG ` G )
13 1 11 3 4 5 7 hlgrcl2 
 |-  ( ph -> C e. P )
14 1 11 3 4 5 7 hlgrcl1 
 |-  ( ph -> A e. P )
15 1 11 3 4 6 8 hlgrcl2 
 |-  ( ph -> F e. P )
16 1 11 3 4 6 8 hlgrcl1 
 |-  ( ph -> D e. P )
17 1 11 3 14 13 5 4 ishlg 
 |-  ( ph -> ( A ( K ` B ) C <-> ( A =/= B /\ C =/= B /\ ( A e. ( B ( Itv ` G ) C ) \/ C e. ( B ( Itv ` G ) A ) ) ) ) )
18 7 17 mpbid 
 |-  ( ph -> ( A =/= B /\ C =/= B /\ ( A e. ( B ( Itv ` G ) C ) \/ C e. ( B ( Itv ` G ) A ) ) ) )
19 18 simp3d 
 |-  ( ph -> ( A e. ( B ( Itv ` G ) C ) \/ C e. ( B ( Itv ` G ) A ) ) )
20 19 orcomd 
 |-  ( ph -> ( C e. ( B ( Itv ` G ) A ) \/ A e. ( B ( Itv ` G ) C ) ) )
21 1 11 3 16 15 6 4 ishlg 
 |-  ( ph -> ( D ( K ` E ) F <-> ( D =/= E /\ F =/= E /\ ( D e. ( E ( Itv ` G ) F ) \/ F e. ( E ( Itv ` G ) D ) ) ) ) )
22 8 21 mpbid 
 |-  ( ph -> ( D =/= E /\ F =/= E /\ ( D e. ( E ( Itv ` G ) F ) \/ F e. ( E ( Itv ` G ) D ) ) ) )
23 22 simp3d 
 |-  ( ph -> ( D e. ( E ( Itv ` G ) F ) \/ F e. ( E ( Itv ` G ) D ) ) )
24 23 orcomd 
 |-  ( ph -> ( F e. ( E ( Itv ` G ) D ) \/ D e. ( E ( Itv ` G ) F ) ) )
25 1 2 11 12 4 5 13 14 6 6 15 16 20 24 9 10 tgcgrsub2 
 |-  ( ph -> ( C .- A ) = ( F .- D ) )