Metamath Proof Explorer


Theorem pfxval0

Description: Value of a prefix operation. This theorem should only be used in proofs if L e. NN0 is not available. Otherwise (and usually), pfxval should be used. (Contributed by AV, 3-Dec-2022) (New usage is discouraged.)

Ref Expression
Assertion pfxval0 SWordASprefixL=Ssubstr0L

Proof

Step Hyp Ref Expression
1 pfxval SWordAL0SprefixL=Ssubstr0L
2 simpr SVL0L0
3 2 con3i ¬L0¬SVL0
4 3 adantl SWordA¬L0¬SVL0
5 pfxnndmnd ¬SVL0SprefixL=
6 4 5 syl SWordA¬L0SprefixL=
7 simpr 00L0L0
8 7 con3i ¬L0¬00L0
9 swrdnnn0nd SWordA¬00L0Ssubstr0L=
10 8 9 sylan2 SWordA¬L0Ssubstr0L=
11 6 10 eqtr4d SWordA¬L0SprefixL=Ssubstr0L
12 1 11 pm2.61dan SWordASprefixL=Ssubstr0L