Theorem ccatlcan

Description: Concatenation of words is left-cancellative. (Contributed by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Assertion	ccatlcan	⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ∧ 𝐶 ∈ Word 𝑋 ) → ( ( 𝐶 ++ 𝐴 ) = ( 𝐶 ++ 𝐵 ) ↔ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( ♯ ‘ 𝐶 ) = ( ♯ ‘ 𝐶 )
2		ccatopth	⊢ ( ( ( 𝐶 ∈ Word 𝑋 ∧ 𝐴 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐶 ) = ( ♯ ‘ 𝐶 ) ) → ( ( 𝐶 ++ 𝐴 ) = ( 𝐶 ++ 𝐵 ) ↔ ( 𝐶 = 𝐶 ∧ 𝐴 = 𝐵 ) ) )
3	1 2	mp3an3	⊢ ( ( ( 𝐶 ∈ Word 𝑋 ∧ 𝐴 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ) ) → ( ( 𝐶 ++ 𝐴 ) = ( 𝐶 ++ 𝐵 ) ↔ ( 𝐶 = 𝐶 ∧ 𝐴 = 𝐵 ) ) )
4	3	3impdi	⊢ ( ( 𝐶 ∈ Word 𝑋 ∧ 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ) → ( ( 𝐶 ++ 𝐴 ) = ( 𝐶 ++ 𝐵 ) ↔ ( 𝐶 = 𝐶 ∧ 𝐴 = 𝐵 ) ) )
5	4	3coml	⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ∧ 𝐶 ∈ Word 𝑋 ) → ( ( 𝐶 ++ 𝐴 ) = ( 𝐶 ++ 𝐵 ) ↔ ( 𝐶 = 𝐶 ∧ 𝐴 = 𝐵 ) ) )
6		eqid	⊢ 𝐶 = 𝐶
7	6	biantrur	⊢ ( 𝐴 = 𝐵 ↔ ( 𝐶 = 𝐶 ∧ 𝐴 = 𝐵 ) )
8	5 7	bitr4di	⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ∧ 𝐶 ∈ Word 𝑋 ) → ( ( 𝐶 ++ 𝐴 ) = ( 𝐶 ++ 𝐵 ) ↔ 𝐴 = 𝐵 ) )