Metamath Proof Explorer

Theorem tgcgrextend

Description: Link congruence over a pair of line segments. Theorem 2.11 of Schwabhauser p. 29. (Contributed by Thierry Arnoux, 23-Mar-2019) (Shortened by David A. Wheeler and Thierry Arnoux, 22-Apr-2020.)

Ref Expression
Hypotheses tkgeom.p 
|- P = ( Base ` G )
tkgeom.d 
|- .- = ( dist ` G )
tkgeom.i 
|- I = ( Itv ` G )
tkgeom.g 
|- ( ph -> G e. TarskiG )
tgcgrextend.a 
|- ( ph -> A e. P )
tgcgrextend.b 
|- ( ph -> B e. P )
tgcgrextend.c 
|- ( ph -> C e. P )
tgcgrextend.d 
|- ( ph -> D e. P )
tgcgrextend.e 
|- ( ph -> E e. P )
tgcgrextend.f 
|- ( ph -> F e. P )
tgcgrextend.1 
|- ( ph -> B e. ( A I C ) )
tgcgrextend.2 
|- ( ph -> E e. ( D I F ) )
tgcgrextend.3 
|- ( ph -> ( A .- B ) = ( D .- E ) )
tgcgrextend.4 
|- ( ph -> ( B .- C ) = ( E .- F ) )
Assertion tgcgrextend 
|- ( ph -> ( A .- C ) = ( D .- F ) )

Proof

Step Hyp Ref Expression
1 tkgeom.p 
 |-  P = ( Base ` G )
2 tkgeom.d 
 |-  .- = ( dist ` G )
3 tkgeom.i 
 |-  I = ( Itv ` G )
4 tkgeom.g 
 |-  ( ph -> G e. TarskiG )
5 tgcgrextend.a 
 |-  ( ph -> A e. P )
6 tgcgrextend.b 
 |-  ( ph -> B e. P )
7 tgcgrextend.c 
 |-  ( ph -> C e. P )
8 tgcgrextend.d 
 |-  ( ph -> D e. P )
9 tgcgrextend.e 
 |-  ( ph -> E e. P )
10 tgcgrextend.f 
 |-  ( ph -> F e. P )
11 tgcgrextend.1 
 |-  ( ph -> B e. ( A I C ) )
12 tgcgrextend.2 
 |-  ( ph -> E e. ( D I F ) )
13 tgcgrextend.3 
 |-  ( ph -> ( A .- B ) = ( D .- E ) )
14 tgcgrextend.4 
 |-  ( ph -> ( B .- C ) = ( E .- F ) )
15 14 adantr 
 |-  ( ( ph /\ A = B ) -> ( B .- C ) = ( E .- F ) )
16 simpr 
 |-  ( ( ph /\ A = B ) -> A = B )
17 16 oveq1d 
 |-  ( ( ph /\ A = B ) -> ( A .- C ) = ( B .- C ) )
18 4 adantr 
 |-  ( ( ph /\ A = B ) -> G e. TarskiG )
19 5 adantr 
 |-  ( ( ph /\ A = B ) -> A e. P )
20 6 adantr 
 |-  ( ( ph /\ A = B ) -> B e. P )
21 8 adantr 
 |-  ( ( ph /\ A = B ) -> D e. P )
22 9 adantr 
 |-  ( ( ph /\ A = B ) -> E e. P )
23 13 adantr 
 |-  ( ( ph /\ A = B ) -> ( A .- B ) = ( D .- E ) )
24 1 2 3 18 19 20 21 22 23 16 tgcgreq 
 |-  ( ( ph /\ A = B ) -> D = E )
25 24 oveq1d 
 |-  ( ( ph /\ A = B ) -> ( D .- F ) = ( E .- F ) )
26 15 17 25 3eqtr4d 
 |-  ( ( ph /\ A = B ) -> ( A .- C ) = ( D .- F ) )
27 4 adantr 
 |-  ( ( ph /\ A =/= B ) -> G e. TarskiG )
28 7 adantr 
 |-  ( ( ph /\ A =/= B ) -> C e. P )
29 5 adantr 
 |-  ( ( ph /\ A =/= B ) -> A e. P )
30 10 adantr 
 |-  ( ( ph /\ A =/= B ) -> F e. P )
31 8 adantr 
 |-  ( ( ph /\ A =/= B ) -> D e. P )
32 6 adantr 
 |-  ( ( ph /\ A =/= B ) -> B e. P )
33 9 adantr 
 |-  ( ( ph /\ A =/= B ) -> E e. P )
34 simpr 
 |-  ( ( ph /\ A =/= B ) -> A =/= B )
35 11 adantr 
 |-  ( ( ph /\ A =/= B ) -> B e. ( A I C ) )
36 12 adantr 
 |-  ( ( ph /\ A =/= B ) -> E e. ( D I F ) )
37 13 adantr 
 |-  ( ( ph /\ A =/= B ) -> ( A .- B ) = ( D .- E ) )
38 14 adantr 
 |-  ( ( ph /\ A =/= B ) -> ( B .- C ) = ( E .- F ) )
39 1 2 3 27 29 31 tgcgrtriv 
 |-  ( ( ph /\ A =/= B ) -> ( A .- A ) = ( D .- D ) )
40 1 2 3 27 29 32 31 33 37 tgcgrcomlr 
 |-  ( ( ph /\ A =/= B ) -> ( B .- A ) = ( E .- D ) )
41 1 2 3 27 29 32 28 31 33 30 29 31 34 35 36 37 38 39 40 axtg5seg 
 |-  ( ( ph /\ A =/= B ) -> ( C .- A ) = ( F .- D ) )
42 1 2 3 27 28 29 30 31 41 tgcgrcomlr 
 |-  ( ( ph /\ A =/= B ) -> ( A .- C ) = ( D .- F ) )
43 26 42 pm2.61dane 
 |-  ( ph -> ( A .- C ) = ( D .- F ) )