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 
|- ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( W = ( U prefix ( # ` W ) ) <-> U = ( W ++ <" ( lastS ` U ) "> ) ) )

Proof

Step Hyp Ref Expression
1 ccats1pfxeq 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( W = ( U prefix ( # ` W ) ) -> U = ( W ++ <" ( lastS ` U ) "> ) ) )
2 simp1 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> W e. Word V )
3 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
4 nn0p1nn 
 |-  ( ( # ` W ) e. NN0 -> ( ( # ` W ) + 1 ) e. NN )
5 3 4 syl 
 |-  ( W e. Word V -> ( ( # ` W ) + 1 ) e. NN )
6 5 3ad2ant1 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( ( # ` W ) + 1 ) e. NN )
7 3simpc 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) )
8 lswlgt0cl 
 |-  ( ( ( ( # ` W ) + 1 ) e. NN /\ ( U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) ) -> ( lastS ` U ) e. V )
9 6 7 8 syl2anc 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( lastS ` U ) e. V )
10 9 s1cld 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> <" ( lastS ` U ) "> e. Word V )
11 eqidd 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( # ` W ) = ( # ` W ) )
12 pfxccatid 
 |-  ( ( W e. Word V /\ <" ( lastS ` U ) "> e. Word V /\ ( # ` W ) = ( # ` W ) ) -> ( ( W ++ <" ( lastS ` U ) "> ) prefix ( # ` W ) ) = W )
13 12 eqcomd 
 |-  ( ( W e. Word V /\ <" ( lastS ` U ) "> e. Word V /\ ( # ` W ) = ( # ` W ) ) -> W = ( ( W ++ <" ( lastS ` U ) "> ) prefix ( # ` W ) ) )
14 2 10 11 13 syl3anc 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> W = ( ( W ++ <" ( lastS ` U ) "> ) prefix ( # ` W ) ) )
15 oveq1 
 |-  ( U = ( W ++ <" ( lastS ` U ) "> ) -> ( U prefix ( # ` W ) ) = ( ( W ++ <" ( lastS ` U ) "> ) prefix ( # ` W ) ) )
16 15 eqcomd 
 |-  ( U = ( W ++ <" ( lastS ` U ) "> ) -> ( ( W ++ <" ( lastS ` U ) "> ) prefix ( # ` W ) ) = ( U prefix ( # ` W ) ) )
17 14 16 sylan9eq 
 |-  ( ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) /\ U = ( W ++ <" ( lastS ` U ) "> ) ) -> W = ( U prefix ( # ` W ) ) )
18 17 ex 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( U = ( W ++ <" ( lastS ` U ) "> ) -> W = ( U prefix ( # ` W ) ) ) )
19 1 18 impbid 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( W = ( U prefix ( # ` W ) ) <-> U = ( W ++ <" ( lastS ` U ) "> ) ) )