Theorem ccatcan2d

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

	Ref	Expression
Hypotheses	ccatcan2d.a	⊢ ( 𝜑 → 𝐴 ∈ Word 𝑉 )
	ccatcan2d.b	⊢ ( 𝜑 → 𝐵 ∈ Word 𝑉 )
	ccatcan2d.c	⊢ ( 𝜑 → 𝐶 ∈ Word 𝑉 )
Assertion	ccatcan2d	⊢ ( 𝜑 → ( ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) ↔ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ccatcan2d.a	⊢ ( 𝜑 → 𝐴 ∈ Word 𝑉 )
2		ccatcan2d.b	⊢ ( 𝜑 → 𝐵 ∈ Word 𝑉 )
3		ccatcan2d.c	⊢ ( 𝜑 → 𝐶 ∈ Word 𝑉 )
4		simpr	⊢ ( ( 𝜑 ∧ ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) ) → ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) )
5		lencl	⊢ ( 𝐴 ∈ Word 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
6	1 5	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
7	6	nn0cnd	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℂ )
8	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) ) → ( ♯ ‘ 𝐴 ) ∈ ℂ )
9		lencl	⊢ ( 𝐵 ∈ Word 𝑉 → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
10	2 9	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
11	10	nn0cnd	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℂ )
12	11	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) ) → ( ♯ ‘ 𝐵 ) ∈ ℂ )
13		lencl	⊢ ( 𝐶 ∈ Word 𝑉 → ( ♯ ‘ 𝐶 ) ∈ ℕ0 )
14	3 13	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝐶 ) ∈ ℕ0 )
15	14	nn0cnd	⊢ ( 𝜑 → ( ♯ ‘ 𝐶 ) ∈ ℂ )
16	15	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) ) → ( ♯ ‘ 𝐶 ) ∈ ℂ )
17		ccatlen	⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐶 ∈ Word 𝑉 ) → ( ♯ ‘ ( 𝐴 ++ 𝐶 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐶 ) ) )
18	1 3 17	syl2anc	⊢ ( 𝜑 → ( ♯ ‘ ( 𝐴 ++ 𝐶 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐶 ) ) )
19		fveq2	⊢ ( ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) → ( ♯ ‘ ( 𝐴 ++ 𝐶 ) ) = ( ♯ ‘ ( 𝐵 ++ 𝐶 ) ) )
20	18 19	sylan9req	⊢ ( ( 𝜑 ∧ ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) ) → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐶 ) ) = ( ♯ ‘ ( 𝐵 ++ 𝐶 ) ) )
21		ccatlen	⊢ ( ( 𝐵 ∈ Word 𝑉 ∧ 𝐶 ∈ Word 𝑉 ) → ( ♯ ‘ ( 𝐵 ++ 𝐶 ) ) = ( ( ♯ ‘ 𝐵 ) + ( ♯ ‘ 𝐶 ) ) )
22	2 3 21	syl2anc	⊢ ( 𝜑 → ( ♯ ‘ ( 𝐵 ++ 𝐶 ) ) = ( ( ♯ ‘ 𝐵 ) + ( ♯ ‘ 𝐶 ) ) )
23	22	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) ) → ( ♯ ‘ ( 𝐵 ++ 𝐶 ) ) = ( ( ♯ ‘ 𝐵 ) + ( ♯ ‘ 𝐶 ) ) )
24	20 23	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) ) → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐶 ) ) = ( ( ♯ ‘ 𝐵 ) + ( ♯ ‘ 𝐶 ) ) )
25	8 12 16 24	addcan2ad	⊢ ( ( 𝜑 ∧ ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) ) → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) )
26	4 25	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) ) → ( ( 𝐴 ++ 𝐶 ) prefix ( ♯ ‘ 𝐴 ) ) = ( ( 𝐵 ++ 𝐶 ) prefix ( ♯ ‘ 𝐵 ) ) )
27	26	ex	⊢ ( 𝜑 → ( ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) → ( ( 𝐴 ++ 𝐶 ) prefix ( ♯ ‘ 𝐴 ) ) = ( ( 𝐵 ++ 𝐶 ) prefix ( ♯ ‘ 𝐵 ) ) ) )
28		pfxccat1	⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐶 ∈ Word 𝑉 ) → ( ( 𝐴 ++ 𝐶 ) prefix ( ♯ ‘ 𝐴 ) ) = 𝐴 )
29	1 3 28	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 ++ 𝐶 ) prefix ( ♯ ‘ 𝐴 ) ) = 𝐴 )
30		pfxccat1	⊢ ( ( 𝐵 ∈ Word 𝑉 ∧ 𝐶 ∈ Word 𝑉 ) → ( ( 𝐵 ++ 𝐶 ) prefix ( ♯ ‘ 𝐵 ) ) = 𝐵 )
31	2 3 30	syl2anc	⊢ ( 𝜑 → ( ( 𝐵 ++ 𝐶 ) prefix ( ♯ ‘ 𝐵 ) ) = 𝐵 )
32	29 31	eqeq12d	⊢ ( 𝜑 → ( ( ( 𝐴 ++ 𝐶 ) prefix ( ♯ ‘ 𝐴 ) ) = ( ( 𝐵 ++ 𝐶 ) prefix ( ♯ ‘ 𝐵 ) ) ↔ 𝐴 = 𝐵 ) )
33	27 32	sylibd	⊢ ( 𝜑 → ( ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) → 𝐴 = 𝐵 ) )
34		oveq1	⊢ ( 𝐴 = 𝐵 → ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) )
35	33 34	impbid1	⊢ ( 𝜑 → ( ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) ↔ 𝐴 = 𝐵 ) )