This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐵 = ( Base ‘ 𝑀 )
gsumspl.m ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
gsumspl.s ⊢ ( 𝜑 → 𝑆 ∈ Word 𝐵 )
gsumspl.f ⊢ ( 𝜑 → 𝐹 ∈ ( 0 ... 𝑇 ) )
gsumspl.t ⊢ ( 𝜑 → 𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
gsumspl.x ⊢ ( 𝜑 → 𝑋 ∈ Word 𝐵 )
gsumspl.y ⊢ ( 𝜑 → 𝑌 ∈ Word 𝐵 )
gsumspl.eq ⊢ ( 𝜑 → ( 𝑀 Σg 𝑋 ) = ( 𝑀 Σg 𝑌 ) )
Assertion gsumspl ( 𝜑 → ( 𝑀 Σg ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑋 ⟩ ) ) = ( 𝑀 Σg ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑌 ⟩ ) ) )

Proof

Step Hyp Ref Expression
1 gsumspl.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 gsumspl.m ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
3 gsumspl.s ⊢ ( 𝜑 → 𝑆 ∈ Word 𝐵 )
4 gsumspl.f ⊢ ( 𝜑 → 𝐹 ∈ ( 0 ... 𝑇 ) )
5 gsumspl.t ⊢ ( 𝜑 → 𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
6 gsumspl.x ⊢ ( 𝜑 → 𝑋 ∈ Word 𝐵 )
7 gsumspl.y ⊢ ( 𝜑 → 𝑌 ∈ Word 𝐵 )
8 gsumspl.eq ⊢ ( 𝜑 → ( 𝑀 Σg 𝑋 ) = ( 𝑀 Σg 𝑌 ) )
9 8 oveq2d ⊢ ( 𝜑 → ( ( 𝑀 Σg ( 𝑆 prefix 𝐹 ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑋 ) ) = ( ( 𝑀 Σg ( 𝑆 prefix 𝐹 ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑌 ) ) )
10 9 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑀 Σg ( 𝑆 prefix 𝐹 ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑋 ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ) = ( ( ( 𝑀 Σg ( 𝑆 prefix 𝐹 ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑌 ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ) )
11 splval ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ ( 𝐹 ∈ ( 0 ... 𝑇 ) ∧ 𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ∧ 𝑋 ∈ Word 𝐵 ) ) → ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑋 ⟩ ) = ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑋 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) )
12 3 4 5 6 11 syl13anc ⊢ ( 𝜑 → ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑋 ⟩ ) = ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑋 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) )
13 12 oveq2d ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑋 ⟩ ) ) = ( 𝑀 Σg ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑋 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ) )
14 pfxcl ⊢ ( 𝑆 ∈ Word 𝐵 → ( 𝑆 prefix 𝐹 ) ∈ Word 𝐵 )
15 3 14 syl ⊢ ( 𝜑 → ( 𝑆 prefix 𝐹 ) ∈ Word 𝐵 )
16 ccatcl ⊢ ( ( ( 𝑆 prefix 𝐹 ) ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵 ) → ( ( 𝑆 prefix 𝐹 ) ++ 𝑋 ) ∈ Word 𝐵 )
17 15 6 16 syl2anc ⊢ ( 𝜑 → ( ( 𝑆 prefix 𝐹 ) ++ 𝑋 ) ∈ Word 𝐵 )
18 swrdcl ⊢ ( 𝑆 ∈ Word 𝐵 → ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ∈ Word 𝐵 )
19 3 18 syl ⊢ ( 𝜑 → ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ∈ Word 𝐵 )
20 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
21 1 20 gsumccat ⊢ ( ( 𝑀 ∈ Mnd ∧ ( ( 𝑆 prefix 𝐹 ) ++ 𝑋 ) ∈ Word 𝐵 ∧ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ∈ Word 𝐵 ) → ( 𝑀 Σg ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑋 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ) = ( ( 𝑀 Σg ( ( 𝑆 prefix 𝐹 ) ++ 𝑋 ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ) )
22 2 17 19 21 syl3anc ⊢ ( 𝜑 → ( 𝑀 Σg ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑋 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ) = ( ( 𝑀 Σg ( ( 𝑆 prefix 𝐹 ) ++ 𝑋 ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ) )
23 1 20 gsumccat ⊢ ( ( 𝑀 ∈ Mnd ∧ ( 𝑆 prefix 𝐹 ) ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵 ) → ( 𝑀 Σg ( ( 𝑆 prefix 𝐹 ) ++ 𝑋 ) ) = ( ( 𝑀 Σg ( 𝑆 prefix 𝐹 ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑋 ) ) )
24 2 15 6 23 syl3anc ⊢ ( 𝜑 → ( 𝑀 Σg ( ( 𝑆 prefix 𝐹 ) ++ 𝑋 ) ) = ( ( 𝑀 Σg ( 𝑆 prefix 𝐹 ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑋 ) ) )
25 24 oveq1d ⊢ ( 𝜑 → ( ( 𝑀 Σg ( ( 𝑆 prefix 𝐹 ) ++ 𝑋 ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ) = ( ( ( 𝑀 Σg ( 𝑆 prefix 𝐹 ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑋 ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ) )
26 13 22 25 3eqtrd ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑋 ⟩ ) ) = ( ( ( 𝑀 Σg ( 𝑆 prefix 𝐹 ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑋 ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ) )
27 splval ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ ( 𝐹 ∈ ( 0 ... 𝑇 ) ∧ 𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ∧ 𝑌 ∈ Word 𝐵 ) ) → ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑌 ⟩ ) = ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) )
28 3 4 5 7 27 syl13anc ⊢ ( 𝜑 → ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑌 ⟩ ) = ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) )
29 28 oveq2d ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑌 ⟩ ) ) = ( 𝑀 Σg ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ) )
30 ccatcl ⊢ ( ( ( 𝑆 prefix 𝐹 ) ∈ Word 𝐵 ∧ 𝑌 ∈ Word 𝐵 ) → ( ( 𝑆 prefix 𝐹 ) ++ 𝑌 ) ∈ Word 𝐵 )
31 15 7 30 syl2anc ⊢ ( 𝜑 → ( ( 𝑆 prefix 𝐹 ) ++ 𝑌 ) ∈ Word 𝐵 )
32 1 20 gsumccat ⊢ ( ( 𝑀 ∈ Mnd ∧ ( ( 𝑆 prefix 𝐹 ) ++ 𝑌 ) ∈ Word 𝐵 ∧ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ∈ Word 𝐵 ) → ( 𝑀 Σg ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ) = ( ( 𝑀 Σg ( ( 𝑆 prefix 𝐹 ) ++ 𝑌 ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ) )
33 2 31 19 32 syl3anc ⊢ ( 𝜑 → ( 𝑀 Σg ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ) = ( ( 𝑀 Σg ( ( 𝑆 prefix 𝐹 ) ++ 𝑌 ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ) )
34 1 20 gsumccat ⊢ ( ( 𝑀 ∈ Mnd ∧ ( 𝑆 prefix 𝐹 ) ∈ Word 𝐵 ∧ 𝑌 ∈ Word 𝐵 ) → ( 𝑀 Σg ( ( 𝑆 prefix 𝐹 ) ++ 𝑌 ) ) = ( ( 𝑀 Σg ( 𝑆 prefix 𝐹 ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑌 ) ) )
35 2 15 7 34 syl3anc ⊢ ( 𝜑 → ( 𝑀 Σg ( ( 𝑆 prefix 𝐹 ) ++ 𝑌 ) ) = ( ( 𝑀 Σg ( 𝑆 prefix 𝐹 ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑌 ) ) )
36 35 oveq1d ⊢ ( 𝜑 → ( ( 𝑀 Σg ( ( 𝑆 prefix 𝐹 ) ++ 𝑌 ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ) = ( ( ( 𝑀 Σg ( 𝑆 prefix 𝐹 ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑌 ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ) )
37 29 33 36 3eqtrd ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑌 ⟩ ) ) = ( ( ( 𝑀 Σg ( 𝑆 prefix 𝐹 ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑌 ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ) )
38 10 26 37 3eqtr4d ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑋 ⟩ ) ) = ( 𝑀 Σg ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑌 ⟩ ) ) )