Metamath Proof Explorer


Theorem pfxlen

Description: Length of a prefix. (Contributed by Stefan O'Rear, 24-Aug-2015) (Revised by AV, 2-May-2020)

Ref Expression
Assertion pfxlen SWordAL0SSprefixL=L

Proof

Step Hyp Ref Expression
1 pfxfn SWordAL0SSprefixLFn0..^L
2 hashfn SprefixLFn0..^LSprefixL=0..^L
3 1 2 syl SWordAL0SSprefixL=0..^L
4 elfznn0 L0SL0
5 4 adantl SWordAL0SL0
6 hashfzo0 L00..^L=L
7 5 6 syl SWordAL0S0..^L=L
8 3 7 eqtrd SWordAL0SSprefixL=L