gsumsgrpccat

Description: Homomorphic property of not empty composites of a group sum over a semigroup. Formerly part of proof for gsumccat . (Contributed by AV, 26-Dec-2023)

	Ref	Expression
Hypotheses	gsumwcl.b	$⊢ B = {Base}_{G}$
	gsumsgrpccat.p	$⊢ \underset{˙}{+} = +_{G}$
Assertion	gsumsgrpccat	$⊢ (G \in Smgrp \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)$

Proof

Step	Hyp	Ref	Expression
1		gsumwcl.b	$⊢ B = {Base}_{G}$
2		gsumsgrpccat.p	$⊢ \underset{˙}{+} = +_{G}$
3		simp1	$⊢ (G \in Smgrp \land (W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to G \in Smgrp$
4		sgrpmgm	$⊢ G \in Smgrp \to G \in Mgm$
5	1 2	mgmcl	$⊢ (G \in Mgm \land x \in B \land y \in B) \to x \underset{˙}{+} y \in B$
6	4 5	syl3an1	$⊢ (G \in Smgrp \land x \in B \land y \in B) \to x \underset{˙}{+} y \in B$
7	6	3expb	$⊢ (G \in Smgrp \land (x \in B \land y \in B)) \to x \underset{˙}{+} y \in B$
8	3 7	sylan	$⊢ ((G \in Smgrp \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$
9	1 2	sgrpass	$⊢ (G \in Smgrp \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
10	3 9	sylan	$⊢ ((G \in Smgrp \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)$
11		lennncl	$⊢ (W \in Word B \land W \neq \emptyset) \to \|W\| \in ℕ$
12	11	ad2ant2r	$⊢ ((W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|W\| \in ℕ$
13	12	3adant1	$⊢ (G \in Smgrp \land (W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|W\| \in ℕ$
14	13	nnzd	$⊢ (G \in Smgrp \land (W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|W\| \in ℤ$
15	14	uzidd	$⊢ (G \in Smgrp \land (W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|W\| \in ℤ_{\geq \|W\|}$
16		lennncl	$⊢ (X \in Word B \land X \neq \emptyset) \to \|X\| \in ℕ$
17	16	ad2ant2l	$⊢ ((W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|X\| \in ℕ$
18	17	3adant1	$⊢ (G \in Smgrp \land (W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|X\| \in ℕ$
19		nnm1nn0	$⊢ \|X\| \in ℕ \to \|X\| - 1 \in ℕ_{0}$
20	18 19	syl	$⊢ (G \in Smgrp \land (W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|X\| - 1 \in ℕ_{0}$
21		uzaddcl	$⊢ (\|W\| \in ℤ_{\geq \|W\|} \land \|X\| - 1 \in ℕ_{0}) \to \|W\| + \|X\| - 1 \in ℤ_{\geq \|W\|}$
22	15 20 21	syl2anc	$⊢ (G \in Smgrp \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\|}$
23	13	nncnd	$⊢ (G \in Smgrp \land (W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|W\| \in ℂ$
24	18	nncnd	$⊢ (G \in Smgrp \land (W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|X\| \in ℂ$
25		1cnd	$⊢ (G \in Smgrp \land (W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to 1 \in ℂ$
26	23 24 25	addsubassd	$⊢ (G \in Smgrp \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$
27		ax-1cn	$⊢ 1 \in ℂ$
28		npcan	$⊢ (\|W\| \in ℂ \land 1 \in ℂ) \to \|W\| - 1 + 1 = \|W\|$
29	23 27 28	sylancl	$⊢ (G \in Smgrp \land (W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|W\| - 1 + 1 = \|W\|$
30	29	fveq2d	$⊢ (G \in Smgrp \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\|}$
31	22 26 30	3eltr4d	$⊢ (G \in Smgrp \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)}$
32		nnm1nn0	$⊢ \|W\| \in ℕ \to \|W\| - 1 \in ℕ_{0}$
33	13 32	syl	$⊢ (G \in Smgrp \land (W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|W\| - 1 \in ℕ_{0}$
34		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
35	33 34	eleqtrdi	$⊢ (G \in Smgrp \land (W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|W\| - 1 \in ℤ_{\geq 0}$
36		ccatcl	$⊢ (W \in Word B \land X \in Word B) \to W ++ X \in Word B$
37	36	3ad2ant2	$⊢ (G \in Smgrp \land (W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to W ++ X \in Word B$
38		wrdf	$⊢ W ++ X \in Word B \to (W ++ X) : (0 ..^\|W ++ X\|) ⟶ B$
39	37 38	syl	$⊢ (G \in Smgrp \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$
40		ccatlen	$⊢ (W \in Word B \land X \in Word B) \to \|W ++ X\| = \|W\| + \|X\|$
41	40	3ad2ant2	$⊢ (G \in Smgrp \land (W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|W ++ X\| = \|W\| + \|X\|$
42	41	oveq2d	$⊢ (G \in Smgrp \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\|)$
43	18	nnzd	$⊢ (G \in Smgrp \land (W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|X\| \in ℤ$
44	14 43	zaddcld	$⊢ (G \in Smgrp \land (W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|W\| + \|X\| \in ℤ$
45		fzoval	$⊢ \|W\| + \|X\| \in ℤ \to (0 ..^\|W\| + \|X\|) = (0 \dots \|W\| + \|X\| - 1)$
46	44 45	syl	$⊢ (G \in Smgrp \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)$
47	42 46	eqtrd	$⊢ (G \in Smgrp \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)$
48	47	feq2d	$⊢ (G \in Smgrp \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)$
49	39 48	mpbid	$⊢ (G \in Smgrp \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$
50	49	ffvelcdmda	$⊢ ((G \in Smgrp \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$
51	8 10 31 35 50	seqsplit	$⊢ (G \in Smgrp \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)$
52		simpl2l	$⊢ ((G \in Smgrp \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$
53		simpl2r	$⊢ ((G \in Smgrp \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$
54		fzoval	$⊢ \|W\| \in ℤ \to (0 ..^\|W\|) = (0 \dots \|W\| - 1)$
55	14 54	syl	$⊢ (G \in Smgrp \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)$
56	55	eleq2d	$⊢ (G \in Smgrp \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))$
57	56	biimpar	$⊢ ((G \in Smgrp \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\|)$
58		ccatval1	$⊢ (W \in Word B \land X \in Word B \land x \in (0 ..^\|W\|)) \to (W ++ X) (x) = W (x)$
59	52 53 57 58	syl3anc	$⊢ ((G \in Smgrp \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)$
60	35 59	seqfveq	$⊢ (G \in Smgrp \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)$
61	23	addlidd	$⊢ (G \in Smgrp \land (W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to 0 + \|W\| = \|W\|$
62	29 61	eqtr4d	$⊢ (G \in Smgrp \land (W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|W\| - 1 + 1 = 0 + \|W\|$
63	62	seqeq1d	$⊢ (G \in Smgrp \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))$
64	23 24	addcomd	$⊢ (G \in Smgrp \land (W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|W\| + \|X\| = \|X\| + \|W\|$
65	64	oveq1d	$⊢ (G \in Smgrp \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$
66	24 23 25	addsubd	$⊢ (G \in Smgrp \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\|$
67	65 66	eqtrd	$⊢ (G \in Smgrp \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\|$
68	63 67	fveq12d	$⊢ (G \in Smgrp \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\|)$
69	20 34	eleqtrdi	$⊢ (G \in Smgrp \land (W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|X\| - 1 \in ℤ_{\geq 0}$
70		simpl2l	$⊢ ((G \in Smgrp \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$
71		simpl2r	$⊢ ((G \in Smgrp \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$
72		fzoval	$⊢ \|X\| \in ℤ \to (0 ..^\|X\|) = (0 \dots \|X\| - 1)$
73	43 72	syl	$⊢ (G \in Smgrp \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)$
74	73	eleq2d	$⊢ (G \in Smgrp \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))$
75	74	biimpar	$⊢ ((G \in Smgrp \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\|)$
76		ccatval3	$⊢ (W \in Word B \land X \in Word B \land x \in (0 ..^\|X\|)) \to (W ++ X) (x + \|W\|) = X (x)$
77	70 71 75 76	syl3anc	$⊢ ((G \in Smgrp \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)$
78	77	eqcomd	$⊢ ((G \in Smgrp \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\|)$
79	69 14 78	seqshft2	$⊢ (G \in Smgrp \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\|)$
80	68 79	eqtr4d	$⊢ (G \in Smgrp \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)$
81	60 80	oveq12d	$⊢ (G \in Smgrp \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)$
82	51 81	eqtrd	$⊢ (G \in Smgrp \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)$
83	13 18	nnaddcld	$⊢ (G \in Smgrp \land (W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|W\| + \|X\| \in ℕ$
84		nnm1nn0	$⊢ \|W\| + \|X\| \in ℕ \to \|W\| + \|X\| - 1 \in ℕ_{0}$
85	83 84	syl	$⊢ (G \in Smgrp \land (W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to \|W\| + \|X\| - 1 \in ℕ_{0}$
86	85 34	eleqtrdi	$⊢ (G \in Smgrp \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}$
87	1 2 3 86 49	gsumval2	$⊢ (G \in Smgrp \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)$
88		simp2l	$⊢ (G \in Smgrp \land (W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to W \in Word B$
89		wrdf	$⊢ W \in Word B \to W : (0 ..^\|W\|) ⟶ B$
90	88 89	syl	$⊢ (G \in Smgrp \land (W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to W : (0 ..^\|W\|) ⟶ B$
91	55	feq2d	$⊢ (G \in Smgrp \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)$
92	90 91	mpbid	$⊢ (G \in Smgrp \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$
93	1 2 3 35 92	gsumval2	$⊢ (G \in Smgrp \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)$
94		simp2r	$⊢ (G \in Smgrp \land (W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to X \in Word B$
95		wrdf	$⊢ X \in Word B \to X : (0 ..^\|X\|) ⟶ B$
96	94 95	syl	$⊢ (G \in Smgrp \land (W \in Word B \land X \in Word B) \land (W \neq \emptyset \land X \neq \emptyset)) \to X : (0 ..^\|X\|) ⟶ B$
97	73	feq2d	$⊢ (G \in Smgrp \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)$
98	96 97	mpbid	$⊢ (G \in Smgrp \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$
99	1 2 3 69 98	gsumval2	$⊢ (G \in Smgrp \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)$
100	93 99	oveq12d	$⊢ (G \in Smgrp \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)$
101	82 87 100	3eqtr4d	$⊢ (G \in Smgrp \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)$

Metamath Proof Explorer

Theorem gsumsgrpccat

Proof