gsumccatOLD

Description: Obsolete version of gsumccat as of 13-Jan-2024. Homomorphic property of composites. (Contributed by Stefan O'Rear, 16-Aug-2015) (Revised by Mario Carneiro, 1-Oct-2015) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	gsumwcl.b	$⊢ B = {Base}_{G}$
	gsumsgrpccat.p	$⊢ \underset{˙}{+} = +_{G}$
Assertion	gsumccatOLD	$⊢ (G \in Mnd \land W \in Word B \land X \in Word B) \to \sum_{G} (W ++ X) = (\sum_{G}, W) \underset{˙}{+} (\sum_{G}, X)$

Proof

Step	Hyp	Ref	Expression
1		gsumwcl.b	$⊢ B = {Base}_{G}$
2		gsumsgrpccat.p	$⊢ \underset{˙}{+} = +_{G}$
3		oveq1	$⊢ W = \emptyset \to W ++ X = \emptyset ++ X$
4	3	oveq2d	$⊢ W = \emptyset \to \sum_{G} (W ++ X) = \sum_{G} (\emptyset ++ X)$
5		oveq2	$⊢ W = \emptyset \to \sum_{G} W = \sum_{G} \emptyset$
6		eqid	$⊢ 0_{G} = 0_{G}$
7	6	gsum0	$⊢ \sum_{G} \emptyset = 0_{G}$
8	5 7	eqtrdi	$⊢ W = \emptyset \to \sum_{G} W = 0_{G}$
9	8	oveq1d	$⊢ W = \emptyset \to (\sum_{G}, W) \underset{˙}{+} (\sum_{G}, X) = 0_{G} \underset{˙}{+} (\sum_{G}, X)$
10	4 9	eqeq12d	$⊢ W = \emptyset \to (\sum_{G} (W ++ X) = (\sum_{G}, W) \underset{˙}{+} (\sum_{G}, X) \leftrightarrow \sum_{G} (\emptyset ++ X) = 0_{G} \underset{˙}{+} (\sum_{G}, X))$
11		oveq2	$⊢ X = \emptyset \to W ++ X = W ++ \emptyset$
12	11	oveq2d	$⊢ X = \emptyset \to \sum_{G} (W ++ X) = \sum_{G} (W ++ \emptyset)$
13		oveq2	$⊢ X = \emptyset \to \sum_{G} X = \sum_{G} \emptyset$
14	13 7	eqtrdi	$⊢ X = \emptyset \to \sum_{G} X = 0_{G}$
15	14	oveq2d	$⊢ X = \emptyset \to (\sum_{G}, W) \underset{˙}{+} (\sum_{G}, X) = (\sum_{G}, W) \underset{˙}{+} 0_{G}$
16	12 15	eqeq12d	$⊢ X = \emptyset \to (\sum_{G} (W ++ X) = (\sum_{G}, W) \underset{˙}{+} (\sum_{G}, X) \leftrightarrow \sum_{G} (W ++ \emptyset) = (\sum_{G}, W) \underset{˙}{+} 0_{G})$
17		simpl1	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to G \in Mnd$
18		lennncl	$⊢ (W \in Word B \land W \neq \emptyset) \to \|W\| \in ℕ$
19	18	3ad2antl2	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land W \neq \emptyset) \to \|W\| \in ℕ$
20	19	adantrr	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|W\| \in ℕ$
21		lennncl	$⊢ (X \in Word B \land X \neq \emptyset) \to \|X\| \in ℕ$
22	21	3ad2antl3	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land X \neq \emptyset) \to \|X\| \in ℕ$
23	22	adantrl	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|X\| \in ℕ$
24	20 23	nnaddcld	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|W\| + \|X\| \in ℕ$
25		nnm1nn0	$⊢ \|W\| + \|X\| \in ℕ \to \|W\| + \|X\| - 1 \in ℕ_{0}$
26	24 25	syl	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|W\| + \|X\| - 1 \in ℕ_{0}$
27		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
28	26 27	eleqtrdi	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|W\| + \|X\| - 1 \in ℤ_{\geq 0}$
29		simpl2	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to W \in Word B$
30		simpl3	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to X \in Word B$
31		ccatcl	$⊢ (W \in Word B \land X \in Word B) \to W ++ X \in Word B$
32	29 30 31	syl2anc	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to W ++ X \in Word B$
33		wrdf	$⊢ W ++ X \in Word B \to (W ++ X) : (0 ..^\|W ++ X\|) ⟶ B$
34	32 33	syl	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to (W ++ X) : (0 ..^\|W ++ X\|) ⟶ B$
35		ccatlen	$⊢ (W \in Word B \land X \in Word B) \to \|W ++ X\| = \|W\| + \|X\|$
36	29 30 35	syl2anc	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|W ++ X\| = \|W\| + \|X\|$
37	36	oveq2d	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to (0 ..^\|W ++ X\|) = (0 ..^\|W\| + \|X\|)$
38	20	nnzd	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|W\| \in ℤ$
39	23	nnzd	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|X\| \in ℤ$
40	38 39	zaddcld	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|W\| + \|X\| \in ℤ$
41		fzoval	$⊢ \|W\| + \|X\| \in ℤ \to (0 ..^\|W\| + \|X\|) = (0 \dots \|W\| + \|X\| - 1)$
42	40 41	syl	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to (0 ..^\|W\| + \|X\|) = (0 \dots \|W\| + \|X\| - 1)$
43	37 42	eqtrd	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to (0 ..^\|W ++ X\|) = (0 \dots \|W\| + \|X\| - 1)$
44	43	feq2d	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to ((W ++ X) : (0 ..^\|W ++ X\|) ⟶ B \leftrightarrow (W ++ X) : (0 \dots \|W\| + \|X\| - 1) ⟶ B)$
45	34 44	mpbid	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to (W ++ X) : (0 \dots \|W\| + \|X\| - 1) ⟶ B$
46	1 2 17 28 45	gsumval2	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \sum_{G} (W ++ X) = seq 0 (\underset{˙}{+}, (W ++ X)) (\|W\| + \|X\| - 1)$
47		nnm1nn0	$⊢ \|W\| \in ℕ \to \|W\| - 1 \in ℕ_{0}$
48	20 47	syl	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|W\| - 1 \in ℕ_{0}$
49	48 27	eleqtrdi	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|W\| - 1 \in ℤ_{\geq 0}$
50		wrdf	$⊢ W \in Word B \to W : (0 ..^\|W\|) ⟶ B$
51	29 50	syl	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to W : (0 ..^\|W\|) ⟶ B$
52		fzoval	$⊢ \|W\| \in ℤ \to (0 ..^\|W\|) = (0 \dots \|W\| - 1)$
53	38 52	syl	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to (0 ..^\|W\|) = (0 \dots \|W\| - 1)$
54	53	feq2d	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to (W : (0 ..^\|W\|) ⟶ B \leftrightarrow W : (0 \dots \|W\| - 1) ⟶ B)$
55	51 54	mpbid	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to W : (0 \dots \|W\| - 1) ⟶ B$
56	1 2 17 49 55	gsumval2	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \sum_{G} W = seq 0 (\underset{˙}{+}, W) (\|W\| - 1)$
57		nnm1nn0	$⊢ \|X\| \in ℕ \to \|X\| - 1 \in ℕ_{0}$
58	23 57	syl	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|X\| - 1 \in ℕ_{0}$
59	58 27	eleqtrdi	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|X\| - 1 \in ℤ_{\geq 0}$
60		wrdf	$⊢ X \in Word B \to X : (0 ..^\|X\|) ⟶ B$
61	30 60	syl	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to X : (0 ..^\|X\|) ⟶ B$
62		fzoval	$⊢ \|X\| \in ℤ \to (0 ..^\|X\|) = (0 \dots \|X\| - 1)$
63	39 62	syl	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to (0 ..^\|X\|) = (0 \dots \|X\| - 1)$
64	63	feq2d	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to (X : (0 ..^\|X\|) ⟶ B \leftrightarrow X : (0 \dots \|X\| - 1) ⟶ B)$
65	61 64	mpbid	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to X : (0 \dots \|X\| - 1) ⟶ B$
66	1 2 17 59 65	gsumval2	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \sum_{G} X = seq 0 (\underset{˙}{+}, X) (\|X\| - 1)$
67	56 66	oveq12d	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to (\sum_{G}, W) \underset{˙}{+} (\sum_{G}, X) = seq 0 (\underset{˙}{+}, W) (\|W\| - 1) \underset{˙}{+} seq 0 (\underset{˙}{+}, X) (\|X\| - 1)$
68	1 2	mndcl	$⊢ (G \in Mnd \land x \in B \land y \in B) \to x \underset{˙}{+} y \in B$
69	68	3expb	$⊢ (G \in Mnd \land (x \in B \land y \in B)) \to x \underset{˙}{+} y \in B$
70	17 69	sylan	$⊢ (((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \land (x \in B \land y \in B)) \to x \underset{˙}{+} y \in B$
71	1 2	mndass	$⊢ (G \in Mnd \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
72	17 71	sylan	$⊢ (((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
73		uzid	$⊢ \|W\| \in ℤ \to \|W\| \in ℤ_{\geq \|W\|}$
74	38 73	syl	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|W\| \in ℤ_{\geq \|W\|}$
75		uzaddcl	$⊢ (\|W\| \in ℤ_{\geq \|W\|} \land \|X\| - 1 \in ℕ_{0}) \to \|W\| + \|X\| - 1 \in ℤ_{\geq \|W\|}$
76	74 58 75	syl2anc	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|W\| + \|X\| - 1 \in ℤ_{\geq \|W\|}$
77	20	nncnd	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|W\| \in ℂ$
78	23	nncnd	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|X\| \in ℂ$
79		1cnd	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to 1 \in ℂ$
80	77 78 79	addsubassd	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|W\| + \|X\| - 1 = \|W\| + \|X\| - 1$
81		ax-1cn	$⊢ 1 \in ℂ$
82		npcan	$⊢ (\|W\| \in ℂ \land 1 \in ℂ) \to \|W\| - 1 + 1 = \|W\|$
83	77 81 82	sylancl	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|W\| - 1 + 1 = \|W\|$
84	83	fveq2d	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to ℤ_{\geq (\|W\| - 1 + 1)} = ℤ_{\geq \|W\|}$
85	76 80 84	3eltr4d	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|W\| + \|X\| - 1 \in ℤ_{\geq (\|W\| - 1 + 1)}$
86	45	ffvelrnda	$⊢ (((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \land x \in (0 \dots \|W\| + \|X\| - 1)) \to (W ++ X) (x) \in B$
87	70 72 85 49 86	seqsplit	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to seq 0 (\underset{˙}{+}, (W ++ X)) (\|W\| + \|X\| - 1) = seq 0 (\underset{˙}{+}, (W ++ X)) (\|W\| - 1) \underset{˙}{+} seq (\|W\| - 1 + 1) (\underset{˙}{+}, (W ++ X)) (\|W\| + \|X\| - 1)$
88		simpll2	$⊢ (((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \land x \in (0 \dots \|W\| - 1)) \to W \in Word B$
89		simpll3	$⊢ (((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \land x \in (0 \dots \|W\| - 1)) \to X \in Word B$
90	53	eleq2d	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to (x \in (0 ..^\|W\|) \leftrightarrow x \in (0 \dots \|W\| - 1))$
91	90	biimpar	$⊢ (((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \land x \in (0 \dots \|W\| - 1)) \to x \in (0 ..^\|W\|)$
92		ccatval1	$⊢ (W \in Word B \land X \in Word B \land x \in (0 ..^\|W\|)) \to (W ++ X) (x) = W (x)$
93	88 89 91 92	syl3anc	$⊢ (((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \land x \in (0 \dots \|W\| - 1)) \to (W ++ X) (x) = W (x)$
94	49 93	seqfveq	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to seq 0 (\underset{˙}{+}, (W ++ X)) (\|W\| - 1) = seq 0 (\underset{˙}{+}, W) (\|W\| - 1)$
95	77	addid2d	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to 0 + \|W\| = \|W\|$
96	83 95	eqtr4d	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|W\| - 1 + 1 = 0 + \|W\|$
97	96	seqeq1d	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to seq (\|W\| - 1 + 1) (\underset{˙}{+}, (W ++ X)) = seq (0 + \|W\|) (\underset{˙}{+}, (W ++ X))$
98	77 78	addcomd	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|W\| + \|X\| = \|X\| + \|W\|$
99	98	oveq1d	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|W\| + \|X\| - 1 = \|X\| + \|W\| - 1$
100	78 77 79	addsubd	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|X\| + \|W\| - 1 = \|X\| - 1 + \|W\|$
101	99 100	eqtrd	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|W\| + \|X\| - 1 = \|X\| - 1 + \|W\|$
102	97 101	fveq12d	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to seq (\|W\| - 1 + 1) (\underset{˙}{+}, (W ++ X)) (\|W\| + \|X\| - 1) = seq (0 + \|W\|) (\underset{˙}{+}, (W ++ X)) (\|X\| - 1 + \|W\|)$
103		simpll2	$⊢ (((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \land x \in (0 \dots \|X\| - 1)) \to W \in Word B$
104		simpll3	$⊢ (((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \land x \in (0 \dots \|X\| - 1)) \to X \in Word B$
105	63	eleq2d	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to (x \in (0 ..^\|X\|) \leftrightarrow x \in (0 \dots \|X\| - 1))$
106	105	biimpar	$⊢ (((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \land x \in (0 \dots \|X\| - 1)) \to x \in (0 ..^\|X\|)$
107		ccatval3	$⊢ (W \in Word B \land X \in Word B \land x \in (0 ..^\|X\|)) \to (W ++ X) (x + \|W\|) = X (x)$
108	103 104 106 107	syl3anc	$⊢ (((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \land x \in (0 \dots \|X\| - 1)) \to (W ++ X) (x + \|W\|) = X (x)$
109	108	eqcomd	$⊢ (((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \land x \in (0 \dots \|X\| - 1)) \to X (x) = (W ++ X) (x + \|W\|)$
110	59 38 109	seqshft2	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to seq 0 (\underset{˙}{+}, X) (\|X\| - 1) = seq (0 + \|W\|) (\underset{˙}{+}, (W ++ X)) (\|X\| - 1 + \|W\|)$
111	102 110	eqtr4d	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to seq (\|W\| - 1 + 1) (\underset{˙}{+}, (W ++ X)) (\|W\| + \|X\| - 1) = seq 0 (\underset{˙}{+}, X) (\|X\| - 1)$
112	94 111	oveq12d	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to seq 0 (\underset{˙}{+}, (W ++ X)) (\|W\| - 1) \underset{˙}{+} seq (\|W\| - 1 + 1) (\underset{˙}{+}, (W ++ X)) (\|W\| + \|X\| - 1) = seq 0 (\underset{˙}{+}, W) (\|W\| - 1) \underset{˙}{+} seq 0 (\underset{˙}{+}, X) (\|X\| - 1)$
113	87 112	eqtrd	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to seq 0 (\underset{˙}{+}, (W ++ X)) (\|W\| + \|X\| - 1) = seq 0 (\underset{˙}{+}, W) (\|W\| - 1) \underset{˙}{+} seq 0 (\underset{˙}{+}, X) (\|X\| - 1)$
114	67 113	eqtr4d	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to (\sum_{G}, W) \underset{˙}{+} (\sum_{G}, X) = seq 0 (\underset{˙}{+}, (W ++ X)) (\|W\| + \|X\| - 1)$
115	46 114	eqtr4d	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \sum_{G} (W ++ X) = (\sum_{G}, W) \underset{˙}{+} (\sum_{G}, X)$
116	115	anassrs	$⊢ (((G \in Mnd \land W \in Word B \land X \in Word B) \land W \neq \emptyset) \land X \neq \emptyset) \to \sum_{G} (W ++ X) = (\sum_{G}, W) \underset{˙}{+} (\sum_{G}, X)$
117		simpl2	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land W \neq \emptyset) \to W \in Word B$
118		ccatrid	$⊢ W \in Word B \to W ++ \emptyset = W$
119	117 118	syl	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land W \neq \emptyset) \to W ++ \emptyset = W$
120	119	oveq2d	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land W \neq \emptyset) \to \sum_{G} (W ++ \emptyset) = \sum_{G} W$
121		simpl1	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land W \neq \emptyset) \to G \in Mnd$
122	1	gsumwcl	$⊢ (G \in Mnd \land W \in Word B) \to \sum_{G} W \in B$
123	122	3adant3	$⊢ (G \in Mnd \land W \in Word B \land X \in Word B) \to \sum_{G} W \in B$
124	123	adantr	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land W \neq \emptyset) \to \sum_{G} W \in B$
125	1 2 6	mndrid	$⊢ (G \in Mnd \land \sum_{G} W \in B) \to (\sum_{G}, W) \underset{˙}{+} 0_{G} = \sum_{G} W$
126	121 124 125	syl2anc	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land W \neq \emptyset) \to (\sum_{G}, W) \underset{˙}{+} 0_{G} = \sum_{G} W$
127	120 126	eqtr4d	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land W \neq \emptyset) \to \sum_{G} (W ++ \emptyset) = (\sum_{G}, W) \underset{˙}{+} 0_{G}$
128	16 116 127	pm2.61ne	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land W \neq \emptyset) \to \sum_{G} (W ++ X) = (\sum_{G}, W) \underset{˙}{+} (\sum_{G}, X)$
129		ccatlid	$⊢ X \in Word B \to \emptyset ++ X = X$
130	129	3ad2ant3	$⊢ (G \in Mnd \land W \in Word B \land X \in Word B) \to \emptyset ++ X = X$
131	130	oveq2d	$⊢ (G \in Mnd \land W \in Word B \land X \in Word B) \to \sum_{G} (\emptyset ++ X) = \sum_{G} X$
132		simp1	$⊢ (G \in Mnd \land W \in Word B \land X \in Word B) \to G \in Mnd$
133	1	gsumwcl	$⊢ (G \in Mnd \land X \in Word B) \to \sum_{G} X \in B$
134	1 2 6	mndlid	$⊢ (G \in Mnd \land \sum_{G} X \in B) \to 0_{G} \underset{˙}{+} (\sum_{G}, X) = \sum_{G} X$
135	132 133 134	3imp3i2an	$⊢ (G \in Mnd \land W \in Word B \land X \in Word B) \to 0_{G} \underset{˙}{+} (\sum_{G}, X) = \sum_{G} X$
136	131 135	eqtr4d	$⊢ (G \in Mnd \land W \in Word B \land X \in Word B) \to \sum_{G} (\emptyset ++ X) = 0_{G} \underset{˙}{+} (\sum_{G}, X)$
137	10 128 136	pm2.61ne	$⊢ (G \in Mnd \land W \in Word B \land X \in Word B) \to \sum_{G} (W ++ X) = (\sum_{G}, W) \underset{˙}{+} (\sum_{G}, X)$

Metamath Proof Explorer

Theorem gsumccatOLD

Proof