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

Metamath Proof Explorer

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