Metamath Proof Explorer

Theorem splcl

Description: Closure of the substring replacement operator. (Contributed by Stefan O'Rear, 26-Aug-2015) (Proof shortened by AV, 15-Oct-2022)

Ref Expression
Assertion splcl 
|- ( ( S e. Word A /\ R e. Word A ) -> ( S splice <. F , T , R >. ) e. Word A )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( S e. Word A -> S e. _V )
2 otex 
 |-  <. F , T , R >. e. _V
3 id 
 |-  ( s = S -> s = S )
4 2fveq3 
 |-  ( b = <. F , T , R >. -> ( 1st ` ( 1st ` b ) ) = ( 1st ` ( 1st ` <. F , T , R >. ) ) )
5 3 4 oveqan12d 
 |-  ( ( s = S /\ b = <. F , T , R >. ) -> ( s prefix ( 1st ` ( 1st ` b ) ) ) = ( S prefix ( 1st ` ( 1st ` <. F , T , R >. ) ) ) )
6 simpr 
 |-  ( ( s = S /\ b = <. F , T , R >. ) -> b = <. F , T , R >. )
7 6 fveq2d 
 |-  ( ( s = S /\ b = <. F , T , R >. ) -> ( 2nd ` b ) = ( 2nd ` <. F , T , R >. ) )
8 5 7 oveq12d 
 |-  ( ( s = S /\ b = <. F , T , R >. ) -> ( ( s prefix ( 1st ` ( 1st ` b ) ) ) ++ ( 2nd ` b ) ) = ( ( S prefix ( 1st ` ( 1st ` <. F , T , R >. ) ) ) ++ ( 2nd ` <. F , T , R >. ) ) )
9 simpl 
 |-  ( ( s = S /\ b = <. F , T , R >. ) -> s = S )
10 6 fveq2d 
 |-  ( ( s = S /\ b = <. F , T , R >. ) -> ( 1st ` b ) = ( 1st ` <. F , T , R >. ) )
11 10 fveq2d 
 |-  ( ( s = S /\ b = <. F , T , R >. ) -> ( 2nd ` ( 1st ` b ) ) = ( 2nd ` ( 1st ` <. F , T , R >. ) ) )
