Metamath Proof Explorer

Theorem gsumspl

Description: The primary purpose of the splice construction is to enable local rewrites. Thus, in any monoidal valuation, if a splice does not cause a local change it does not cause a global change. (Contributed by Stefan O'Rear, 23-Aug-2015)

Ref Expression
Hypotheses gsumspl.b 
|- B = ( Base ` M )
gsumspl.m 
|- ( ph -> M e. Mnd )
gsumspl.s 
|- ( ph -> S e. Word B )
gsumspl.f 
|- ( ph -> F e. ( 0 ... T ) )
gsumspl.t 
|- ( ph -> T e. ( 0 ... ( # ` S ) ) )
gsumspl.x 
|- ( ph -> X e. Word B )
gsumspl.y 
|- ( ph -> Y e. Word B )
gsumspl.eq 
|- ( ph -> ( M gsum X ) = ( M gsum Y ) )
Assertion gsumspl 
|- ( ph -> ( M gsum ( S splice <. F , T , X >. ) ) = ( M gsum ( S splice <. F , T , Y >. ) ) )

Proof

Step Hyp Ref Expression
1 gsumspl.b 
 |-  B = ( Base ` M )
2 gsumspl.m 
 |-  ( ph -> M e. Mnd )
3 gsumspl.s 
 |-  ( ph -> S e. Word B )
4 gsumspl.f 
 |-  ( ph -> F e. ( 0 ... T ) )
5 gsumspl.t 
 |-  ( ph -> T e. ( 0 ... ( # ` S ) ) )
6 gsumspl.x 
 |-  ( ph -> X e. Word B )
7 gsumspl.y 
 |-  ( ph -> Y e. Word B )
8 gsumspl.eq 
 |-  ( ph -> ( M gsum X ) = ( M gsum Y ) )
9 8 oveq2d 
 |-  ( ph -> ( ( M gsum ( S prefix F ) ) ( +g ` M ) ( M gsum X ) ) = ( ( M gsum ( S prefix F ) ) ( +g ` M ) ( M gsum Y ) ) )
