Metamath Proof Explorer

Theorem lpadval

Description: Value of the leftpad function. (Contributed by Thierry Arnoux, 7-Aug-2023)

Ref Expression
Hypotheses lpadval.1 
|- ( ph -> L e. NN0 )
lpadval.2 
|- ( ph -> W e. Word S )
lpadval.3 
|- ( ph -> C e. S )
Assertion lpadval 
|- ( ph -> ( ( C leftpad W ) ` L ) = ( ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ++ W ) )

Proof

Step Hyp Ref Expression
1 lpadval.1 
 |-  ( ph -> L e. NN0 )
2 lpadval.2 
 |-  ( ph -> W e. Word S )
3 lpadval.3 
 |-  ( ph -> C e. S )
4 df-lpad 
 |-  leftpad = ( c e. _V , w e. _V |-> ( l e. NN0 |-> ( ( ( 0 ..^ ( l - ( # ` w ) ) ) X. { c } ) ++ w ) ) )
5 4 a1i 
 |-  ( ph -> leftpad = ( c e. _V , w e. _V |-> ( l e. NN0 |-> ( ( ( 0 ..^ ( l - ( # ` w ) ) ) X. { c } ) ++ w ) ) ) )
6 simprr 
 |-  ( ( ph /\ ( c = C /\ w = W ) ) -> w = W )
7 6 fveq2d 
 |-  ( ( ph /\ ( c = C /\ w = W ) ) -> ( # ` w ) = ( # ` W ) )
8 7 oveq2d 
 |-  ( ( ph /\ ( c = C /\ w = W ) ) -> ( l - ( # ` w ) ) = ( l - ( # ` W ) ) )
9 8 oveq2d 
 |-  ( ( ph /\ ( c = C /\ w = W ) ) -> ( 0 ..^ ( l - ( # ` w ) ) ) = ( 0 ..^ ( l - ( # ` W ) ) ) )
10 simprl 
 |-  ( ( ph /\ ( c = C /\ w = W ) ) -> c = C )
11 10 sneqd 
 |-  ( ( ph /\ ( c = C /\ w = W ) ) -> { c } = { C } )
12 9 11 xpeq12d 
 |-  ( ( ph /\ ( c = C /\ w = W ) ) -> ( ( 0 ..^ ( l - ( # ` w ) ) ) X. { c } ) = ( ( 0 ..^ ( l - ( # ` W ) ) ) X. { C } ) )
13 12 6 oveq12d 
 |-  ( ( ph /\ ( c = C /\ w = W ) ) -> ( ( ( 0 ..^ ( l - ( # ` w ) ) ) X. { c } ) ++ w ) = ( ( ( 0 ..^ ( l - ( # ` W ) ) ) X. { C } ) ++ W ) )
14 13 mpteq2dv 
 |-  ( ( ph /\ ( c = C /\ w = W ) ) -> ( l e. NN0 |-> ( ( ( 0 ..^ ( l - ( # ` w ) ) ) X. { c } ) ++ w ) ) = ( l e. NN0 |-> ( ( ( 0 ..^ ( l - ( # ` W ) ) ) X. { C } ) ++ W ) ) )
15 3 elexd 
 |-  ( ph -> C e. _V )
16 2 elexd 
 |-  ( ph -> W e. _V )
17 nn0ex 
 |-  NN0 e. _V
18 17 a1i 
 |-  ( ph -> NN0 e. _V )
19 18 mptexd 
 |-  ( ph -> ( l e. NN0 |-> ( ( ( 0 ..^ ( l - ( # ` W ) ) ) X. { C } ) ++ W ) ) e. _V )
20 5 14 15 16 19 ovmpod 
 |-  ( ph -> ( C leftpad W ) = ( l e. NN0 |-> ( ( ( 0 ..^ ( l - ( # ` W ) ) ) X. { C } ) ++ W ) ) )
21 simpr 
 |-  ( ( ph /\ l = L ) -> l = L )
22 21 oveq1d 
 |-  ( ( ph /\ l = L ) -> ( l - ( # ` W ) ) = ( L - ( # ` W ) ) )
23 22 oveq2d 
 |-  ( ( ph /\ l = L ) -> ( 0 ..^ ( l - ( # ` W ) ) ) = ( 0 ..^ ( L - ( # ` W ) ) ) )
24 23 xpeq1d 
 |-  ( ( ph /\ l = L ) -> ( ( 0 ..^ ( l - ( # ` W ) ) ) X. { C } ) = ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) )
25 24 oveq1d 
 |-  ( ( ph /\ l = L ) -> ( ( ( 0 ..^ ( l - ( # ` W ) ) ) X. { C } ) ++ W ) = ( ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ++ W ) )
26 ovexd 
 |-  ( ph -> ( ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ++ W ) e. _V )
27 20 25 1 26 fvmptd 
 |-  ( ph -> ( ( C leftpad W ) ` L ) = ( ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ++ W ) )