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	$⊢ φ \to M \in Mnd$
	gsumspl.s	$⊢ φ \to S \in Word B$
	gsumspl.f	$⊢ φ \to F \in (0 \dots T)$
	gsumspl.t	$⊢ φ \to T \in (0 \dots \|S\|)$
	gsumspl.x	$⊢ φ \to X \in Word B$
	gsumspl.y	$⊢ φ \to Y \in Word B$
	gsumspl.eq	$⊢ φ \to \sum_{M} X = \sum_{M} Y$
Assertion	gsumspl	$⊢ φ \to \sum_{M} (S splice ⟨F, T, X⟩) = \sum_{M} (S splice ⟨F, T, Y⟩)$

Proof

Step	Hyp	Ref	Expression
1		gsumspl.b	$⊢ B = {Base}_{M}$
2		gsumspl.m	$⊢ φ \to M \in Mnd$
3		gsumspl.s	$⊢ φ \to S \in Word B$
4		gsumspl.f	$⊢ φ \to F \in (0 \dots T)$
5		gsumspl.t	$⊢ φ \to T \in (0 \dots \|S\|)$
6		gsumspl.x	$⊢ φ \to X \in Word B$
7		gsumspl.y	$⊢ φ \to Y \in Word B$
8		gsumspl.eq	$⊢ φ \to \sum_{M} X = \sum_{M} Y$
9	8	oveq2d	$⊢ φ \to (\sum_{M}, (S prefix F)) +_{M} (\sum_{M}, X) = (\sum_{M}, (S prefix F)) +_{M} (\sum_{M}, Y)$
10	9	oveq1d	$⊢ φ \to ((\sum_{M}, (S prefix F)) +_{M} (\sum_{M}, X)) +_{M} (\sum_{M}, (S substr ⟨T, \|S\|⟩)) = ((\sum_{M}, (S prefix F)) +_{M} (\sum_{M}, Y)) +_{M} (\sum_{M}, (S substr ⟨T, \|S\|⟩))$
11		splval	$⊢ (S \in Word B \land (F \in (0 \dots T) \land T \in (0 \dots \|S\|) \land X \in Word B)) \to S splice ⟨F, T, X⟩ = ((S prefix F) ++ X) ++ (S substr ⟨T, \|S\|⟩)$
12	3 4 5 6 11	syl13anc	$⊢ φ \to S splice ⟨F, T, X⟩ = ((S prefix F) ++ X) ++ (S substr ⟨T, \|S\|⟩)$
13	12	oveq2d	$⊢ φ \to \sum_{M} (S splice ⟨F, T, X⟩) = \sum_{M} (((S prefix F) ++ X) ++ (S substr ⟨T, \|S\|⟩))$
14		pfxcl	$⊢ S \in Word B \to S prefix F \in Word B$
15	3 14	syl	$⊢ φ \to S prefix F \in Word B$
16		ccatcl	$⊢ (S prefix F \in Word B \land X \in Word B) \to (S prefix F) ++ X \in Word B$
17	15 6 16	syl2anc	$⊢ φ \to (S prefix F) ++ X \in Word B$
18		swrdcl	$⊢ S \in Word B \to S substr ⟨T, \|S\|⟩ \in Word B$
19	3 18	syl	$⊢ φ \to S substr ⟨T, \|S\|⟩ \in Word B$
20		eqid	$⊢ +_{M} = +_{M}$
21	1 20	gsumccat	$⊢ (M \in Mnd \land (S prefix F) ++ X \in Word B \land S substr ⟨T, \|S\|⟩ \in Word B) \to \sum_{M} (((S prefix F) ++ X) ++ (S substr ⟨T, \|S\|⟩)) = (\sum_{M}, ((S prefix F) ++ X)) +_{M} (\sum_{M}, (S substr ⟨T, \|S\|⟩))$
22	2 17 19 21	syl3anc	$⊢ φ \to \sum_{M} (((S prefix F) ++ X) ++ (S substr ⟨T, \|S\|⟩)) = (\sum_{M}, ((S prefix F) ++ X)) +_{M} (\sum_{M}, (S substr ⟨T, \|S\|⟩))$
23	1 20	gsumccat	$⊢ (M \in Mnd \land S prefix F \in Word B \land X \in Word B) \to \sum_{M} ((S prefix F) ++ X) = (\sum_{M}, (S prefix F)) +_{M} (\sum_{M}, X)$
24	2 15 6 23	syl3anc	$⊢ φ \to \sum_{M} ((S prefix F) ++ X) = (\sum_{M}, (S prefix F)) +_{M} (\sum_{M}, X)$
25	24	oveq1d	$⊢ φ \to (\sum_{M}, ((S prefix F) ++ X)) +_{M} (\sum_{M}, (S substr ⟨T, \|S\|⟩)) = ((\sum_{M}, (S prefix F)) +_{M} (\sum_{M}, X)) +_{M} (\sum_{M}, (S substr ⟨T, \|S\|⟩))$
26	13 22 25	3eqtrd	$⊢ φ \to \sum_{M} (S splice ⟨F, T, X⟩) = ((\sum_{M}, (S prefix F)) +_{M} (\sum_{M}, X)) +_{M} (\sum_{M}, (S substr ⟨T, \|S\|⟩))$
27		splval	$⊢ (S \in Word B \land (F \in (0 \dots T) \land T \in (0 \dots \|S\|) \land Y \in Word B)) \to S splice ⟨F, T, Y⟩ = ((S prefix F) ++ Y) ++ (S substr ⟨T, \|S\|⟩)$
28	3 4 5 7 27	syl13anc	$⊢ φ \to S splice ⟨F, T, Y⟩ = ((S prefix F) ++ Y) ++ (S substr ⟨T, \|S\|⟩)$
29	28	oveq2d	$⊢ φ \to \sum_{M} (S splice ⟨F, T, Y⟩) = \sum_{M} (((S prefix F) ++ Y) ++ (S substr ⟨T, \|S\|⟩))$
30		ccatcl	$⊢ (S prefix F \in Word B \land Y \in Word B) \to (S prefix F) ++ Y \in Word B$
31	15 7 30	syl2anc	$⊢ φ \to (S prefix F) ++ Y \in Word B$
32	1 20	gsumccat	$⊢ (M \in Mnd \land (S prefix F) ++ Y \in Word B \land S substr ⟨T, \|S\|⟩ \in Word B) \to \sum_{M} (((S prefix F) ++ Y) ++ (S substr ⟨T, \|S\|⟩)) = (\sum_{M}, ((S prefix F) ++ Y)) +_{M} (\sum_{M}, (S substr ⟨T, \|S\|⟩))$
33	2 31 19 32	syl3anc	$⊢ φ \to \sum_{M} (((S prefix F) ++ Y) ++ (S substr ⟨T, \|S\|⟩)) = (\sum_{M}, ((S prefix F) ++ Y)) +_{M} (\sum_{M}, (S substr ⟨T, \|S\|⟩))$
34	1 20	gsumccat	$⊢ (M \in Mnd \land S prefix F \in Word B \land Y \in Word B) \to \sum_{M} ((S prefix F) ++ Y) = (\sum_{M}, (S prefix F)) +_{M} (\sum_{M}, Y)$
35	2 15 7 34	syl3anc	$⊢ φ \to \sum_{M} ((S prefix F) ++ Y) = (\sum_{M}, (S prefix F)) +_{M} (\sum_{M}, Y)$
36	35	oveq1d	$⊢ φ \to (\sum_{M}, ((S prefix F) ++ Y)) +_{M} (\sum_{M}, (S substr ⟨T, \|S\|⟩)) = ((\sum_{M}, (S prefix F)) +_{M} (\sum_{M}, Y)) +_{M} (\sum_{M}, (S substr ⟨T, \|S\|⟩))$
37	29 33 36	3eqtrd	$⊢ φ \to \sum_{M} (S splice ⟨F, T, Y⟩) = ((\sum_{M}, (S prefix F)) +_{M} (\sum_{M}, Y)) +_{M} (\sum_{M}, (S substr ⟨T, \|S\|⟩))$
38	10 26 37	3eqtr4d	$⊢ φ \to \sum_{M} (S splice ⟨F, T, X⟩) = \sum_{M} (S splice ⟨F, T, Y⟩)$

Metamath Proof Explorer

Theorem gsumspl

Proof