Theorem ccatcan2d

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

	Ref	Expression
Hypotheses	ccatcan2d.a	|- ( ph -> A e. Word V )
	ccatcan2d.b	|- ( ph -> B e. Word V )
	ccatcan2d.c	|- ( ph -> C e. Word V )
Assertion	ccatcan2d	|- ( ph -> ( ( A ++ C ) = ( B ++ C ) <-> A = B ) )

Proof

Step	Hyp	Ref	Expression
1		ccatcan2d.a	|- ( ph -> A e. Word V )
2		ccatcan2d.b	|- ( ph -> B e. Word V )
3		ccatcan2d.c	|- ( ph -> C e. Word V )
4		simpr	|- ( ( ph /\ ( A ++ C ) = ( B ++ C ) ) -> ( A ++ C ) = ( B ++ C ) )
5		lencl	|- ( A e. Word V -> ( # ` A ) e. NN0 )
6	1 5	syl	|- ( ph -> ( # ` A ) e. NN0 )
7	6	nn0cnd	|- ( ph -> ( # ` A ) e. CC )
8	7	adantr	|- ( ( ph /\ ( A ++ C ) = ( B ++ C ) ) -> ( # ` A ) e. CC )
9		lencl	|- ( B e. Word V -> ( # ` B ) e. NN0 )
10	2 9	syl	|- ( ph -> ( # ` B ) e. NN0 )
11	10	nn0cnd	|- ( ph -> ( # ` B ) e. CC )
12	11	adantr	|- ( ( ph /\ ( A ++ C ) = ( B ++ C ) ) -> ( # ` B ) e. CC )
13		lencl	|- ( C e. Word V -> ( # ` C ) e. NN0 )
14	3 13	syl	|- ( ph -> ( # ` C ) e. NN0 )
15	14	nn0cnd	|- ( ph -> ( # ` C ) e. CC )
16	15	adantr	|- ( ( ph /\ ( A ++ C ) = ( B ++ C ) ) -> ( # ` C ) e. CC )
17		ccatlen	|- ( ( A e. Word V /\ C e. Word V ) -> ( # ` ( A ++ C ) ) = ( ( # ` A ) + ( # ` C ) ) )
18	1 3 17	syl2anc	|- ( ph -> ( # ` ( A ++ C ) ) = ( ( # ` A ) + ( # ` C ) ) )
19		fveq2	|- ( ( A ++ C ) = ( B ++ C ) -> ( # ` ( A ++ C ) ) = ( # ` ( B ++ C ) ) )
20	18 19	sylan9req	|- ( ( ph /\ ( A ++ C ) = ( B ++ C ) ) -> ( ( # ` A ) + ( # ` C ) ) = ( # ` ( B ++ C ) ) )
21		ccatlen	|- ( ( B e. Word V /\ C e. Word V ) -> ( # ` ( B ++ C ) ) = ( ( # ` B ) + ( # ` C ) ) )
22	2 3 21	syl2anc	|- ( ph -> ( # ` ( B ++ C ) ) = ( ( # ` B ) + ( # ` C ) ) )
23	22	adantr	|- ( ( ph /\ ( A ++ C ) = ( B ++ C ) ) -> ( # ` ( B ++ C ) ) = ( ( # ` B ) + ( # ` C ) ) )
24	20 23	eqtrd	|- ( ( ph /\ ( A ++ C ) = ( B ++ C ) ) -> ( ( # ` A ) + ( # ` C ) ) = ( ( # ` B ) + ( # ` C ) ) )
25	8 12 16 24	addcan2ad	|- ( ( ph /\ ( A ++ C ) = ( B ++ C ) ) -> ( # ` A ) = ( # ` B ) )
26	4 25	oveq12d	|- ( ( ph /\ ( A ++ C ) = ( B ++ C ) ) -> ( ( A ++ C ) prefix ( # ` A ) ) = ( ( B ++ C ) prefix ( # ` B ) ) )
27	26	ex	|- ( ph -> ( ( A ++ C ) = ( B ++ C ) -> ( ( A ++ C ) prefix ( # ` A ) ) = ( ( B ++ C ) prefix ( # ` B ) ) ) )
28		pfxccat1	|- ( ( A e. Word V /\ C e. Word V ) -> ( ( A ++ C ) prefix ( # ` A ) ) = A )
29	1 3 28	syl2anc	|- ( ph -> ( ( A ++ C ) prefix ( # ` A ) ) = A )
30		pfxccat1	|- ( ( B e. Word V /\ C e. Word V ) -> ( ( B ++ C ) prefix ( # ` B ) ) = B )
31	2 3 30	syl2anc	|- ( ph -> ( ( B ++ C ) prefix ( # ` B ) ) = B )
32	29 31	eqeq12d	|- ( ph -> ( ( ( A ++ C ) prefix ( # ` A ) ) = ( ( B ++ C ) prefix ( # ` B ) ) <-> A = B ) )
33	27 32	sylibd	|- ( ph -> ( ( A ++ C ) = ( B ++ C ) -> A = B ) )
34		oveq1	|- ( A = B -> ( A ++ C ) = ( B ++ C ) )
35	33 34	impbid1	|- ( ph -> ( ( A ++ C ) = ( B ++ C ) <-> A = B ) )