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 ⟨ 𝐹 , 𝑇 , 𝑌 ⟩ ) ) )