Metamath Proof Explorer


Theorem tgifscgr

Description: Inner five segment congruence. Take two triangles, A D C and E H K , with B between A and C and F between E and K . If the other components of the triangles are congruent, then so are B D and F H . Theorem 4.2 of Schwabhauser p. 34. (Contributed by Thierry Arnoux, 24-Mar-2019)

Ref Expression
Hypotheses tgbtwncgr.p P=BaseG
tgbtwncgr.m -˙=distG
tgbtwncgr.i I=ItvG
tgbtwncgr.g φG𝒢Tarski
tgbtwncgr.a φAP
tgbtwncgr.b φBP
tgbtwncgr.c φCP
tgbtwncgr.d φDP
tgifscgr.e φEP
tgifscgr.f φFP
tgifscgr.g φKP
tgifscgr.h φHP
tgifscgr.1 φBAIC
tgifscgr.2 φFEIK
tgifscgr.3 φA-˙C=E-˙K
tgifscgr.4 φB-˙C=F-˙K
tgifscgr.5 φA-˙D=E-˙H
tgifscgr.6 φC-˙D=K-˙H
Assertion tgifscgr φB-˙D=F-˙H

Proof

Step Hyp Ref Expression
1 tgbtwncgr.p P=BaseG
2 tgbtwncgr.m -˙=distG
3 tgbtwncgr.i I=ItvG
4 tgbtwncgr.g φG𝒢Tarski
5 tgbtwncgr.a φAP
6 tgbtwncgr.b φBP
7 tgbtwncgr.c φCP
8 tgbtwncgr.d φDP
9 tgifscgr.e φEP
10 tgifscgr.f φFP
11 tgifscgr.g φKP
12 tgifscgr.h φHP
13 tgifscgr.1 φBAIC
14 tgifscgr.2 φFEIK
15 tgifscgr.3 φA-˙C=E-˙K
16 tgifscgr.4 φB-˙C=F-˙K
17 tgifscgr.5 φA-˙D=E-˙H
18 tgifscgr.6 φC-˙D=K-˙H
19 4 adantr φP=1G𝒢Tarski
20 6 adantr φP=1BP
21 8 adantr φP=1DP
22 10 adantr φP=1FP
23 simpr φP=1P=1
24 12 adantr φP=1HP
25 1 2 3 19 20 21 22 23 24 tgldim0cgr φP=1B-˙D=F-˙H
26 18 ad2antrr φ2PA=CC-˙D=K-˙H
27 4 ad2antrr φ2PA=CG𝒢Tarski
28 7 ad2antrr φ2PA=CCP
29 6 ad2antrr φ2PA=CBP
30 13 ad2antrr φ2PA=CBAIC
31 simpr φ2PA=CA=C
32 31 oveq1d φ2PA=CAIC=CIC
33 30 32 eleqtrd φ2PA=CBCIC
34 1 2 3 27 28 29 33 axtgbtwnid φ2PA=CC=B
35 34 oveq1d φ2PA=CC-˙D=B-˙D
36 11 ad2antrr φ2PA=CKP
37 10 ad2antrr φ2PA=CFP
38 14 ad2antrr φ2PA=CFEIK
39 9 ad2antrr φ2PA=CEP
40 5 ad2antrr φ2PA=CAP
41 31 oveq2d φ2PA=CA-˙A=A-˙C
42 15 ad2antrr φ2PA=CA-˙C=E-˙K
43 41 42 eqtr2d φ2PA=CE-˙K=A-˙A
44 1 2 3 27 39 36 40 43 axtgcgrid φ2PA=CE=K
45 44 oveq1d φ2PA=CEIK=KIK
46 38 45 eleqtrd φ2PA=CFKIK
47 1 2 3 27 36 37 46 axtgbtwnid φ2PA=CK=F
48 47 oveq1d φ2PA=CK-˙H=F-˙H
49 26 35 48 3eqtr3d φ2PA=CB-˙D=F-˙H
50 4 ad2antrr φ2PACG𝒢Tarski
51 50 ad2antrr φ2PACePCAIeCeG𝒢Tarski
52 51 ad2antrr φ2PACePCAIeCefPKEIfK-˙f=C-˙eG𝒢Tarski
53 simp-4r φ2PACePCAIeCefPKEIfK-˙f=C-˙eeP
54 7 ad2antrr φ2PACCP
55 54 ad2antrr φ2PACePCAIeCeCP
56 55 ad2antrr φ2PACePCAIeCefPKEIfK-˙f=C-˙eCP
57 6 ad6antr φ2PACePCAIeCefPKEIfK-˙f=C-˙eBP
58 simplr φ2PACePCAIeCefPKEIfK-˙f=C-˙efP
59 11 ad4antr φ2PACePCAIeCeKP
60 59 ad2antrr φ2PACePCAIeCefPKEIfK-˙f=C-˙eKP
61 10 ad6antr φ2PACePCAIeCefPKEIfK-˙f=C-˙eFP
62 8 ad6antr φ2PACePCAIeCefPKEIfK-˙f=C-˙eDP
63 12 ad6antr φ2PACePCAIeCefPKEIfK-˙f=C-˙eHP
64 simpllr φ2PACePCAIeCefPKEIfK-˙f=C-˙eCAIeCe
65 64 simprd φ2PACePCAIeCefPKEIfK-˙f=C-˙eCe
66 65 necomd φ2PACePCAIeCefPKEIfK-˙f=C-˙eeC
67 5 ad2antrr φ2PACAP
68 67 ad4antr φ2PACePCAIeCefPKEIfK-˙f=C-˙eAP
69 13 ad6antr φ2PACePCAIeCefPKEIfK-˙f=C-˙eBAIC
70 64 simpld φ2PACePCAIeCefPKEIfK-˙f=C-˙eCAIe
71 1 2 3 52 68 57 56 53 69 70 tgbtwnexch3 φ2PACePCAIeCefPKEIfK-˙f=C-˙eCBIe
72 1 2 3 52 57 56 53 71 tgbtwncom φ2PACePCAIeCefPKEIfK-˙f=C-˙eCeIB
73 9 ad6antr φ2PACePCAIeCefPKEIfK-˙f=C-˙eEP
74 14 ad6antr φ2PACePCAIeCefPKEIfK-˙f=C-˙eFEIK
75 simprl φ2PACePCAIeCefPKEIfK-˙f=C-˙eKEIf
76 1 2 3 52 73 61 60 58 74 75 tgbtwnexch3 φ2PACePCAIeCefPKEIfK-˙f=C-˙eKFIf
77 1 2 3 52 61 60 58 76 tgbtwncom φ2PACePCAIeCefPKEIfK-˙f=C-˙eKfIF
78 simprr φ2PACePCAIeCefPKEIfK-˙f=C-˙eK-˙f=C-˙e
79 78 eqcomd φ2PACePCAIeCefPKEIfK-˙f=C-˙eC-˙e=K-˙f
80 1 2 3 52 56 53 60 58 79 tgcgrcomlr φ2PACePCAIeCefPKEIfK-˙f=C-˙ee-˙C=f-˙K
81 16 ad6antr φ2PACePCAIeCefPKEIfK-˙f=C-˙eB-˙C=F-˙K
82 1 2 3 52 57 56 61 60 81 tgcgrcomlr φ2PACePCAIeCefPKEIfK-˙f=C-˙eC-˙B=K-˙F
83 simp-5r φ2PACePCAIeCefPKEIfK-˙f=C-˙eAC
84 15 ad6antr φ2PACePCAIeCefPKEIfK-˙f=C-˙eA-˙C=E-˙K
85 17 ad6antr φ2PACePCAIeCefPKEIfK-˙f=C-˙eA-˙D=E-˙H
86 18 ad6antr φ2PACePCAIeCefPKEIfK-˙f=C-˙eC-˙D=K-˙H
87 1 2 3 52 68 56 53 73 60 58 62 63 83 70 75 84 79 85 86 axtg5seg φ2PACePCAIeCefPKEIfK-˙f=C-˙ee-˙D=f-˙H
88 1 2 3 52 53 56 57 58 60 61 62 63 66 72 77 80 82 87 86 axtg5seg φ2PACePCAIeCefPKEIfK-˙f=C-˙eB-˙D=F-˙H
89 9 ad4antr φ2PACePCAIeCeEP
90 simplr φ2PACePCAIeCeeP
91 1 2 3 51 89 59 55 90 axtgsegcon φ2PACePCAIeCefPKEIfK-˙f=C-˙e
92 88 91 r19.29a φ2PACePCAIeCeB-˙D=F-˙H
93 simplr φ2PAC2P
94 1 2 3 50 67 54 93 tgbtwndiff φ2PACePCAIeCe
95 92 94 r19.29a φ2PACB-˙D=F-˙H
96 49 95 pm2.61dane φ2PB-˙D=F-˙H
97 1 5 tgldimor φP=12P
98 25 96 97 mpjaodan φB-˙D=F-˙H