10 9 oveq1d 
 |-  ( ph -> ( ( ( M gsum ( S prefix F ) ) ( +g ` M ) ( M gsum X ) ) ( +g ` M ) ( M gsum ( S substr <. T , ( # ` S ) >. ) ) ) = ( ( ( M gsum ( S prefix F ) ) ( +g ` M ) ( M gsum Y ) ) ( +g ` M ) ( M gsum ( S substr <. T , ( # ` S ) >. ) ) ) )
11 splval 
 |-  ( ( S e. Word B /\ ( F e. ( 0 ... T ) /\ T e. ( 0 ... ( # ` S ) ) /\ X e. Word B ) ) -> ( S splice <. F , T , X >. ) = ( ( ( S prefix F ) ++ X ) ++ ( S substr <. T , ( # ` S ) >. ) ) )
12 3 4 5 6 11 syl13anc 
 |-  ( ph -> ( S splice <. F , T , X >. ) = ( ( ( S prefix F ) ++ X ) ++ ( S substr <. T , ( # ` S ) >. ) ) )
13 12 oveq2d 
 |-  ( ph -> ( M gsum ( S splice <. F , T , X >. ) ) = ( M gsum ( ( ( S prefix F ) ++ X ) ++ ( S substr <. T , ( # ` S ) >. ) ) ) )
14 pfxcl 
 |-  ( S e. Word B -> ( S prefix F ) e. Word B )
15 3 14 syl 
 |-  ( ph -> ( S prefix F ) e. Word B )
16 ccatcl 
 |-  ( ( ( S prefix F ) e. Word B /\ X e. Word B ) -> ( ( S prefix F ) ++ X ) e. Word B )
17 15 6 16 syl2anc 
 |-  ( ph -> ( ( S prefix F ) ++ X ) e. Word B )
18 swrdcl 
 |-  ( S e. Word B -> ( S substr <. T , ( # ` S ) >. ) e. Word B )
19 3 18 syl 
 |-  ( ph -> ( S substr <. T , ( # ` S ) >. ) e. Word B )
20 eqid 
 |-  ( +g ` M ) = ( +g ` M )
21 1 20 gsumccat 
 |-  ( ( M e. Mnd /\ ( ( S prefix F ) ++ X ) e. Word B /\ ( S substr <. T , ( # ` S ) >. ) e. Word B ) -> ( M gsum ( ( ( S prefix F ) ++ X ) ++ ( S substr <. T , ( # ` S ) >. ) ) ) = ( ( M gsum ( ( S prefix F ) ++ X ) ) ( +g ` M ) ( M gsum ( S substr <. T , ( # ` S ) >. ) ) ) )
22 2 17 19 21 syl3anc 
 |-  ( ph -> ( M gsum ( ( ( S prefix F ) ++ X ) ++ ( S substr <. T , ( # ` S ) >. ) ) ) = ( ( M gsum ( ( S prefix F ) ++ X ) ) ( +g ` M ) ( M gsum ( S substr <. T , ( # ` S ) >. ) ) ) )
23 1 20 gsumccat 
 |-  ( ( M e. Mnd /\ ( S prefix F ) e. Word B /\ X e. Word B ) -> ( M gsum ( ( S prefix F ) ++ X ) ) = ( ( M gsum ( S prefix F ) ) ( +g ` M ) ( M gsum X ) ) )
24 2 15 6 23 syl3anc 
 |-  ( ph -> ( M gsum ( ( S prefix F ) ++ X ) ) = ( ( M gsum ( S prefix F ) ) ( +g ` M ) ( M gsum X ) ) )
25 24 oveq1d 
 |-  ( ph -> ( ( M gsum ( ( S prefix F ) ++ X ) ) ( +g ` M ) ( M gsum ( S substr <. T , ( # ` S ) >. ) ) ) = ( ( ( M gsum ( S prefix F ) ) ( +g ` M ) ( M gsum X ) ) ( +g ` M ) ( M gsum ( S substr <. T , ( # ` S ) >. ) ) ) )
26 13 22 25 3eqtrd 
 |-  ( ph -> ( M gsum ( S splice <. F , T , X >. ) ) = ( ( ( M gsum ( S prefix F ) ) ( +g ` M ) ( M gsum X ) ) ( +g ` M ) ( M gsum ( S substr <. T , ( # ` S ) >. ) ) ) )
27 splval 
 |-  ( ( S e. Word B /\ ( F e. ( 0 ... T ) /\ T e. ( 0 ... ( # ` S ) ) /\ Y e. Word B ) ) -> ( S splice <. F , T , Y >. ) = ( ( ( S prefix F ) ++ Y ) ++ ( S substr <. T , ( # ` S ) >. ) ) )
28 3 4 5 7 27 syl13anc 
 |-  ( ph -> ( S splice <. F , T , Y >. ) = ( ( ( S prefix F ) ++ Y ) ++ ( S substr <. T , ( # ` S ) >. ) ) )
29 28 oveq2d 
 |-  ( ph -> ( M gsum ( S splice <. F , T , Y >. ) ) = ( M gsum ( ( ( S prefix F ) ++ Y ) ++ ( S substr <. T , ( # ` S ) >. ) ) ) )
30 ccatcl 
 |-  ( ( ( S prefix F ) e. Word B /\ Y e. Word B ) -> ( ( S prefix F ) ++ Y ) e. Word B )
31 15 7 30 syl2anc 
 |-  ( ph -> ( ( S prefix F ) ++ Y ) e. Word B )
32 1 20 gsumccat 
 |-  ( ( M e. Mnd /\ ( ( S prefix F ) ++ Y ) e. Word B /\ ( S substr <. T , ( # ` S ) >. ) e. Word B ) -> ( M gsum ( ( ( S prefix F ) ++ Y ) ++ ( S substr <. T , ( # ` S ) >. ) ) ) = ( ( M gsum ( ( S prefix F ) ++ Y ) ) ( +g ` M ) ( M gsum ( S substr <. T , ( # ` S ) >. ) ) ) )
33 2 31 19 32 syl3anc 
 |-  ( ph -> ( M gsum ( ( ( S prefix F ) ++ Y ) ++ ( S substr <. T , ( # ` S ) >. ) ) ) = ( ( M gsum ( ( S prefix F ) ++ Y ) ) ( +g ` M ) ( M gsum ( S substr <. T , ( # ` S ) >. ) ) ) )
34 1 20 gsumccat 
 |-  ( ( M e. Mnd /\ ( S prefix F ) e. Word B /\ Y e. Word B ) -> ( M gsum ( ( S prefix F ) ++ Y ) ) = ( ( M gsum ( S prefix F ) ) ( +g ` M ) ( M gsum Y ) ) )
35 2 15 7 34 syl3anc 
 |-  ( ph -> ( M gsum ( ( S prefix F ) ++ Y ) ) = ( ( M gsum ( S prefix F ) ) ( +g ` M ) ( M gsum Y ) ) )
36 35 oveq1d 
 |-  ( ph -> ( ( M gsum ( ( S prefix F ) ++ Y ) ) ( +g ` M ) ( M gsum ( S substr <. T , ( # ` S ) >. ) ) ) = ( ( ( M gsum ( S prefix F ) ) ( +g ` M ) ( M gsum Y ) ) ( +g ` M ) ( M gsum ( S substr <. T , ( # ` S ) >. ) ) ) )
37 29 33 36 3eqtrd 
 |-  ( ph -> ( M gsum ( S splice <. F , T , Y >. ) ) = ( ( ( M gsum ( S prefix F ) ) ( +g ` M ) ( M gsum Y ) ) ( +g ` M ) ( M gsum ( S substr <. T , ( # ` S ) >. ) ) ) )
38 10 26 37 3eqtr4d 
 |-  ( ph -> ( M gsum ( S splice <. F , T , X >. ) ) = ( M gsum ( S splice <. F , T , Y >. ) ) )