12 9 fveq2d 
 |-  ( ( s = S /\ b = <. F , T , R >. ) -> ( # ` s ) = ( # ` S ) )
13 11 12 opeq12d 
 |-  ( ( s = S /\ b = <. F , T , R >. ) -> <. ( 2nd ` ( 1st ` b ) ) , ( # ` s ) >. = <. ( 2nd ` ( 1st ` <. F , T , R >. ) ) , ( # ` S ) >. )
14 9 13 oveq12d 
 |-  ( ( s = S /\ b = <. F , T , R >. ) -> ( s substr <. ( 2nd ` ( 1st ` b ) ) , ( # ` s ) >. ) = ( S substr <. ( 2nd ` ( 1st ` <. F , T , R >. ) ) , ( # ` S ) >. ) )
15 8 14 oveq12d 
 |-  ( ( s = S /\ b = <. F , T , R >. ) -> ( ( ( s prefix ( 1st ` ( 1st ` b ) ) ) ++ ( 2nd ` b ) ) ++ ( s substr <. ( 2nd ` ( 1st ` b ) ) , ( # ` s ) >. ) ) = ( ( ( S prefix ( 1st ` ( 1st ` <. F , T , R >. ) ) ) ++ ( 2nd ` <. F , T , R >. ) ) ++ ( S substr <. ( 2nd ` ( 1st ` <. F , T , R >. ) ) , ( # ` S ) >. ) ) )
16 df-splice 
 |-  splice = ( s e. _V , b e. _V |-> ( ( ( s prefix ( 1st ` ( 1st ` b ) ) ) ++ ( 2nd ` b ) ) ++ ( s substr <. ( 2nd ` ( 1st ` b ) ) , ( # ` s ) >. ) ) )
17 ovex 
 |-  ( ( ( S prefix ( 1st ` ( 1st ` <. F , T , R >. ) ) ) ++ ( 2nd ` <. F , T , R >. ) ) ++ ( S substr <. ( 2nd ` ( 1st ` <. F , T , R >. ) ) , ( # ` S ) >. ) ) e. _V
18 15 16 17 ovmpoa 
 |-  ( ( S e. _V /\ <. F , T , R >. e. _V ) -> ( S splice <. F , T , R >. ) = ( ( ( S prefix ( 1st ` ( 1st ` <. F , T , R >. ) ) ) ++ ( 2nd ` <. F , T , R >. ) ) ++ ( S substr <. ( 2nd ` ( 1st ` <. F , T , R >. ) ) , ( # ` S ) >. ) ) )
19 1 2 18 sylancl 
 |-  ( S e. Word A -> ( S splice <. F , T , R >. ) = ( ( ( S prefix ( 1st ` ( 1st ` <. F , T , R >. ) ) ) ++ ( 2nd ` <. F , T , R >. ) ) ++ ( S substr <. ( 2nd ` ( 1st ` <. F , T , R >. ) ) , ( # ` S ) >. ) ) )
20 19 adantr 
 |-  ( ( S e. Word A /\ R e. Word A ) -> ( S splice <. F , T , R >. ) = ( ( ( S prefix ( 1st ` ( 1st ` <. F , T , R >. ) ) ) ++ ( 2nd ` <. F , T , R >. ) ) ++ ( S substr <. ( 2nd ` ( 1st ` <. F , T , R >. ) ) , ( # ` S ) >. ) ) )
21 pfxcl 
 |-  ( S e. Word A -> ( S prefix ( 1st ` ( 1st ` <. F , T , R >. ) ) ) e. Word A )
22 21 adantr 
 |-  ( ( S e. Word A /\ R e. Word A ) -> ( S prefix ( 1st ` ( 1st ` <. F , T , R >. ) ) ) e. Word A )
23 ot3rdg 
 |-  ( R e. Word A -> ( 2nd ` <. F , T , R >. ) = R )
24 23 adantl 
 |-  ( ( S e. Word A /\ R e. Word A ) -> ( 2nd ` <. F , T , R >. ) = R )
25 simpr 
 |-  ( ( S e. Word A /\ R e. Word A ) -> R e. Word A )
26 24 25 eqeltrd 
 |-  ( ( S e. Word A /\ R e. Word A ) -> ( 2nd ` <. F , T , R >. ) e. Word A )
27 ccatcl 
 |-  ( ( ( S prefix ( 1st ` ( 1st ` <. F , T , R >. ) ) ) e. Word A /\ ( 2nd ` <. F , T , R >. ) e. Word A ) -> ( ( S prefix ( 1st ` ( 1st ` <. F , T , R >. ) ) ) ++ ( 2nd ` <. F , T , R >. ) ) e. Word A )
28 22 26 27 syl2anc 
 |-  ( ( S e. Word A /\ R e. Word A ) -> ( ( S prefix ( 1st ` ( 1st ` <. F , T , R >. ) ) ) ++ ( 2nd ` <. F , T , R >. ) ) e. Word A )
29 swrdcl 
 |-  ( S e. Word A -> ( S substr <. ( 2nd ` ( 1st ` <. F , T , R >. ) ) , ( # ` S ) >. ) e. Word A )
30 29 adantr 
 |-  ( ( S e. Word A /\ R e. Word A ) -> ( S substr <. ( 2nd ` ( 1st ` <. F , T , R >. ) ) , ( # ` S ) >. ) e. Word A )
31 ccatcl 
 |-  ( ( ( ( S prefix ( 1st ` ( 1st ` <. F , T , R >. ) ) ) ++ ( 2nd ` <. F , T , R >. ) ) e. Word A /\ ( S substr <. ( 2nd ` ( 1st ` <. F , T , R >. ) ) , ( # ` S ) >. ) e. Word A ) -> ( ( ( S prefix ( 1st ` ( 1st ` <. F , T , R >. ) ) ) ++ ( 2nd ` <. F , T , R >. ) ) ++ ( S substr <. ( 2nd ` ( 1st ` <. F , T , R >. ) ) , ( # ` S ) >. ) ) e. Word A )
32 28 30 31 syl2anc 
 |-  ( ( S e. Word A /\ R e. Word A ) -> ( ( ( S prefix ( 1st ` ( 1st ` <. F , T , R >. ) ) ) ++ ( 2nd ` <. F , T , R >. ) ) ++ ( S substr <. ( 2nd ` ( 1st ` <. F , T , R >. ) ) , ( # ` S ) >. ) ) e. Word A )
33 20 32 eqeltrd 
 |-  ( ( S e. Word A /\ R e. Word A ) -> ( S splice <. F , T , R >. ) e. Word A )