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

Metamath Proof Explorer

Theorem ccats1pfxeqbi

Description: A word is a prefix of a word with length greater by 1 than the first word iff the second word is the first word concatenated with the last symbol of the second word. (Contributed by AV, 24-Oct-2018) (Revised by AV, 10-May-2020)

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

Proof

Step Hyp Ref Expression
1 ccats1pfxeq ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( 𝑊 = ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) → 𝑈 = ( 𝑊 ++ ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) ) )
2 simp1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → 𝑊 ∈ Word 𝑉 )
3 lencl ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
4 nn0p1nn ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑊 ) + 1 ) ∈ ℕ )
5 3 4 syl ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑊 ) + 1 ) ∈ ℕ )
6 5 3ad2ant1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( ( ♯ ‘ 𝑊 ) + 1 ) ∈ ℕ )
7 3simpc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) )
8 lswlgt0cl ⊢ ( ( ( ( ♯ ‘ 𝑊 ) + 1 ) ∈ ℕ ∧ ( 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) → ( lastS ‘ 𝑈 ) ∈ 𝑉 )
9 6 7 8 syl2anc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( lastS ‘ 𝑈 ) ∈ 𝑉 )
10 9 s1cld ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ∈ Word 𝑉 )
11 eqidd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) )
12 pfxccatid ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 ++ ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) prefix ( ♯ ‘ 𝑊 ) ) = 𝑊 )
13 12 eqcomd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) ) → 𝑊 = ( ( 𝑊 ++ ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) prefix ( ♯ ‘ 𝑊 ) ) )
14 2 10 11 13 syl3anc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → 𝑊 = ( ( 𝑊 ++ ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) prefix ( ♯ ‘ 𝑊 ) ) )
15 oveq1 ⊢ ( 𝑈 = ( 𝑊 ++ ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) → ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) = ( ( 𝑊 ++ ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) prefix ( ♯ ‘ 𝑊 ) ) )
16 15 eqcomd ⊢ ( 𝑈 = ( 𝑊 ++ ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) → ( ( 𝑊 ++ ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) prefix ( ♯ ‘ 𝑊 ) ) = ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) )
17 14 16 sylan9eq ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ∧ 𝑈 = ( 𝑊 ++ ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) ) → 𝑊 = ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) )
18 17 ex ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( 𝑈 = ( 𝑊 ++ ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) → 𝑊 = ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) ) )
19 1 18 impbid ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( 𝑊 = ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) ↔ 𝑈 = ( 𝑊 ++ ⟨“ ( lastS ‘ 𝑈 ) ”⟩ ) ) )