Metamath Proof Explorer

Theorem splval

Description: Value of the substring replacement operator. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by AV, 11-May-2020) (Revised by AV, 15-Oct-2022)

Ref Expression
Assertion splval 
|- ( ( S e. V /\ ( F e. W /\ T e. X /\ R e. Y ) ) -> ( S splice <. F , T , R >. ) = ( ( ( S prefix F ) ++ R ) ++ ( S substr <. T , ( # ` S ) >. ) ) )

Proof

Step Hyp Ref Expression
1 df-splice 
 |-  splice = ( s e. _V , b e. _V |-> ( ( ( s prefix ( 1st ` ( 1st ` b ) ) ) ++ ( 2nd ` b ) ) ++ ( s substr <. ( 2nd ` ( 1st ` b ) ) , ( # ` s ) >. ) ) )
2 1 a1i 
 |-  ( ( S e. V /\ ( F e. W /\ T e. X /\ R e. Y ) ) -> splice = ( s e. _V , b e. _V |-> ( ( ( s prefix ( 1st ` ( 1st ` b ) ) ) ++ ( 2nd ` b ) ) ++ ( s substr <. ( 2nd ` ( 1st ` b ) ) , ( # ` s ) >. ) ) ) )
3 simprl 
 |-  ( ( ( S e. V /\ ( F e. W /\ T e. X /\ R e. Y ) ) /\ ( s = S /\ b = <. F , T , R >. ) ) -> s = S )
4 2fveq3 
 |-  ( b = <. F , T , R >. -> ( 1st ` ( 1st ` b ) ) = ( 1st ` ( 1st ` <. F , T , R >. ) ) )
5 4 adantl 
 |-  ( ( s = S /\ b = <. F , T , R >. ) -> ( 1st ` ( 1st ` b ) ) = ( 1st ` ( 1st ` <. F , T , R >. ) ) )
6 ot1stg 
 |-  ( ( F e. W /\ T e. X /\ R e. Y ) -> ( 1st ` ( 1st ` <. F , T , R >. ) ) = F )
7 6 adantl 
 |-  ( ( S e. V /\ ( F e. W /\ T e. X /\ R e. Y ) ) -> ( 1st ` ( 1st ` <. F , T , R >. ) ) = F )
8 5 7 sylan9eqr 
 |-  ( ( ( S e. V /\ ( F e. W /\ T e. X /\ R e. Y ) ) /\ ( s = S /\ b = <. F , T , R >. ) ) -> ( 1st ` ( 1st ` b ) ) = F )
9 3 8 oveq12d 
 |-  ( ( ( S e. V /\ ( F e. W /\ T e. X /\ R e. Y ) ) /\ ( s = S /\ b = <. F , T , R >. ) ) -> ( s prefix ( 1st ` ( 1st ` b ) ) ) = ( S prefix F ) )
10 fveq2 
 |-  ( b = <. F , T , R >. -> ( 2nd ` b ) = ( 2nd ` <. F , T , R >. ) )
11 10 adantl 
 |-  ( ( s = S /\ b = <. F , T , R >. ) -> ( 2nd ` b ) = ( 2nd ` <. F , T , R >. ) )
12 ot3rdg 
 |-  ( R e. Y -> ( 2nd ` <. F , T , R >. ) = R )
13 12 3ad2ant3 
 |-  ( ( F e. W /\ T e. X /\ R e. Y ) -> ( 2nd ` <. F , T , R >. ) = R )
14 13 adantl 
 |-  ( ( S e. V /\ ( F e. W /\ T e. X /\ R e. Y ) ) -> ( 2nd ` <. F , T , R >. ) = R )
15 11 14 sylan9eqr 
 |-  ( ( ( S e. V /\ ( F e. W /\ T e. X /\ R e. Y ) ) /\ ( s = S /\ b = <. F , T , R >. ) ) -> ( 2nd ` b ) = R )
