Metamath Proof Explorer


Theorem pfxco

Description: Mapping of words commutes with the prefix operation. (Contributed by AV, 15-May-2020)

Ref Expression
Assertion pfxco WWordAN0WF:ABFWprefixN=FWprefixN

Proof

Step Hyp Ref Expression
1 elfznn0 N0WN0
2 1 3ad2ant2 WWordAN0WF:ABN0
3 0elfz N000N
4 2 3 syl WWordAN0WF:AB00N
5 simp2 WWordAN0WF:ABN0W
6 4 5 jca WWordAN0WF:AB00NN0W
7 swrdco WWordA00NN0WF:ABFWsubstr0N=FWsubstr0N
8 6 7 syld3an2 WWordAN0WF:ABFWsubstr0N=FWsubstr0N
9 pfxval WWordAN0WprefixN=Wsubstr0N
10 1 9 sylan2 WWordAN0WWprefixN=Wsubstr0N
11 10 coeq2d WWordAN0WFWprefixN=FWsubstr0N
12 11 3adant3 WWordAN0WF:ABFWprefixN=FWsubstr0N
13 ffun F:ABFunF
14 13 anim2i WWordAF:ABWWordAFunF
15 14 ancomd WWordAF:ABFunFWWordA
16 15 3adant2 WWordAN0WF:ABFunFWWordA
17 cofunexg FunFWWordAFWV
18 16 17 syl WWordAN0WF:ABFWV
19 18 2 jca WWordAN0WF:ABFWVN0
20 pfxval FWVN0FWprefixN=FWsubstr0N
21 19 20 syl WWordAN0WF:ABFWprefixN=FWsubstr0N
22 8 12 21 3eqtr4d WWordAN0WF:ABFWprefixN=FWprefixN