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 
|- ( ( 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 oveq1 
 |-  ( W = ( U prefix ( # ` W ) ) -> ( W ++ <" ( lastS ` U ) "> ) = ( ( U prefix ( # ` W ) ) ++ <" ( lastS ` U ) "> ) )
2 1 adantl 
 |-  ( ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) /\ W = ( U prefix ( # ` W ) ) ) -> ( W ++ <" ( lastS ` U ) "> ) = ( ( U prefix ( # ` W ) ) ++ <" ( lastS ` U ) "> ) )
3 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
4 3 nn0cnd 
 |-  ( W e. Word V -> ( # ` W ) e. CC )
5 pncan1 
 |-  ( ( # ` W ) e. CC -> ( ( ( # ` W ) + 1 ) - 1 ) = ( # ` W ) )
6 4 5 syl 
 |-  ( W e. Word V -> ( ( ( # ` W ) + 1 ) - 1 ) = ( # ` W ) )
7 6 eqcomd 
 |-  ( W e. Word V -> ( # ` W ) = ( ( ( # ` W ) + 1 ) - 1 ) )
8 7 3ad2ant1 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( # ` W ) = ( ( ( # ` W ) + 1 ) - 1 ) )
9 oveq1 
 |-  ( ( # ` U ) = ( ( # ` W ) + 1 ) -> ( ( # ` U ) - 1 ) = ( ( ( # ` W ) + 1 ) - 1 ) )
10 9 eqcomd 
 |-  ( ( # ` U ) = ( ( # ` W ) + 1 ) -> ( ( ( # ` W ) + 1 ) - 1 ) = ( ( # ` U ) - 1 ) )
11 10 3ad2ant3 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( ( ( # ` W ) + 1 ) - 1 ) = ( ( # ` U ) - 1 ) )
12 8 11 eqtrd 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( # ` W ) = ( ( # ` U ) - 1 ) )
13 12 oveq2d 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( U prefix ( # ` W ) ) = ( U prefix ( ( # ` U ) - 1 ) ) )
14 13 oveq1d 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( ( U prefix ( # ` W ) ) ++ <" ( lastS ` U ) "> ) = ( ( U prefix ( ( # ` U ) - 1 ) ) ++ <" ( lastS ` U ) "> ) )
15 simp2 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> U e. Word V )
16 nn0p1gt0 
 |-  ( ( # ` W ) e. NN0 -> 0 < ( ( # ` W ) + 1 ) )
17 3 16 syl 
 |-  ( W e. Word V -> 0 < ( ( # ` W ) + 1 ) )
18 17 3ad2ant1 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> 0 < ( ( # ` W ) + 1 ) )
19 breq2 
 |-  ( ( # ` U ) = ( ( # ` W ) + 1 ) -> ( 0 < ( # ` U ) <-> 0 < ( ( # ` W ) + 1 ) ) )
20 19 3ad2ant3 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( 0 < ( # ` U ) <-> 0 < ( ( # ` W ) + 1 ) ) )
21 18 20 mpbird 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> 0 < ( # ` U ) )
22 hashneq0 
 |-  ( U e. Word V -> ( 0 < ( # ` U ) <-> U =/= (/) ) )
23 22 3ad2ant2 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( 0 < ( # ` U ) <-> U =/= (/) ) )
24 21 23 mpbid 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> U =/= (/) )
25 pfxlswccat 
 |-  ( ( U e. Word V /\ U =/= (/) ) -> ( ( U prefix ( ( # ` U ) - 1 ) ) ++ <" ( lastS ` U ) "> ) = U )
26 15 24 25 syl2anc 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( ( U prefix ( ( # ` U ) - 1 ) ) ++ <" ( lastS ` U ) "> ) = U )
27 14 26 eqtrd 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( ( U prefix ( # ` W ) ) ++ <" ( lastS ` U ) "> ) = U )
28 27 adantr 
 |-  ( ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) /\ W = ( U prefix ( # ` W ) ) ) -> ( ( U prefix ( # ` W ) ) ++ <" ( lastS ` U ) "> ) = U )
29 2 28 eqtr2d 
 |-  ( ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) /\ W = ( U prefix ( # ` W ) ) ) -> U = ( W ++ <" ( lastS ` U ) "> ) )
30 29 ex 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( W = ( U prefix ( # ` W ) ) -> U = ( W ++ <" ( lastS ` U ) "> ) ) )