Description: Cancellation law for concatenation. (Contributed by SN, 6-Sep-2023)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ccatcan2d.a | |
|
ccatcan2d.b | |
||
ccatcan2d.c | |
||
Assertion | ccatcan2d | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ccatcan2d.a | |
|
2 | ccatcan2d.b | |
|
3 | ccatcan2d.c | |
|
4 | simpr | |
|
5 | lencl | |
|
6 | 1 5 | syl | |
7 | 6 | nn0cnd | |
8 | 7 | adantr | |
9 | lencl | |
|
10 | 2 9 | syl | |
11 | 10 | nn0cnd | |
12 | 11 | adantr | |
13 | lencl | |
|
14 | 3 13 | syl | |
15 | 14 | nn0cnd | |
16 | 15 | adantr | |
17 | ccatlen | |
|
18 | 1 3 17 | syl2anc | |
19 | fveq2 | |
|
20 | 18 19 | sylan9req | |
21 | ccatlen | |
|
22 | 2 3 21 | syl2anc | |
23 | 22 | adantr | |
24 | 20 23 | eqtrd | |
25 | 8 12 16 24 | addcan2ad | |
26 | 4 25 | oveq12d | |
27 | 26 | ex | |
28 | pfxccat1 | |
|
29 | 1 3 28 | syl2anc | |
30 | pfxccat1 | |
|
31 | 2 3 30 | syl2anc | |
32 | 29 31 | eqeq12d | |
33 | 27 32 | sylibd | |
34 | oveq1 | |
|
35 | 33 34 | impbid1 | |