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

Metamath Proof Explorer

Theorem ccatopth

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

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

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( ( 𝐴 ++ 𝐵 ) = ( 𝐶 ++ 𝐷 ) → ( ( 𝐴 ++ 𝐵 ) prefix ( ♯ ‘ 𝐴 ) ) = ( ( 𝐶 ++ 𝐷 ) prefix ( ♯ ‘ 𝐴 ) ) )
2 pfxccat1 ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ) → ( ( 𝐴 ++ 𝐵 ) prefix ( ♯ ‘ 𝐴 ) ) = 𝐴 )
3 oveq2 ⊢ ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐶 ) → ( ( 𝐶 ++ 𝐷 ) prefix ( ♯ ‘ 𝐴 ) ) = ( ( 𝐶 ++ 𝐷 ) prefix ( ♯ ‘ 𝐶 ) ) )
4 pfxccat1 ⊢ ( ( 𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋 ) → ( ( 𝐶 ++ 𝐷 ) prefix ( ♯ ‘ 𝐶 ) ) = 𝐶 )
5 3 4 sylan9eqr ⊢ ( ( ( 𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐶 ) ) → ( ( 𝐶 ++ 𝐷 ) prefix ( ♯ ‘ 𝐴 ) ) = 𝐶 )
6 2 5 eqeqan12d ⊢ ( ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ) ∧ ( ( 𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐶 ) ) ) → ( ( ( 𝐴 ++ 𝐵 ) prefix ( ♯ ‘ 𝐴 ) ) = ( ( 𝐶 ++ 𝐷 ) prefix ( ♯ ‘ 𝐴 ) ) ↔ 𝐴 = 𝐶 ) )
7 1 6 imbitrid ⊢ ( ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ) ∧ ( ( 𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐶 ) ) ) → ( ( 𝐴 ++ 𝐵 ) = ( 𝐶 ++ 𝐷 ) → 𝐴 = 𝐶 ) )
8 7 3impb ⊢ ( ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐶 ) ) → ( ( 𝐴 ++ 𝐵 ) = ( 𝐶 ++ 𝐷 ) → 𝐴 = 𝐶 ) )
9 simpr ⊢ ( ( ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐶 ) ) ∧ ( 𝐴 ++ 𝐵 ) = ( 𝐶 ++ 𝐷 ) ) → ( 𝐴 ++ 𝐵 ) = ( 𝐶 ++ 𝐷 ) )
10 simpl3 ⊢ ( ( ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐶 ) ) ∧ ( 𝐴 ++ 𝐵 ) = ( 𝐶 ++ 𝐷 ) ) → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐶 ) )
11 9 fveq2d ⊢ ( ( ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐶 ) ) ∧ ( 𝐴 ++ 𝐵 ) = ( 𝐶 ++ 𝐷 ) ) → ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) = ( ♯ ‘ ( 𝐶 ++ 𝐷 ) ) )
12 simpl1 ⊢ ( ( ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐶 ) ) ∧ ( 𝐴 ++ 𝐵 ) = ( 𝐶 ++ 𝐷 ) ) → ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ) )
13 ccatlen ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ) → ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) )
14 12 13 syl ⊢ ( ( ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐶 ) ) ∧ ( 𝐴 ++ 𝐵 ) = ( 𝐶 ++ 𝐷 ) ) → ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) )
15 simpl2 ⊢ ( ( ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐶 ) ) ∧ ( 𝐴 ++ 𝐵 ) = ( 𝐶 ++ 𝐷 ) ) → ( 𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋 ) )
16 ccatlen ⊢ ( ( 𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋 ) → ( ♯ ‘ ( 𝐶 ++ 𝐷 ) ) = ( ( ♯ ‘ 𝐶 ) + ( ♯ ‘ 𝐷 ) ) )
17 15 16 syl ⊢ ( ( ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐶 ) ) ∧ ( 𝐴 ++ 𝐵 ) = ( 𝐶 ++ 𝐷 ) ) → ( ♯ ‘ ( 𝐶 ++ 𝐷 ) ) = ( ( ♯ ‘ 𝐶 ) + ( ♯ ‘ 𝐷 ) ) )
18 11 14 17 3eqtr3d ⊢ ( ( ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐶 ) ) ∧ ( 𝐴 ++ 𝐵 ) = ( 𝐶 ++ 𝐷 ) ) → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) = ( ( ♯ ‘ 𝐶 ) + ( ♯ ‘ 𝐷 ) ) )
19 10 18 opeq12d ⊢ ( ( ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐶 ) ) ∧ ( 𝐴 ++ 𝐵 ) = ( 𝐶 ++ 𝐷 ) ) → ⟨ ( ♯ ‘ 𝐴 ) , ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ⟩ = ⟨ ( ♯ ‘ 𝐶 ) , ( ( ♯ ‘ 𝐶 ) + ( ♯ ‘ 𝐷 ) ) ⟩ )
20 9 19 oveq12d ⊢ ( ( ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐶 ) ) ∧ ( 𝐴 ++ 𝐵 ) = ( 𝐶 ++ 𝐷 ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ ( ♯ ‘ 𝐴 ) , ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ⟩ ) = ( ( 𝐶 ++ 𝐷 ) substr ⟨ ( ♯ ‘ 𝐶 ) , ( ( ♯ ‘ 𝐶 ) + ( ♯ ‘ 𝐷 ) ) ⟩ ) )
21 swrdccat2 ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ ( ♯ ‘ 𝐴 ) , ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ⟩ ) = 𝐵 )
22 12 21 syl ⊢ ( ( ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐶 ) ) ∧ ( 𝐴 ++ 𝐵 ) = ( 𝐶 ++ 𝐷 ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ ( ♯ ‘ 𝐴 ) , ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ⟩ ) = 𝐵 )
23 swrdccat2 ⊢ ( ( 𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋 ) → ( ( 𝐶 ++ 𝐷 ) substr ⟨ ( ♯ ‘ 𝐶 ) , ( ( ♯ ‘ 𝐶 ) + ( ♯ ‘ 𝐷 ) ) ⟩ ) = 𝐷 )
24 15 23 syl ⊢ ( ( ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐶 ) ) ∧ ( 𝐴 ++ 𝐵 ) = ( 𝐶 ++ 𝐷 ) ) → ( ( 𝐶 ++ 𝐷 ) substr ⟨ ( ♯ ‘ 𝐶 ) , ( ( ♯ ‘ 𝐶 ) + ( ♯ ‘ 𝐷 ) ) ⟩ ) = 𝐷 )
25 20 22 24 3eqtr3d ⊢ ( ( ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐶 ) ) ∧ ( 𝐴 ++ 𝐵 ) = ( 𝐶 ++ 𝐷 ) ) → 𝐵 = 𝐷 )
26 25 ex ⊢ ( ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐶 ) ) → ( ( 𝐴 ++ 𝐵 ) = ( 𝐶 ++ 𝐷 ) → 𝐵 = 𝐷 ) )
27 8 26 jcad ⊢ ( ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐶 ) ) → ( ( 𝐴 ++ 𝐵 ) = ( 𝐶 ++ 𝐷 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
28 oveq12 ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → ( 𝐴 ++ 𝐵 ) = ( 𝐶 ++ 𝐷 ) )
29 27 28 impbid1 ⊢ ( ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ) ∧ ( 𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐶 ) ) → ( ( 𝐴 ++ 𝐵 ) = ( 𝐶 ++ 𝐷 ) ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )