Metamath Proof Explorer

Theorem ccats1pfxeqrex

Description: There exists a symbol such that its concatenation after the prefix obtained by deleting the last symbol of a nonempty word results in the word itself. (Contributed by AV, 5-Oct-2018) (Revised by AV, 9-May-2020)

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

Proof

Step Hyp Ref Expression
1 simp2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → 𝑈 ∈ Word 𝑉 )
2 lencl ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
3 2 3ad2ant1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
4 nn0p1nn ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑊 ) + 1 ) ∈ ℕ )
5 nngt0 ⊢ ( ( ( ♯ ‘ 𝑊 ) + 1 ) ∈ ℕ → 0 < ( ( ♯ ‘ 𝑊 ) + 1 ) )
6 3 4 5 3syl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → 0 < ( ( ♯ ‘ 𝑊 ) + 1 ) )
7 breq2 ⊢ ( ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) → ( 0 < ( ♯ ‘ 𝑈 ) ↔ 0 < ( ( ♯ ‘ 𝑊 ) + 1 ) ) )
8 7 3ad2ant3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( 0 < ( ♯ ‘ 𝑈 ) ↔ 0 < ( ( ♯ ‘ 𝑊 ) + 1 ) ) )
9 6 8 mpbird ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → 0 < ( ♯ ‘ 𝑈 ) )
10 hashgt0n0 ⊢ ( ( 𝑈 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑈 ) ) → 𝑈 ≠ ∅ )
11 1 9 10 syl2anc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → 𝑈 ≠ ∅ )
12 lswcl ⊢ ( ( 𝑈 ∈ Word 𝑉 ∧ 𝑈 ≠ ∅ ) → ( lastS ‘ 𝑈 ) ∈ 𝑉 )
13 1 11 12 syl2anc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( lastS ‘ 𝑈 ) ∈ 𝑉 )
14 ccats1pfxeq ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( 𝑊 = ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) → 𝑈 = ( 𝑊 ++ ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) ) )
15 s1eq ⊢ ( 𝑠 = ( lastS ‘ 𝑈 ) → ⟨“ 𝑠 ”⟩ = ⟨“ ( lastS ‘ 𝑈 ) ”⟩ )
16 15 oveq2d ⊢ ( 𝑠 = ( lastS ‘ 𝑈 ) → ( 𝑊 ++ ⟨“ 𝑠 ”⟩ ) = ( 𝑊 ++ ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) )
17 16 rspceeqv ⊢ ( ( ( lastS ‘ 𝑈 ) ∈ 𝑉 ∧ 𝑈 = ( 𝑊 ++ ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) ) → ∃ 𝑠 ∈ 𝑉 𝑈 = ( 𝑊 ++ ⟨“ 𝑠 ”⟩ ) )
18 13 14 17 syl6an ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( 𝑊 = ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) → ∃ 𝑠 ∈ 𝑉 𝑈 = ( 𝑊 ++ ⟨“ 𝑠 ”⟩ ) ) )