Metamath Proof Explorer

Theorem tgfscgr

Description: Congruence law for the general five segment configuration. Theorem 4.16 of Schwabhauser p. 37. (Contributed by Thierry Arnoux, 27-Apr-2019)

Ref Expression
Hypotheses tglngval.p 
|- P = ( Base ` G )
tglngval.l 
|- L = ( LineG ` G )
tglngval.i 
|- I = ( Itv ` G )
tglngval.g 
|- ( ph -> G e. TarskiG )
tglngval.x 
|- ( ph -> X e. P )
tglngval.y 
|- ( ph -> Y e. P )
tgcolg.z 
|- ( ph -> Z e. P )
lnxfr.r 
|- .~ = ( cgrG ` G )
lnxfr.a 
|- ( ph -> A e. P )
lnxfr.b 
|- ( ph -> B e. P )
lnxfr.d 
|- .- = ( dist ` G )
tgfscgr.t 
|- ( ph -> T e. P )
tgfscgr.c 
|- ( ph -> C e. P )
tgfscgr.d 
|- ( ph -> D e. P )
tgfscgr.1 
|- ( ph -> ( Y e. ( X L Z ) \/ X = Z ) )
tgfscgr.2 
|- ( ph -> <" X Y Z "> .~ <" A B C "> )
tgfscgr.3 
|- ( ph -> ( X .- T ) = ( A .- D ) )
tgfscgr.4 
|- ( ph -> ( Y .- T ) = ( B .- D ) )
tgfscgr.5 
|- ( ph -> X =/= Y )
Assertion tgfscgr 
|- ( ph -> ( Z .- T ) = ( C .- D ) )

Proof

Step Hyp Ref Expression
1 tglngval.p 
 |-  P = ( Base ` G )
2 tglngval.l 
 |-  L = ( LineG ` G )
3 tglngval.i 
 |-  I = ( Itv ` G )
4 tglngval.g 
 |-  ( ph -> G e. TarskiG )
5 tglngval.x 
 |-  ( ph -> X e. P )
6 tglngval.y 
 |-  ( ph -> Y e. P )
7 tgcolg.z 
 |-  ( ph -> Z e. P )
8 lnxfr.r 
 |-  .~ = ( cgrG ` G )
9 lnxfr.a 
 |-  ( ph -> A e. P )
10 lnxfr.b 
 |-  ( ph -> B e. P )
11 lnxfr.d 
 |-  .- = ( dist ` G )
12 tgfscgr.t 
 |-  ( ph -> T e. P )
13 tgfscgr.c 
 |-  ( ph -> C e. P )
14 tgfscgr.d 
 |-  ( ph -> D e. P )
15 tgfscgr.1 
 |-  ( ph -> ( Y e. ( X L Z ) \/ X = Z ) )
16 tgfscgr.2 
 |-  ( ph -> <" X Y Z "> .~ <" A B C "> )
17 tgfscgr.3 
 |-  ( ph -> ( X .- T ) = ( A .- D ) )
18 tgfscgr.4 
 |-  ( ph -> ( Y .- T ) = ( B .- D ) )
19 tgfscgr.5 
 |-  ( ph -> X =/= Y )
20 4 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> G e. TarskiG )
21 5 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> X e. P )
22 6 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> Y e. P )
23 7 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> Z e. P )
24 9 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> A e. P )
25 10 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> B e. P )
26 13 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> C e. P )
27 12 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> T e. P )
28 14 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> D e. P )
29 19 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> X =/= Y )
30 simpr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> Y e. ( X I Z ) )
31 16 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> <" X Y Z "> .~ <" A B C "> )
32 1 11 3 8 20 21 22 23 24 25 26 31 30 tgbtwnxfr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> B e. ( A I C ) )
33 1 11 3 8 20 21 22 23 24 25 26 31 cgr3simp1 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> ( X .- Y ) = ( A .- B ) )
34 1 11 3 8 20 21 22 23 24 25 26 31 cgr3simp2 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> ( Y .- Z ) = ( B .- C ) )
35 17 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> ( X .- T ) = ( A .- D ) )
36 18 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> ( Y .- T ) = ( B .- D ) )
37 1 11 3 20 21 22 23 24 25 26 27 28 29 30 32 33 34 35 36 axtg5seg 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> ( Z .- T ) = ( C .- D ) )
38 4 adantr 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> G e. TarskiG )
39 6 adantr 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> Y e. P )
40 5 adantr 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> X e. P )
41 7 adantr 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> Z e. P )
42 10 adantr 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> B e. P )
43 9 adantr 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> A e. P )
44 13 adantr 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> C e. P )
45 12 adantr 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> T e. P )
46 14 adantr 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> D e. P )
47 19 necomd 
 |-  ( ph -> Y =/= X )
48 47 adantr 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> Y =/= X )
49 simpr 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> X e. ( Y I Z ) )
50 16 adantr 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> <" X Y Z "> .~ <" A B C "> )
51 1 11 3 8 38 40 39 41 43 42 44 50 cgr3swap12 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> <" Y X Z "> .~ <" B A C "> )
52 1 11 3 8 38 39 40 41 42 43 44 51 49 tgbtwnxfr 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> A e. ( B I C ) )
53 1 11 3 8 38 39 40 41 42 43 44 51 cgr3simp1 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> ( Y .- X ) = ( B .- A ) )
54 1 11 3 8 38 39 40 41 42 43 44 51 cgr3simp2 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> ( X .- Z ) = ( A .- C ) )
55 18 adantr 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> ( Y .- T ) = ( B .- D ) )
56 17 adantr 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> ( X .- T ) = ( A .- D ) )
57 1 11 3 38 39 40 41 42 43 44 45 46 48 49 52 53 54 55 56 axtg5seg 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> ( Z .- T ) = ( C .- D ) )
58 4 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> G e. TarskiG )
59 5 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> X e. P )
60 7 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> Z e. P )
61 6 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> Y e. P )
62 12 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> T e. P )
63 9 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> A e. P )
64 13 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> C e. P )
65 10 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> B e. P )
66 14 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> D e. P )
67 simpr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> Z e. ( X I Y ) )
68 16 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> <" X Y Z "> .~ <" A B C "> )
69 1 11 3 8 58 59 61 60 63 65 64 68 cgr3swap23 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> <" X Z Y "> .~ <" A C B "> )
70 1 11 3 8 58 59 60 61 63 64 65 69 67 tgbtwnxfr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> C e. ( A I B ) )
71 1 11 3 8 58 59 61 60 63 65 64 68 cgr3simp1 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> ( X .- Y ) = ( A .- B ) )
72 1 11 3 8 58 59 60 61 63 64 65 69 cgr3simp2 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> ( Z .- Y ) = ( C .- B ) )
73 17 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> ( X .- T ) = ( A .- D ) )
74 18 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> ( Y .- T ) = ( B .- D ) )
75 1 11 3 58 59 60 61 62 63 64 65 66 67 70 71 72 73 74 tgifscgr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> ( Z .- T ) = ( C .- D ) )
76 1 2 3 4 5 7 6 tgcolg 
 |-  ( ph -> ( ( Y e. ( X L Z ) \/ X = Z ) <-> ( Y e. ( X I Z ) \/ X e. ( Y I Z ) \/ Z e. ( X I Y ) ) ) )
77 15 76 mpbid 
 |-  ( ph -> ( Y e. ( X I Z ) \/ X e. ( Y I Z ) \/ Z e. ( X I Y ) ) )
78 37 57 75 77 mpjao3dan 
 |-  ( ph -> ( Z .- T ) = ( C .- D ) )