Metamath Proof Explorer


Theorem wrdmap

Description: Words as a mapping. (Contributed by Thierry Arnoux, 4-Mar-2020)

Ref Expression
Assertion wrdmap V X N 0 W Word V W = N W V 0 ..^ N

Proof

Step Hyp Ref Expression
1 fveqeq2 w = W w = N W = N
2 1 elrab W w Word V | w = N W Word V W = N
3 wrdnval V X N 0 w Word V | w = N = V 0 ..^ N
4 3 eleq2d V X N 0 W w Word V | w = N W V 0 ..^ N
5 2 4 bitr3id V X N 0 W Word V W = N W V 0 ..^ N