# Metamath Proof Explorer

## Theorem ccatopth2

Description: An opth -like theorem for recovering the two halves of a concatenated word. (Contributed by Mario Carneiro, 1-Oct-2015)

Ref Expression
Assertion ccatopth2 ( ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐵 ) = ( ♯ ‘ 𝐷 ) ) → ( ( 𝐴 ++ 𝐵 ) = ( 𝐶 ++ 𝐷 ) ↔ ( 𝐴 = 𝐶𝐵 = 𝐷 ) ) )

### Proof

Step Hyp Ref Expression
1 fveq2 ( ( 𝐴 ++ 𝐵 ) = ( 𝐶 ++ 𝐷 ) → ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) = ( ♯ ‘ ( 𝐶 ++ 𝐷 ) ) )
2 ccatlen ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑋 ) → ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) )
3 2 3ad2ant1 ( ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐵 ) = ( ♯ ‘ 𝐷 ) ) → ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) )
4 simp3 ( ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐵 ) = ( ♯ ‘ 𝐷 ) ) → ( ♯ ‘ 𝐵 ) = ( ♯ ‘ 𝐷 ) )
5 4 oveq2d ( ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐵 ) = ( ♯ ‘ 𝐷 ) ) → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐷 ) ) )
6 3 5 eqtrd ( ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐵 ) = ( ♯ ‘ 𝐷 ) ) → ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐷 ) ) )
7 ccatlen ( ( 𝐶 ∈ Word 𝑋𝐷 ∈ Word 𝑋 ) → ( ♯ ‘ ( 𝐶 ++ 𝐷 ) ) = ( ( ♯ ‘ 𝐶 ) + ( ♯ ‘ 𝐷 ) ) )
8 7 3ad2ant2 ( ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐵 ) = ( ♯ ‘ 𝐷 ) ) → ( ♯ ‘ ( 𝐶 ++ 𝐷 ) ) = ( ( ♯ ‘ 𝐶 ) + ( ♯ ‘ 𝐷 ) ) )
9 6 8 eqeq12d ( ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐵 ) = ( ♯ ‘ 𝐷 ) ) → ( ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) = ( ♯ ‘ ( 𝐶 ++ 𝐷 ) ) ↔ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐷 ) ) = ( ( ♯ ‘ 𝐶 ) + ( ♯ ‘ 𝐷 ) ) ) )
10 simp1l ( ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐵 ) = ( ♯ ‘ 𝐷 ) ) → 𝐴 ∈ Word 𝑋 )
11 lencl ( 𝐴 ∈ Word 𝑋 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
12 10 11 syl ( ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐵 ) = ( ♯ ‘ 𝐷 ) ) → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
13 12 nn0cnd ( ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐵 ) = ( ♯ ‘ 𝐷 ) ) → ( ♯ ‘ 𝐴 ) ∈ ℂ )
14 simp2l ( ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐵 ) = ( ♯ ‘ 𝐷 ) ) → 𝐶 ∈ Word 𝑋 )
15 lencl ( 𝐶 ∈ Word 𝑋 → ( ♯ ‘ 𝐶 ) ∈ ℕ0 )
16 14 15 syl ( ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐵 ) = ( ♯ ‘ 𝐷 ) ) → ( ♯ ‘ 𝐶 ) ∈ ℕ0 )
17 16 nn0cnd ( ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐵 ) = ( ♯ ‘ 𝐷 ) ) → ( ♯ ‘ 𝐶 ) ∈ ℂ )
18 simp2r ( ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐵 ) = ( ♯ ‘ 𝐷 ) ) → 𝐷 ∈ Word 𝑋 )
19 lencl ( 𝐷 ∈ Word 𝑋 → ( ♯ ‘ 𝐷 ) ∈ ℕ0 )
20 18 19 syl ( ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐵 ) = ( ♯ ‘ 𝐷 ) ) → ( ♯ ‘ 𝐷 ) ∈ ℕ0 )
21 20 nn0cnd ( ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐵 ) = ( ♯ ‘ 𝐷 ) ) → ( ♯ ‘ 𝐷 ) ∈ ℂ )
22 13 17 21 addcan2d ( ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐵 ) = ( ♯ ‘ 𝐷 ) ) → ( ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐷 ) ) = ( ( ♯ ‘ 𝐶 ) + ( ♯ ‘ 𝐷 ) ) ↔ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐶 ) ) )
23 9 22 bitrd ( ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐵 ) = ( ♯ ‘ 𝐷 ) ) → ( ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) = ( ♯ ‘ ( 𝐶 ++ 𝐷 ) ) ↔ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐶 ) ) )
24 1 23 syl5ib ( ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐵 ) = ( ♯ ‘ 𝐷 ) ) → ( ( 𝐴 ++ 𝐵 ) = ( 𝐶 ++ 𝐷 ) → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐶 ) ) )
25 ccatopth ( ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐶 ) ) → ( ( 𝐴 ++ 𝐵 ) = ( 𝐶 ++ 𝐷 ) ↔ ( 𝐴 = 𝐶𝐵 = 𝐷 ) ) )
26 25 biimpd ( ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐶 ) ) → ( ( 𝐴 ++ 𝐵 ) = ( 𝐶 ++ 𝐷 ) → ( 𝐴 = 𝐶𝐵 = 𝐷 ) ) )
27 26 3expia ( ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋𝐷 ∈ Word 𝑋 ) ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐶 ) → ( ( 𝐴 ++ 𝐵 ) = ( 𝐶 ++ 𝐷 ) → ( 𝐴 = 𝐶𝐵 = 𝐷 ) ) ) )
28 27 com23 ( ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋𝐷 ∈ Word 𝑋 ) ) → ( ( 𝐴 ++ 𝐵 ) = ( 𝐶 ++ 𝐷 ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐶 ) → ( 𝐴 = 𝐶𝐵 = 𝐷 ) ) ) )
29 28 3adant3 ( ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐵 ) = ( ♯ ‘ 𝐷 ) ) → ( ( 𝐴 ++ 𝐵 ) = ( 𝐶 ++ 𝐷 ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐶 ) → ( 𝐴 = 𝐶𝐵 = 𝐷 ) ) ) )
30 24 29 mpdd ( ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐵 ) = ( ♯ ‘ 𝐷 ) ) → ( ( 𝐴 ++ 𝐵 ) = ( 𝐶 ++ 𝐷 ) → ( 𝐴 = 𝐶𝐵 = 𝐷 ) ) )
31 oveq12 ( ( 𝐴 = 𝐶𝐵 = 𝐷 ) → ( 𝐴 ++ 𝐵 ) = ( 𝐶 ++ 𝐷 ) )
32 30 31 impbid1 ( ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐵 ) = ( ♯ ‘ 𝐷 ) ) → ( ( 𝐴 ++ 𝐵 ) = ( 𝐶 ++ 𝐷 ) ↔ ( 𝐴 = 𝐶𝐵 = 𝐷 ) ) )