Metamath Proof Explorer


Theorem tgcgreqb

Description: Congruence and equality. (Contributed by Thierry Arnoux, 27-Aug-2019)

Ref Expression
Hypotheses tkgeom.p P=BaseG
tkgeom.d -˙=distG
tkgeom.i I=ItvG
tkgeom.g φG𝒢Tarski
tgcgrcomlr.a φAP
tgcgrcomlr.b φBP
tgcgrcomlr.c φCP
tgcgrcomlr.d φDP
tgcgrcomlr.6 φA-˙B=C-˙D
Assertion tgcgreqb φA=BC=D

Proof

Step Hyp Ref Expression
1 tkgeom.p P=BaseG
2 tkgeom.d -˙=distG
3 tkgeom.i I=ItvG
4 tkgeom.g φG𝒢Tarski
5 tgcgrcomlr.a φAP
6 tgcgrcomlr.b φBP
7 tgcgrcomlr.c φCP
8 tgcgrcomlr.d φDP
9 tgcgrcomlr.6 φA-˙B=C-˙D
10 4 adantr φA=BG𝒢Tarski
11 7 adantr φA=BCP
12 8 adantr φA=BDP
13 6 adantr φA=BBP
14 9 adantr φA=BA-˙B=C-˙D
15 simpr φA=BA=B
16 15 oveq1d φA=BA-˙B=B-˙B
17 14 16 eqtr3d φA=BC-˙D=B-˙B
18 1 2 3 10 11 12 13 17 axtgcgrid φA=BC=D
19 4 adantr φC=DG𝒢Tarski
20 5 adantr φC=DAP
21 6 adantr φC=DBP
22 8 adantr φC=DDP
23 9 adantr φC=DA-˙B=C-˙D
24 simpr φC=DC=D
25 24 oveq1d φC=DC-˙D=D-˙D
26 23 25 eqtrd φC=DA-˙B=D-˙D
27 1 2 3 19 20 21 22 26 axtgcgrid φC=DA=B
28 18 27 impbida φA=BC=D