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 imbitrid ⊢ ( ( ( 𝐴 ∈ 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 𝑋 ) ∧ ( ♯ ‘ 𝐵 ) = ( ♯ ‘ 𝐷 ) ) → ( ( 𝐴 ++ 𝐵 ) = ( 𝐶 ++ 𝐷 ) ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )