This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑋 ) → ( ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) ↔ 𝐴 = 𝐵 ) )