Metamath Proof Explorer

Theorem ccats1pfxeq

Description: The last symbol of a word concatenated with the word with the last symbol removed results in the word itself. (Contributed by Alexander van der Vekens, 24-Oct-2018) (Revised by AV, 9-May-2020)

Ref Expression
Assertion ccats1pfxeq ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( 𝑊 = ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) → 𝑈 = ( 𝑊 ++ ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝑊 = ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) → ( 𝑊 ++ ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) = ( ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) ++ ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) )
2 1 adantl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ∧ 𝑊 = ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ++ ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) = ( ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) ++ ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) )
3 lencl ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
4 3 nn0cnd ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℂ )
5 pncan1 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℂ → ( ( ( ♯ ‘ 𝑊 ) + 1 ) − 1 ) = ( ♯ ‘ 𝑊 ) )
6 4 5 syl ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ( ♯ ‘ 𝑊 ) + 1 ) − 1 ) = ( ♯ ‘ 𝑊 ) )
7 6 eqcomd ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) = ( ( ( ♯ ‘ 𝑊 ) + 1 ) − 1 ) )
8 7 3ad2ant1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( ♯ ‘ 𝑊 ) = ( ( ( ♯ ‘ 𝑊 ) + 1 ) − 1 ) )
9 oveq1 ⊢ ( ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) → ( ( ♯ ‘ 𝑈 ) − 1 ) = ( ( ( ♯ ‘ 𝑊 ) + 1 ) − 1 ) )
10 9 eqcomd ⊢ ( ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) → ( ( ( ♯ ‘ 𝑊 ) + 1 ) − 1 ) = ( ( ♯ ‘ 𝑈 ) − 1 ) )
11 10 3ad2ant3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( ( ( ♯ ‘ 𝑊 ) + 1 ) − 1 ) = ( ( ♯ ‘ 𝑈 ) − 1 ) )
12 8 11 eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( ♯ ‘ 𝑊 ) = ( ( ♯ ‘ 𝑈 ) − 1 ) )
13 12 oveq2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) = ( 𝑈 prefix ( ( ♯ ‘ 𝑈 ) − 1 ) ) )
14 13 oveq1d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) ++ ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) = ( ( 𝑈 prefix ( ( ♯ ‘ 𝑈 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) )
15 simp2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → 𝑈 ∈ Word 𝑉 )
16 nn0p1gt0 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → 0 < ( ( ♯ ‘ 𝑊 ) + 1 ) )
17 3 16 syl ⊢ ( 𝑊 ∈ Word 𝑉 → 0 < ( ( ♯ ‘ 𝑊 ) + 1 ) )
18 17 3ad2ant1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → 0 < ( ( ♯ ‘ 𝑊 ) + 1 ) )
19 breq2 ⊢ ( ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) → ( 0 < ( ♯ ‘ 𝑈 ) ↔ 0 < ( ( ♯ ‘ 𝑊 ) + 1 ) ) )
20 19 3ad2ant3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( 0 < ( ♯ ‘ 𝑈 ) ↔ 0 < ( ( ♯ ‘ 𝑊 ) + 1 ) ) )
21 18 20 mpbird ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → 0 < ( ♯ ‘ 𝑈 ) )
22 hashneq0 ⊢ ( 𝑈 ∈ Word 𝑉 → ( 0 < ( ♯ ‘ 𝑈 ) ↔ 𝑈 ≠ ∅ ) )
23 22 3ad2ant2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( 0 < ( ♯ ‘ 𝑈 ) ↔ 𝑈 ≠ ∅ ) )
24 21 23 mpbid ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → 𝑈 ≠ ∅ )
25 pfxlswccat ⊢ ( ( 𝑈 ∈ Word 𝑉 ∧ 𝑈 ≠ ∅ ) → ( ( 𝑈 prefix ( ( ♯ ‘ 𝑈 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) = 𝑈 )
26 15 24 25 syl2anc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( ( 𝑈 prefix ( ( ♯ ‘ 𝑈 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) = 𝑈 )
27 14 26 eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) ++ ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) = 𝑈 )
28 27 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ∧ 𝑊 = ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) ++ ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) = 𝑈 )
29 2 28 eqtr2d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ∧ 𝑊 = ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) ) → 𝑈 = ( 𝑊 ++ ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) )
30 29 ex ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( 𝑊 = ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) → 𝑈 = ( 𝑊 ++ ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) ) )