Theorem ccatrcan

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

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

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( ♯ ‘ 𝐶 ) = ( ♯ ‘ 𝐶 )
2		ccatopth2	⊢ ( ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐶 ∈ Word 𝑋 ) ∧ ( 𝐵 ∈ Word 𝑋 ∧ 𝐶 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐶 ) = ( ♯ ‘ 𝐶 ) ) → ( ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) ↔ ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐶 ) ) )
3	1 2	mp3an3	⊢ ( ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐶 ∈ Word 𝑋 ) ∧ ( 𝐵 ∈ Word 𝑋 ∧ 𝐶 ∈ Word 𝑋 ) ) → ( ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) ↔ ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐶 ) ) )
4	3	3impdir	⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ∧ 𝐶 ∈ Word 𝑋 ) → ( ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) ↔ ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐶 ) ) )
5		eqid	⊢ 𝐶 = 𝐶
6	5	biantru	⊢ ( 𝐴 = 𝐵 ↔ ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐶 ) )
7	4 6	bitr4di	⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ∧ 𝐶 ∈ Word 𝑋 ) → ( ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) ↔ 𝐴 = 𝐵 ) )