gsumwun

Description: In a commutative ring, a group sum of a word W of characters taken from two submonoids E and F can be written as a simple sum. (Contributed by Thierry Arnoux, 6-Oct-2025)

	Ref	Expression
Hypotheses	gsumwun.p	$⊢ \underset{˙}{+} = +_{M}$
	gsumwun.m	$⊢ φ \to M \in CMnd$
	gsumwun.e	$⊢ φ \to E \in SubMnd (M)$
	gsumwun.f	$⊢ φ \to F \in SubMnd (M)$
	gsumwun.w	$⊢ φ \to W \in Word (E \cup F)$
Assertion	gsumwun	$⊢ φ \to \exists e \in E \exists f \in F \sum_{M} W = e \underset{˙}{+} f$

Proof

Step	Hyp	Ref	Expression
1		gsumwun.p	$⊢ \underset{˙}{+} = +_{M}$
2		gsumwun.m	$⊢ φ \to M \in CMnd$
3		gsumwun.e	$⊢ φ \to E \in SubMnd (M)$
4		gsumwun.f	$⊢ φ \to F \in SubMnd (M)$
5		gsumwun.w	$⊢ φ \to W \in Word (E \cup F)$
6		oveq2	$⊢ v = \emptyset \to \sum_{M} v = \sum_{M} \emptyset$
7	6	eqeq1d	$⊢ v = \emptyset \to (\sum_{M} v = e \underset{˙}{+} f \leftrightarrow \sum_{M} \emptyset = e \underset{˙}{+} f)$
8	7	2rexbidv	$⊢ v = \emptyset \to (\exists e \in E \exists f \in F \sum_{M} v = e \underset{˙}{+} f \leftrightarrow \exists e \in E \exists f \in F \sum_{M} \emptyset = e \underset{˙}{+} f)$
9	8	imbi2d	$⊢ v = \emptyset \to ((φ \to \exists e \in E \exists f \in F \sum_{M} v = e \underset{˙}{+} f) \leftrightarrow (φ \to \exists e \in E \exists f \in F \sum_{M} \emptyset = e \underset{˙}{+} f))$
10		oveq2	$⊢ v = w \to \sum_{M} v = \sum_{M} w$
11	10	eqeq1d	$⊢ v = w \to (\sum_{M} v = e \underset{˙}{+} f \leftrightarrow \sum_{M} w = e \underset{˙}{+} f)$
12	11	2rexbidv	$⊢ v = w \to (\exists e \in E \exists f \in F \sum_{M} v = e \underset{˙}{+} f \leftrightarrow \exists e \in E \exists f \in F \sum_{M} w = e \underset{˙}{+} f)$
13	12	imbi2d	$⊢ v = w \to ((φ \to \exists e \in E \exists f \in F \sum_{M} v = e \underset{˙}{+} f) \leftrightarrow (φ \to \exists e \in E \exists f \in F \sum_{M} w = e \underset{˙}{+} f))$
14		oveq1	$⊢ e = i \to e \underset{˙}{+} f = i \underset{˙}{+} f$
15	14	eqeq2d	$⊢ e = i \to (\sum_{M} v = e \underset{˙}{+} f \leftrightarrow \sum_{M} v = i \underset{˙}{+} f)$
16		oveq2	$⊢ f = j \to i \underset{˙}{+} f = i \underset{˙}{+} j$
17	16	eqeq2d	$⊢ f = j \to (\sum_{M} v = i \underset{˙}{+} f \leftrightarrow \sum_{M} v = i \underset{˙}{+} j)$
18	15 17	cbvrex2vw	$⊢ \exists e \in E \exists f \in F \sum_{M} v = e \underset{˙}{+} f \leftrightarrow \exists i \in E \exists j \in F \sum_{M} v = i \underset{˙}{+} j$
19		oveq2	$⊢ v = w ++ ⟨“ x ”⟩ \to \sum_{M} v = \sum_{M} (w ++ ⟨“ x ”⟩)$
20	19	eqeq1d	$⊢ v = w ++ ⟨“ x ”⟩ \to (\sum_{M} v = i \underset{˙}{+} j \leftrightarrow \sum_{M} (w ++ ⟨“ x ”⟩) = i \underset{˙}{+} j)$
21	20	2rexbidv	$⊢ v = w ++ ⟨“ x ”⟩ \to (\exists i \in E \exists j \in F \sum_{M} v = i \underset{˙}{+} j \leftrightarrow \exists i \in E \exists j \in F \sum_{M} (w ++ ⟨“ x ”⟩) = i \underset{˙}{+} j)$
22	18 21	bitrid	$⊢ v = w ++ ⟨“ x ”⟩ \to (\exists e \in E \exists f \in F \sum_{M} v = e \underset{˙}{+} f \leftrightarrow \exists i \in E \exists j \in F \sum_{M} (w ++ ⟨“ x ”⟩) = i \underset{˙}{+} j)$
23	22	imbi2d	$⊢ v = w ++ ⟨“ x ”⟩ \to ((φ \to \exists e \in E \exists f \in F \sum_{M} v = e \underset{˙}{+} f) \leftrightarrow (φ \to \exists i \in E \exists j \in F \sum_{M} (w ++ ⟨“ x ”⟩) = i \underset{˙}{+} j))$
24		oveq2	$⊢ v = W \to \sum_{M} v = \sum_{M} W$
25	24	eqeq1d	$⊢ v = W \to (\sum_{M} v = e \underset{˙}{+} f \leftrightarrow \sum_{M} W = e \underset{˙}{+} f)$
26	25	2rexbidv	$⊢ v = W \to (\exists e \in E \exists f \in F \sum_{M} v = e \underset{˙}{+} f \leftrightarrow \exists e \in E \exists f \in F \sum_{M} W = e \underset{˙}{+} f)$
27	26	imbi2d	$⊢ v = W \to ((φ \to \exists e \in E \exists f \in F \sum_{M} v = e \underset{˙}{+} f) \leftrightarrow (φ \to \exists e \in E \exists f \in F \sum_{M} W = e \underset{˙}{+} f))$
28		oveq1	$⊢ e = 0_{M} \to e \underset{˙}{+} f = 0_{M} \underset{˙}{+} f$
29	28	eqeq2d	$⊢ e = 0_{M} \to (\sum_{M} \emptyset = e \underset{˙}{+} f \leftrightarrow \sum_{M} \emptyset = 0_{M} \underset{˙}{+} f)$
30		oveq2	$⊢ f = 0_{M} \to 0_{M} \underset{˙}{+} f = 0_{M} \underset{˙}{+} 0_{M}$
31	30	eqeq2d	$⊢ f = 0_{M} \to (\sum_{M} \emptyset = 0_{M} \underset{˙}{+} f \leftrightarrow \sum_{M} \emptyset = 0_{M} \underset{˙}{+} 0_{M})$
32		eqid	$⊢ 0_{M} = 0_{M}$
33	32	subm0cl	$⊢ E \in SubMnd (M) \to 0_{M} \in E$
34	3 33	syl	$⊢ φ \to 0_{M} \in E$
35	32	subm0cl	$⊢ F \in SubMnd (M) \to 0_{M} \in F$
36	4 35	syl	$⊢ φ \to 0_{M} \in F$
37	32	gsum0	$⊢ \sum_{M} \emptyset = 0_{M}$
38	2	cmnmndd	$⊢ φ \to M \in Mnd$
39		eqid	$⊢ {Base}_{M} = {Base}_{M}$
40	39 32	mndidcl	$⊢ M \in Mnd \to 0_{M} \in {Base}_{M}$
41	39 1 32	mndlid	$⊢ (M \in Mnd \land 0_{M} \in {Base}_{M}) \to 0_{M} \underset{˙}{+} 0_{M} = 0_{M}$
42	38 40 41	syl2anc2	$⊢ φ \to 0_{M} \underset{˙}{+} 0_{M} = 0_{M}$
43	37 42	eqtr4id	$⊢ φ \to \sum_{M} \emptyset = 0_{M} \underset{˙}{+} 0_{M}$
44	29 31 34 36 43	2rspcedvdw	$⊢ φ \to \exists e \in E \exists f \in F \sum_{M} \emptyset = e \underset{˙}{+} f$
45		oveq1	$⊢ i = e \underset{˙}{+} x \to i \underset{˙}{+} j = (e \underset{˙}{+} x) \underset{˙}{+} j$
46	45	eqeq2d	$⊢ i = e \underset{˙}{+} x \to (\sum_{M} (w ++ ⟨“ x ”⟩) = i \underset{˙}{+} j \leftrightarrow \sum_{M} (w ++ ⟨“ x ”⟩) = (e \underset{˙}{+} x) \underset{˙}{+} j)$
47		oveq2	$⊢ j = f \to (e \underset{˙}{+} x) \underset{˙}{+} j = (e \underset{˙}{+} x) \underset{˙}{+} f$
48	47	eqeq2d	$⊢ j = f \to (\sum_{M} (w ++ ⟨“ x ”⟩) = (e \underset{˙}{+} x) \underset{˙}{+} j \leftrightarrow \sum_{M} (w ++ ⟨“ x ”⟩) = (e \underset{˙}{+} x) \underset{˙}{+} f)$
49	3	ad6antr	$⊢ ((((((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land e \in E) \land f \in F) \land \sum_{M} w = e \underset{˙}{+} f) \land x \in E) \to E \in SubMnd (M)$
50		simp-4r	$⊢ ((((((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land e \in E) \land f \in F) \land \sum_{M} w = e \underset{˙}{+} f) \land x \in E) \to e \in E$
51		simpr	$⊢ ((((((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land e \in E) \land f \in F) \land \sum_{M} w = e \underset{˙}{+} f) \land x \in E) \to x \in E$
52	1 49 50 51	submcld	$⊢ ((((((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land e \in E) \land f \in F) \land \sum_{M} w = e \underset{˙}{+} f) \land x \in E) \to e \underset{˙}{+} x \in E$
53		simpllr	$⊢ ((((((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land e \in E) \land f \in F) \land \sum_{M} w = e \underset{˙}{+} f) \land x \in E) \to f \in F$
54	38	ad5antr	$⊢ (((((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land e \in E) \land f \in F) \land \sum_{M} w = e \underset{˙}{+} f) \to M \in Mnd$
55	39	submss	$⊢ E \in SubMnd (M) \to E \subseteq {Base}_{M}$
56	3 55	syl	$⊢ φ \to E \subseteq {Base}_{M}$
57	39	submss	$⊢ F \in SubMnd (M) \to F \subseteq {Base}_{M}$
58	4 57	syl	$⊢ φ \to F \subseteq {Base}_{M}$
59	56 58	unssd	$⊢ φ \to E \cup F \subseteq {Base}_{M}$
60		sswrd	$⊢ E \cup F \subseteq {Base}_{M} \to Word (E \cup F) \subseteq Word {Base}_{M}$
61	59 60	syl	$⊢ φ \to Word (E \cup F) \subseteq Word {Base}_{M}$
62	61	sselda	$⊢ (φ \land w \in Word (E \cup F)) \to w \in Word {Base}_{M}$
63	62	ad4antr	$⊢ (((((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land e \in E) \land f \in F) \land \sum_{M} w = e \underset{˙}{+} f) \to w \in Word {Base}_{M}$
64	59	adantr	$⊢ (φ \land w \in Word (E \cup F)) \to E \cup F \subseteq {Base}_{M}$
65	64	sselda	$⊢ ((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \to x \in {Base}_{M}$
66	65	ad3antrrr	$⊢ (((((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land e \in E) \land f \in F) \land \sum_{M} w = e \underset{˙}{+} f) \to x \in {Base}_{M}$
67	39 1	gsumccatsn	$⊢ (M \in Mnd \land w \in Word {Base}_{M} \land x \in {Base}_{M}) \to \sum_{M} (w ++ ⟨“ x ”⟩) = (\sum_{M}, w) \underset{˙}{+} x$
68	54 63 66 67	syl3anc	$⊢ (((((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land e \in E) \land f \in F) \land \sum_{M} w = e \underset{˙}{+} f) \to \sum_{M} (w ++ ⟨“ x ”⟩) = (\sum_{M}, w) \underset{˙}{+} x$
69		simpr	$⊢ (((((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land e \in E) \land f \in F) \land \sum_{M} w = e \underset{˙}{+} f) \to \sum_{M} w = e \underset{˙}{+} f$
70	69	oveq1d	$⊢ (((((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land e \in E) \land f \in F) \land \sum_{M} w = e \underset{˙}{+} f) \to (\sum_{M}, w) \underset{˙}{+} x = (e \underset{˙}{+} f) \underset{˙}{+} x$
71	56	ad2antrr	$⊢ ((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \to E \subseteq {Base}_{M}$
72	71	sselda	$⊢ (((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land e \in E) \to e \in {Base}_{M}$
73	72	ad2antrr	$⊢ (((((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land e \in E) \land f \in F) \land \sum_{M} w = e \underset{˙}{+} f) \to e \in {Base}_{M}$
74	58	ad3antrrr	$⊢ (((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land e \in E) \to F \subseteq {Base}_{M}$
75	74	sselda	$⊢ ((((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land e \in E) \land f \in F) \to f \in {Base}_{M}$
76	75	adantr	$⊢ (((((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land e \in E) \land f \in F) \land \sum_{M} w = e \underset{˙}{+} f) \to f \in {Base}_{M}$
77	2	ad5antr	$⊢ (((((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land e \in E) \land f \in F) \land \sum_{M} w = e \underset{˙}{+} f) \to M \in CMnd$
78	39 1	cmncom	$⊢ (M \in CMnd \land f \in {Base}_{M} \land x \in {Base}_{M}) \to f \underset{˙}{+} x = x \underset{˙}{+} f$
79	77 76 66 78	syl3anc	$⊢ (((((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land e \in E) \land f \in F) \land \sum_{M} w = e \underset{˙}{+} f) \to f \underset{˙}{+} x = x \underset{˙}{+} f$
80	39 1 54 73 76 66 79	mnd32g	$⊢ (((((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land e \in E) \land f \in F) \land \sum_{M} w = e \underset{˙}{+} f) \to (e \underset{˙}{+} f) \underset{˙}{+} x = (e \underset{˙}{+} x) \underset{˙}{+} f$
81	68 70 80	3eqtrd	$⊢ (((((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land e \in E) \land f \in F) \land \sum_{M} w = e \underset{˙}{+} f) \to \sum_{M} (w ++ ⟨“ x ”⟩) = (e \underset{˙}{+} x) \underset{˙}{+} f$
82	81	adantr	$⊢ ((((((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land e \in E) \land f \in F) \land \sum_{M} w = e \underset{˙}{+} f) \land x \in E) \to \sum_{M} (w ++ ⟨“ x ”⟩) = (e \underset{˙}{+} x) \underset{˙}{+} f$
83	46 48 52 53 82	2rspcedvdw	$⊢ ((((((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land e \in E) \land f \in F) \land \sum_{M} w = e \underset{˙}{+} f) \land x \in E) \to \exists i \in E \exists j \in F \sum_{M} (w ++ ⟨“ x ”⟩) = i \underset{˙}{+} j$
84		oveq1	$⊢ i = e \to i \underset{˙}{+} j = e \underset{˙}{+} j$
85	84	eqeq2d	$⊢ i = e \to (\sum_{M} (w ++ ⟨“ x ”⟩) = i \underset{˙}{+} j \leftrightarrow \sum_{M} (w ++ ⟨“ x ”⟩) = e \underset{˙}{+} j)$
86		oveq2	$⊢ j = f \underset{˙}{+} x \to e \underset{˙}{+} j = e \underset{˙}{+} (f \underset{˙}{+} x)$
87	86	eqeq2d	$⊢ j = f \underset{˙}{+} x \to (\sum_{M} (w ++ ⟨“ x ”⟩) = e \underset{˙}{+} j \leftrightarrow \sum_{M} (w ++ ⟨“ x ”⟩) = e \underset{˙}{+} (f \underset{˙}{+} x))$
88		simp-4r	$⊢ ((((((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land e \in E) \land f \in F) \land \sum_{M} w = e \underset{˙}{+} f) \land x \in F) \to e \in E$
89	4	ad6antr	$⊢ ((((((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land e \in E) \land f \in F) \land \sum_{M} w = e \underset{˙}{+} f) \land x \in F) \to F \in SubMnd (M)$
90		simpllr	$⊢ ((((((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land e \in E) \land f \in F) \land \sum_{M} w = e \underset{˙}{+} f) \land x \in F) \to f \in F$
91		simpr	$⊢ ((((((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land e \in E) \land f \in F) \land \sum_{M} w = e \underset{˙}{+} f) \land x \in F) \to x \in F$
92	1 89 90 91	submcld	$⊢ ((((((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land e \in E) \land f \in F) \land \sum_{M} w = e \underset{˙}{+} f) \land x \in F) \to f \underset{˙}{+} x \in F$
93	39 1 54 73 76 66	mndassd	$⊢ (((((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land e \in E) \land f \in F) \land \sum_{M} w = e \underset{˙}{+} f) \to (e \underset{˙}{+} f) \underset{˙}{+} x = e \underset{˙}{+} (f \underset{˙}{+} x)$
94	68 70 93	3eqtrd	$⊢ (((((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land e \in E) \land f \in F) \land \sum_{M} w = e \underset{˙}{+} f) \to \sum_{M} (w ++ ⟨“ x ”⟩) = e \underset{˙}{+} (f \underset{˙}{+} x)$
95	94	adantr	$⊢ ((((((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land e \in E) \land f \in F) \land \sum_{M} w = e \underset{˙}{+} f) \land x \in F) \to \sum_{M} (w ++ ⟨“ x ”⟩) = e \underset{˙}{+} (f \underset{˙}{+} x)$
96	85 87 88 92 95	2rspcedvdw	$⊢ ((((((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land e \in E) \land f \in F) \land \sum_{M} w = e \underset{˙}{+} f) \land x \in F) \to \exists i \in E \exists j \in F \sum_{M} (w ++ ⟨“ x ”⟩) = i \underset{˙}{+} j$
97		elun	$⊢ x \in (E \cup F) \leftrightarrow (x \in E \lor x \in F)$
98	97	biimpi	$⊢ x \in (E \cup F) \to (x \in E \lor x \in F)$
99	98	ad4antlr	$⊢ (((((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land e \in E) \land f \in F) \land \sum_{M} w = e \underset{˙}{+} f) \to (x \in E \lor x \in F)$
100	83 96 99	mpjaodan	$⊢ (((((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land e \in E) \land f \in F) \land \sum_{M} w = e \underset{˙}{+} f) \to \exists i \in E \exists j \in F \sum_{M} (w ++ ⟨“ x ”⟩) = i \underset{˙}{+} j$
101	100	r19.29ffa	$⊢ (((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \land \exists e \in E \exists f \in F \sum_{M} w = e \underset{˙}{+} f) \to \exists i \in E \exists j \in F \sum_{M} (w ++ ⟨“ x ”⟩) = i \underset{˙}{+} j$
102	101	ex	$⊢ ((φ \land w \in Word (E \cup F)) \land x \in (E \cup F)) \to (\exists e \in E \exists f \in F \sum_{M} w = e \underset{˙}{+} f \to \exists i \in E \exists j \in F \sum_{M} (w ++ ⟨“ x ”⟩) = i \underset{˙}{+} j)$
103	102	expl	$⊢ φ \to ((w \in Word (E \cup F) \land x \in (E \cup F)) \to (\exists e \in E \exists f \in F \sum_{M} w = e \underset{˙}{+} f \to \exists i \in E \exists j \in F \sum_{M} (w ++ ⟨“ x ”⟩) = i \underset{˙}{+} j))$
104	103	com12	$⊢ (w \in Word (E \cup F) \land x \in (E \cup F)) \to (φ \to (\exists e \in E \exists f \in F \sum_{M} w = e \underset{˙}{+} f \to \exists i \in E \exists j \in F \sum_{M} (w ++ ⟨“ x ”⟩) = i \underset{˙}{+} j))$
105	104	a2d	$⊢ (w \in Word (E \cup F) \land x \in (E \cup F)) \to ((φ \to \exists e \in E \exists f \in F \sum_{M} w = e \underset{˙}{+} f) \to (φ \to \exists i \in E \exists j \in F \sum_{M} (w ++ ⟨“ x ”⟩) = i \underset{˙}{+} j))$
106	9 13 23 27 44 105	wrdind	$⊢ W \in Word (E \cup F) \to (φ \to \exists e \in E \exists f \in F \sum_{M} W = e \underset{˙}{+} f)$
107	5 106	mpcom	$⊢ φ \to \exists e \in E \exists f \in F \sum_{M} W = e \underset{˙}{+} f$

Metamath Proof Explorer

Theorem gsumwun

Proof