16 9 15 oveq12d 
 |-  ( ( ( S e. V /\ ( F e. W /\ T e. X /\ R e. Y ) ) /\ ( s = S /\ b = <. F , T , R >. ) ) -> ( ( s prefix ( 1st ` ( 1st ` b ) ) ) ++ ( 2nd ` b ) ) = ( ( S prefix F ) ++ R ) )
17 2fveq3 
 |-  ( b = <. F , T , R >. -> ( 2nd ` ( 1st ` b ) ) = ( 2nd ` ( 1st ` <. F , T , R >. ) ) )
18 17 adantl 
 |-  ( ( s = S /\ b = <. F , T , R >. ) -> ( 2nd ` ( 1st ` b ) ) = ( 2nd ` ( 1st ` <. F , T , R >. ) ) )
19 ot2ndg 
 |-  ( ( F e. W /\ T e. X /\ R e. Y ) -> ( 2nd ` ( 1st ` <. F , T , R >. ) ) = T )
20 19 adantl 
 |-  ( ( S e. V /\ ( F e. W /\ T e. X /\ R e. Y ) ) -> ( 2nd ` ( 1st ` <. F , T , R >. ) ) = T )
21 18 20 sylan9eqr 
 |-  ( ( ( S e. V /\ ( F e. W /\ T e. X /\ R e. Y ) ) /\ ( s = S /\ b = <. F , T , R >. ) ) -> ( 2nd ` ( 1st ` b ) ) = T )
22 3 fveq2d 
 |-  ( ( ( S e. V /\ ( F e. W /\ T e. X /\ R e. Y ) ) /\ ( s = S /\ b = <. F , T , R >. ) ) -> ( # ` s ) = ( # ` S ) )
23 21 22 opeq12d 
 |-  ( ( ( S e. V /\ ( F e. W /\ T e. X /\ R e. Y ) ) /\ ( s = S /\ b = <. F , T , R >. ) ) -> <. ( 2nd ` ( 1st ` b ) ) , ( # ` s ) >. = <. T , ( # ` S ) >. )
24 3 23 oveq12d 
 |-  ( ( ( S e. V /\ ( F e. W /\ T e. X /\ R e. Y ) ) /\ ( s = S /\ b = <. F , T , R >. ) ) -> ( s substr <. ( 2nd ` ( 1st ` b ) ) , ( # ` s ) >. ) = ( S substr <. T , ( # ` S ) >. ) )
25 16 24 oveq12d 
 |-  ( ( ( S e. V /\ ( F e. W /\ T e. X /\ R e. Y ) ) /\ ( s = S /\ b = <. F , T , R >. ) ) -> ( ( ( s prefix ( 1st ` ( 1st ` b ) ) ) ++ ( 2nd ` b ) ) ++ ( s substr <. ( 2nd ` ( 1st ` b ) ) , ( # ` s ) >. ) ) = ( ( ( S prefix F ) ++ R ) ++ ( S substr <. T , ( # ` S ) >. ) ) )
26 elex 
 |-  ( S e. V -> S e. _V )
27 26 adantr 
 |-  ( ( S e. V /\ ( F e. W /\ T e. X /\ R e. Y ) ) -> S e. _V )
28 otex 
 |-  <. F , T , R >. e. _V
29 28 a1i 
 |-  ( ( S e. V /\ ( F e. W /\ T e. X /\ R e. Y ) ) -> <. F , T , R >. e. _V )
30 ovexd 
 |-  ( ( S e. V /\ ( F e. W /\ T e. X /\ R e. Y ) ) -> ( ( ( S prefix F ) ++ R ) ++ ( S substr <. T , ( # ` S ) >. ) ) e. _V )
31 2 25 27 29 30 ovmpod 
 |-  ( ( S e. V /\ ( F e. W /\ T e. X /\ R e. Y ) ) -> ( S splice <. F , T , R >. ) = ( ( ( S prefix F ) ++ R ) ++ ( S substr <. T , ( # ` S ) >. ) ) )