Metamath Proof Explorer

Theorem lpadright

Description: The suffix of a left-padded word the original word W . (Contributed by Thierry Arnoux, 7-Aug-2023)

Ref Expression
Hypotheses lpadlen.1 
|- ( ph -> L e. NN0 )
lpadlen.2 
|- ( ph -> W e. Word S )
lpadlen.3 
|- ( ph -> C e. S )
lpadright.1 
|- ( ph -> M = if ( L <_ ( # ` W ) , 0 , ( L - ( # ` W ) ) ) )
lpadright.2 
|- ( ph -> N e. ( 0 ..^ ( # ` W ) ) )
Assertion lpadright 
|- ( ph -> ( ( ( C leftpad W ) ` L ) ` ( N + M ) ) = ( W ` N ) )

Proof

Step Hyp Ref Expression
1 lpadlen.1 
 |-  ( ph -> L e. NN0 )
2 lpadlen.2 
 |-  ( ph -> W e. Word S )
3 lpadlen.3 
 |-  ( ph -> C e. S )
4 lpadright.1 
 |-  ( ph -> M = if ( L <_ ( # ` W ) , 0 , ( L - ( # ` W ) ) ) )
5 lpadright.2 
 |-  ( ph -> N e. ( 0 ..^ ( # ` W ) ) )
6 1 2 3 lpadval 
 |-  ( ph -> ( ( C leftpad W ) ` L ) = ( ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ++ W ) )
7 6 fveq1d 
 |-  ( ph -> ( ( ( C leftpad W ) ` L ) ` ( N + M ) ) = ( ( ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ++ W ) ` ( N + M ) ) )
8 eqeq2 
 |-  ( 0 = if ( L <_ ( # ` W ) , 0 , ( L - ( # ` W ) ) ) -> ( ( # ` ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ) = 0 <-> ( # ` ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ) = if ( L <_ ( # ` W ) , 0 , ( L - ( # ` W ) ) ) ) )
9 eqeq2 
 |-  ( ( L - ( # ` W ) ) = if ( L <_ ( # ` W ) , 0 , ( L - ( # ` W ) ) ) -> ( ( # ` ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ) = ( L - ( # ` W ) ) <-> ( # ` ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ) = if ( L <_ ( # ` W ) , 0 , ( L - ( # ` W ) ) ) ) )
10 1 adantr 
 |-  ( ( ph /\ L <_ ( # ` W ) ) -> L e. NN0 )
11 2 adantr 
 |-  ( ( ph /\ L <_ ( # ` W ) ) -> W e. Word S )
12 3 adantr 
 |-  ( ( ph /\ L <_ ( # ` W ) ) -> C e. S )
13 simpr 
 |-  ( ( ph /\ L <_ ( # ` W ) ) -> L <_ ( # ` W ) )
14 10 11 12 13 lpadlem3 
 |-  ( ( ph /\ L <_ ( # ` W ) ) -> ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) = (/) )
15 14 fveq2d 
 |-  ( ( ph /\ L <_ ( # ` W ) ) -> ( # ` ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ) = ( # ` (/) ) )
16 hash0 
 |-  ( # ` (/) ) = 0
17 15 16 eqtrdi 
 |-  ( ( ph /\ L <_ ( # ` W ) ) -> ( # ` ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ) = 0 )
18 1 adantr 
 |-  ( ( ph /\ -. L <_ ( # ` W ) ) -> L e. NN0 )
19 2 adantr 
 |-  ( ( ph /\ -. L <_ ( # ` W ) ) -> W e. Word S )
20 3 adantr 
 |-  ( ( ph /\ -. L <_ ( # ` W ) ) -> C e. S )
21 lencl 
 |-  ( W e. Word S -> ( # ` W ) e. NN0 )
22 2 21 syl 
 |-  ( ph -> ( # ` W ) e. NN0 )
23 22 nn0red 
 |-  ( ph -> ( # ` W ) e. RR )
24 23 adantr 
 |-  ( ( ph /\ -. L <_ ( # ` W ) ) -> ( # ` W ) e. RR )
25 1 nn0red 
 |-  ( ph -> L e. RR )
26 25 adantr 
 |-  ( ( ph /\ -. L <_ ( # ` W ) ) -> L e. RR )
27 23 25 ltnled 
 |-  ( ph -> ( ( # ` W ) < L <-> -. L <_ ( # ` W ) ) )
28 27 biimpar 
 |-  ( ( ph /\ -. L <_ ( # ` W ) ) -> ( # ` W ) < L )
29 24 26 28 ltled 
 |-  ( ( ph /\ -. L <_ ( # ` W ) ) -> ( # ` W ) <_ L )
30 18 19 20 29 lpadlem2 
 |-  ( ( ph /\ -. L <_ ( # ` W ) ) -> ( # ` ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ) = ( L - ( # ` W ) ) )
31 8 9 17 30 ifbothda 
 |-  ( ph -> ( # ` ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ) = if ( L <_ ( # ` W ) , 0 , ( L - ( # ` W ) ) ) )
32 31 4 eqtr4d 
 |-  ( ph -> ( # ` ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ) = M )
33 32 oveq2d 
 |-  ( ph -> ( N + ( # ` ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ) ) = ( N + M ) )
34 33 fveq2d 
 |-  ( ph -> ( ( ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ++ W ) ` ( N + ( # ` ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ) ) ) = ( ( ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ++ W ) ` ( N + M ) ) )
35 3 lpadlem1 
 |-  ( ph -> ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) e. Word S )
36 ccatval3 
 |-  ( ( ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) e. Word S /\ W e. Word S /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( ( ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ++ W ) ` ( N + ( # ` ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ) ) ) = ( W ` N ) )
37 35 2 5 36 syl3anc 
 |-  ( ph -> ( ( ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ++ W ) ` ( N + ( # ` ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ) ) ) = ( W ` N ) )
38 7 34 37 3eqtr2d 
 |-  ( ph -> ( ( ( C leftpad W ) ` L ) ` ( N + M ) ) = ( W ` N ) )