Metamath Proof Explorer

Theorem pfxval

Description: Value of a prefix operation. (Contributed by AV, 2-May-2020)

Ref Expression
Assertion pfxval 
|- ( ( S e. V /\ L e. NN0 ) -> ( S prefix L ) = ( S substr <. 0 , L >. ) )

Proof

Step Hyp Ref Expression
1 df-pfx 
 |-  prefix = ( s e. _V , l e. NN0 |-> ( s substr <. 0 , l >. ) )
2 1 a1i 
 |-  ( ( S e. V /\ L e. NN0 ) -> prefix = ( s e. _V , l e. NN0 |-> ( s substr <. 0 , l >. ) ) )
3 simpl 
 |-  ( ( s = S /\ l = L ) -> s = S )
4 opeq2 
 |-  ( l = L -> <. 0 , l >. = <. 0 , L >. )
5 4 adantl 
 |-  ( ( s = S /\ l = L ) -> <. 0 , l >. = <. 0 , L >. )
6 3 5 oveq12d 
 |-  ( ( s = S /\ l = L ) -> ( s substr <. 0 , l >. ) = ( S substr <. 0 , L >. ) )
7 6 adantl 
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( s = S /\ l = L ) ) -> ( s substr <. 0 , l >. ) = ( S substr <. 0 , L >. ) )
8 elex 
 |-  ( S e. V -> S e. _V )
9 8 adantr 
 |-  ( ( S e. V /\ L e. NN0 ) -> S e. _V )
10 simpr 
 |-  ( ( S e. V /\ L e. NN0 ) -> L e. NN0 )
11 ovexd 
 |-  ( ( S e. V /\ L e. NN0 ) -> ( S substr <. 0 , L >. ) e. _V )
12 2 7 9 10 11 ovmpod 
 |-  ( ( S e. V /\ L e. NN0 ) -> ( S prefix L ) = ( S substr <. 0 , L >. ) )