Metamath Proof Explorer

Theorem splid

Description: Splicing a subword for the same subword makes no difference. (Contributed by Stefan O'Rear, 20-Aug-2015) (Proof shortened by AV, 14-Oct-2022)

Ref Expression
Assertion splid 
|- ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... ( # ` S ) ) ) ) -> ( S splice <. X , Y , ( S substr <. X , Y >. ) >. ) = S )

Proof

Step Hyp Ref Expression
1 ovex 
 |-  ( S substr <. X , Y >. ) e. _V
2 splval 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... ( # ` S ) ) /\ ( S substr <. X , Y >. ) e. _V ) ) -> ( S splice <. X , Y , ( S substr <. X , Y >. ) >. ) = ( ( ( S prefix X ) ++ ( S substr <. X , Y >. ) ) ++ ( S substr <. Y , ( # ` S ) >. ) ) )
3 1 2 mp3anr3 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... ( # ` S ) ) ) ) -> ( S splice <. X , Y , ( S substr <. X , Y >. ) >. ) = ( ( ( S prefix X ) ++ ( S substr <. X , Y >. ) ) ++ ( S substr <. Y , ( # ` S ) >. ) ) )
4 ccatpfx 
 |-  ( ( S e. Word A /\ X e. ( 0 ... Y ) /\ Y e. ( 0 ... ( # ` S ) ) ) -> ( ( S prefix X ) ++ ( S substr <. X , Y >. ) ) = ( S prefix Y ) )
5 4 3expb 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... ( # ` S ) ) ) ) -> ( ( S prefix X ) ++ ( S substr <. X , Y >. ) ) = ( S prefix Y ) )
6 5 oveq1d 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... ( # ` S ) ) ) ) -> ( ( ( S prefix X ) ++ ( S substr <. X , Y >. ) ) ++ ( S substr <. Y , ( # ` S ) >. ) ) = ( ( S prefix Y ) ++ ( S substr <. Y , ( # ` S ) >. ) ) )
7 simpl 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... ( # ` S ) ) ) ) -> S e. Word A )
8 simprr 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... ( # ` S ) ) ) ) -> Y e. ( 0 ... ( # ` S ) ) )
9 elfzuz2 
 |-  ( Y e. ( 0 ... ( # ` S ) ) -> ( # ` S ) e. ( ZZ>= ` 0 ) )
10 9 ad2antll 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... ( # ` S ) ) ) ) -> ( # ` S ) e. ( ZZ>= ` 0 ) )
11 eluzfz2 
 |-  ( ( # ` S ) e. ( ZZ>= ` 0 ) -> ( # ` S ) e. ( 0 ... ( # ` S ) ) )
12 10 11 syl 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... ( # ` S ) ) ) ) -> ( # ` S ) e. ( 0 ... ( # ` S ) ) )
13 ccatpfx 
 |-  ( ( S e. Word A /\ Y e. ( 0 ... ( # ` S ) ) /\ ( # ` S ) e. ( 0 ... ( # ` S ) ) ) -> ( ( S prefix Y ) ++ ( S substr <. Y , ( # ` S ) >. ) ) = ( S prefix ( # ` S ) ) )
14 7 8 12 13 syl3anc 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... ( # ` S ) ) ) ) -> ( ( S prefix Y ) ++ ( S substr <. Y , ( # ` S ) >. ) ) = ( S prefix ( # ` S ) ) )
15 pfxid 
 |-  ( S e. Word A -> ( S prefix ( # ` S ) ) = S )
16 15 adantr 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... ( # ` S ) ) ) ) -> ( S prefix ( # ` S ) ) = S )
17 14 16 eqtrd 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... ( # ` S ) ) ) ) -> ( ( S prefix Y ) ++ ( S substr <. Y , ( # ` S ) >. ) ) = S )
18 6 17 eqtrd 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... ( # ` S ) ) ) ) -> ( ( ( S prefix X ) ++ ( S substr <. X , Y >. ) ) ++ ( S substr <. Y , ( # ` S ) >. ) ) = S )
19 3 18 eqtrd 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... ( # ` S ) ) ) ) -> ( S splice <. X , Y , ( S substr <. X , Y >. ) >. ) = S )