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 ‘ 𝑈 ) ”⟩ ) ) )