Metamath Proof Explorer


Theorem ccatcan2d

Description: Cancellation law for concatenation. (Contributed by SN, 6-Sep-2023)

Ref Expression
Hypotheses ccatcan2d.a φAWordV
ccatcan2d.b φBWordV
ccatcan2d.c φCWordV
Assertion ccatcan2d φA++C=B++CA=B

Proof

Step Hyp Ref Expression
1 ccatcan2d.a φAWordV
2 ccatcan2d.b φBWordV
3 ccatcan2d.c φCWordV
4 simpr φA++C=B++CA++C=B++C
5 lencl AWordVA0
6 1 5 syl φA0
7 6 nn0cnd φA
8 7 adantr φA++C=B++CA
9 lencl BWordVB0
10 2 9 syl φB0
11 10 nn0cnd φB
12 11 adantr φA++C=B++CB
13 lencl CWordVC0
14 3 13 syl φC0
15 14 nn0cnd φC
16 15 adantr φA++C=B++CC
17 ccatlen AWordVCWordVA++C=A+C
18 1 3 17 syl2anc φA++C=A+C
19 fveq2 A++C=B++CA++C=B++C
20 18 19 sylan9req φA++C=B++CA+C=B++C
21 ccatlen BWordVCWordVB++C=B+C
22 2 3 21 syl2anc φB++C=B+C
23 22 adantr φA++C=B++CB++C=B+C
24 20 23 eqtrd φA++C=B++CA+C=B+C
25 8 12 16 24 addcan2ad φA++C=B++CA=B
26 4 25 oveq12d φA++C=B++CA++CprefixA=B++CprefixB
27 26 ex φA++C=B++CA++CprefixA=B++CprefixB
28 pfxccat1 AWordVCWordVA++CprefixA=A
29 1 3 28 syl2anc φA++CprefixA=A
30 pfxccat1 BWordVCWordVB++CprefixB=B
31 2 3 30 syl2anc φB++CprefixB=B
32 29 31 eqeq12d φA++CprefixA=B++CprefixBA=B
33 27 32 sylibd φA++C=B++CA=B
34 oveq1 A=BA++C=B++C
35 33 34 impbid1 φA++C=B++CA=B