Theorem 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	⊢ + = ( +g ‘ 𝑀 )
	gsumwun.m	⊢ ( 𝜑 → 𝑀 ∈ CMnd )
	gsumwun.e	⊢ ( 𝜑 → 𝐸 ∈ ( SubMnd ‘ 𝑀 ) )
	gsumwun.f	⊢ ( 𝜑 → 𝐹 ∈ ( SubMnd ‘ 𝑀 ) )
	gsumwun.w	⊢ ( 𝜑 → 𝑊 ∈ Word ( 𝐸 ∪ 𝐹 ) )
Assertion	gsumwun	⊢ ( 𝜑 → ∃ 𝑒 ∈ 𝐸 ∃ 𝑓 ∈ 𝐹 ( 𝑀 Σg 𝑊 ) = ( 𝑒 + 𝑓 ) )

Proof

Step	Hyp	Ref	Expression
1		gsumwun.p	⊢ + = ( +g ‘ 𝑀 )
2		gsumwun.m	⊢ ( 𝜑 → 𝑀 ∈ CMnd )
3		gsumwun.e	⊢ ( 𝜑 → 𝐸 ∈ ( SubMnd ‘ 𝑀 ) )
4		gsumwun.f	⊢ ( 𝜑 → 𝐹 ∈ ( SubMnd ‘ 𝑀 ) )
5		gsumwun.w	⊢ ( 𝜑 → 𝑊 ∈ Word ( 𝐸 ∪ 𝐹 ) )
6		oveq2	⊢ ( 𝑣 = ∅ → ( 𝑀 Σg 𝑣 ) = ( 𝑀 Σg ∅ ) )
7	6	eqeq1d	⊢ ( 𝑣 = ∅ → ( ( 𝑀 Σg 𝑣 ) = ( 𝑒 + 𝑓 ) ↔ ( 𝑀 Σg ∅ ) = ( 𝑒 + 𝑓 ) ) )
8	7	2rexbidv	⊢ ( 𝑣 = ∅ → ( ∃ 𝑒 ∈ 𝐸 ∃ 𝑓 ∈ 𝐹 ( 𝑀 Σg 𝑣 ) = ( 𝑒 + 𝑓 ) ↔ ∃ 𝑒 ∈ 𝐸 ∃ 𝑓 ∈ 𝐹 ( 𝑀 Σg ∅ ) = ( 𝑒 + 𝑓 ) ) )
9	8	imbi2d	⊢ ( 𝑣 = ∅ → ( ( 𝜑 → ∃ 𝑒 ∈ 𝐸 ∃ 𝑓 ∈ 𝐹 ( 𝑀 Σg 𝑣 ) = ( 𝑒 + 𝑓 ) ) ↔ ( 𝜑 → ∃ 𝑒 ∈ 𝐸 ∃ 𝑓 ∈ 𝐹 ( 𝑀 Σg ∅ ) = ( 𝑒 + 𝑓 ) ) ) )
10		oveq2	⊢ ( 𝑣 = 𝑤 → ( 𝑀 Σg 𝑣 ) = ( 𝑀 Σg 𝑤 ) )
11	10	eqeq1d	⊢ ( 𝑣 = 𝑤 → ( ( 𝑀 Σg 𝑣 ) = ( 𝑒 + 𝑓 ) ↔ ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) )
12	11	2rexbidv	⊢ ( 𝑣 = 𝑤 → ( ∃ 𝑒 ∈ 𝐸 ∃ 𝑓 ∈ 𝐹 ( 𝑀 Σg 𝑣 ) = ( 𝑒 + 𝑓 ) ↔ ∃ 𝑒 ∈ 𝐸 ∃ 𝑓 ∈ 𝐹 ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) )
13	12	imbi2d	⊢ ( 𝑣 = 𝑤 → ( ( 𝜑 → ∃ 𝑒 ∈ 𝐸 ∃ 𝑓 ∈ 𝐹 ( 𝑀 Σg 𝑣 ) = ( 𝑒 + 𝑓 ) ) ↔ ( 𝜑 → ∃ 𝑒 ∈ 𝐸 ∃ 𝑓 ∈ 𝐹 ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) ) )
14		oveq1	⊢ ( 𝑒 = 𝑖 → ( 𝑒 + 𝑓 ) = ( 𝑖 + 𝑓 ) )
15	14	eqeq2d	⊢ ( 𝑒 = 𝑖 → ( ( 𝑀 Σg 𝑣 ) = ( 𝑒 + 𝑓 ) ↔ ( 𝑀 Σg 𝑣 ) = ( 𝑖 + 𝑓 ) ) )
16		oveq2	⊢ ( 𝑓 = 𝑗 → ( 𝑖 + 𝑓 ) = ( 𝑖 + 𝑗 ) )
17	16	eqeq2d	⊢ ( 𝑓 = 𝑗 → ( ( 𝑀 Σg 𝑣 ) = ( 𝑖 + 𝑓 ) ↔ ( 𝑀 Σg 𝑣 ) = ( 𝑖 + 𝑗 ) ) )
18	15 17	cbvrex2vw	⊢ ( ∃ 𝑒 ∈ 𝐸 ∃ 𝑓 ∈ 𝐹 ( 𝑀 Σg 𝑣 ) = ( 𝑒 + 𝑓 ) ↔ ∃ 𝑖 ∈ 𝐸 ∃ 𝑗 ∈ 𝐹 ( 𝑀 Σg 𝑣 ) = ( 𝑖 + 𝑗 ) )
19		oveq2	⊢ ( 𝑣 = ( 𝑤 ++ ⟨“ 𝑥 ”⟩ ) → ( 𝑀 Σg 𝑣 ) = ( 𝑀 Σg ( 𝑤 ++ ⟨“ 𝑥 ”⟩ ) ) )
20	19	eqeq1d	⊢ ( 𝑣 = ( 𝑤 ++ ⟨“ 𝑥 ”⟩ ) → ( ( 𝑀 Σg 𝑣 ) = ( 𝑖 + 𝑗 ) ↔ ( 𝑀 Σg ( 𝑤 ++ ⟨“ 𝑥 ”⟩ ) ) = ( 𝑖 + 𝑗 ) ) )
21	20	2rexbidv	⊢ ( 𝑣 = ( 𝑤 ++ ⟨“ 𝑥 ”⟩ ) → ( ∃ 𝑖 ∈ 𝐸 ∃ 𝑗 ∈ 𝐹 ( 𝑀 Σg 𝑣 ) = ( 𝑖 + 𝑗 ) ↔ ∃ 𝑖 ∈ 𝐸 ∃ 𝑗 ∈ 𝐹 ( 𝑀 Σg ( 𝑤 ++ ⟨“ 𝑥 ”⟩ ) ) = ( 𝑖 + 𝑗 ) ) )
22	18 21	bitrid	⊢ ( 𝑣 = ( 𝑤 ++ ⟨“ 𝑥 ”⟩ ) → ( ∃ 𝑒 ∈ 𝐸 ∃ 𝑓 ∈ 𝐹 ( 𝑀 Σg 𝑣 ) = ( 𝑒 + 𝑓 ) ↔ ∃ 𝑖 ∈ 𝐸 ∃ 𝑗 ∈ 𝐹 ( 𝑀 Σg ( 𝑤 ++ ⟨“ 𝑥 ”⟩ ) ) = ( 𝑖 + 𝑗 ) ) )
23	22	imbi2d	⊢ ( 𝑣 = ( 𝑤 ++ ⟨“ 𝑥 ”⟩ ) → ( ( 𝜑 → ∃ 𝑒 ∈ 𝐸 ∃ 𝑓 ∈ 𝐹 ( 𝑀 Σg 𝑣 ) = ( 𝑒 + 𝑓 ) ) ↔ ( 𝜑 → ∃ 𝑖 ∈ 𝐸 ∃ 𝑗 ∈ 𝐹 ( 𝑀 Σg ( 𝑤 ++ ⟨“ 𝑥 ”⟩ ) ) = ( 𝑖 + 𝑗 ) ) ) )
24		oveq2	⊢ ( 𝑣 = 𝑊 → ( 𝑀 Σg 𝑣 ) = ( 𝑀 Σg 𝑊 ) )
25	24	eqeq1d	⊢ ( 𝑣 = 𝑊 → ( ( 𝑀 Σg 𝑣 ) = ( 𝑒 + 𝑓 ) ↔ ( 𝑀 Σg 𝑊 ) = ( 𝑒 + 𝑓 ) ) )
26	25	2rexbidv	⊢ ( 𝑣 = 𝑊 → ( ∃ 𝑒 ∈ 𝐸 ∃ 𝑓 ∈ 𝐹 ( 𝑀 Σg 𝑣 ) = ( 𝑒 + 𝑓 ) ↔ ∃ 𝑒 ∈ 𝐸 ∃ 𝑓 ∈ 𝐹 ( 𝑀 Σg 𝑊 ) = ( 𝑒 + 𝑓 ) ) )
27	26	imbi2d	⊢ ( 𝑣 = 𝑊 → ( ( 𝜑 → ∃ 𝑒 ∈ 𝐸 ∃ 𝑓 ∈ 𝐹 ( 𝑀 Σg 𝑣 ) = ( 𝑒 + 𝑓 ) ) ↔ ( 𝜑 → ∃ 𝑒 ∈ 𝐸 ∃ 𝑓 ∈ 𝐹 ( 𝑀 Σg 𝑊 ) = ( 𝑒 + 𝑓 ) ) ) )
28		oveq1	⊢ ( 𝑒 = ( 0g ‘ 𝑀 ) → ( 𝑒 + 𝑓 ) = ( ( 0g ‘ 𝑀 ) + 𝑓 ) )
29	28	eqeq2d	⊢ ( 𝑒 = ( 0g ‘ 𝑀 ) → ( ( 𝑀 Σg ∅ ) = ( 𝑒 + 𝑓 ) ↔ ( 𝑀 Σg ∅ ) = ( ( 0g ‘ 𝑀 ) + 𝑓 ) ) )
30		oveq2	⊢ ( 𝑓 = ( 0g ‘ 𝑀 ) → ( ( 0g ‘ 𝑀 ) + 𝑓 ) = ( ( 0g ‘ 𝑀 ) + ( 0g ‘ 𝑀 ) ) )
31	30	eqeq2d	⊢ ( 𝑓 = ( 0g ‘ 𝑀 ) → ( ( 𝑀 Σg ∅ ) = ( ( 0g ‘ 𝑀 ) + 𝑓 ) ↔ ( 𝑀 Σg ∅ ) = ( ( 0g ‘ 𝑀 ) + ( 0g ‘ 𝑀 ) ) ) )
32		eqid	⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
33	32	subm0cl	⊢ ( 𝐸 ∈ ( SubMnd ‘ 𝑀 ) → ( 0g ‘ 𝑀 ) ∈ 𝐸 )
34	3 33	syl	⊢ ( 𝜑 → ( 0g ‘ 𝑀 ) ∈ 𝐸 )
35	32	subm0cl	⊢ ( 𝐹 ∈ ( SubMnd ‘ 𝑀 ) → ( 0g ‘ 𝑀 ) ∈ 𝐹 )
36	4 35	syl	⊢ ( 𝜑 → ( 0g ‘ 𝑀 ) ∈ 𝐹 )
37	32	gsum0	⊢ ( 𝑀 Σg ∅ ) = ( 0g ‘ 𝑀 )
38	2	cmnmndd	⊢ ( 𝜑 → 𝑀 ∈ Mnd )
39		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
40	39 32	mndidcl	⊢ ( 𝑀 ∈ Mnd → ( 0g ‘ 𝑀 ) ∈ ( Base ‘ 𝑀 ) )
41	39 1 32	mndlid	⊢ ( ( 𝑀 ∈ Mnd ∧ ( 0g ‘ 𝑀 ) ∈ ( Base ‘ 𝑀 ) ) → ( ( 0g ‘ 𝑀 ) + ( 0g ‘ 𝑀 ) ) = ( 0g ‘ 𝑀 ) )
42	38 40 41	syl2anc2	⊢ ( 𝜑 → ( ( 0g ‘ 𝑀 ) + ( 0g ‘ 𝑀 ) ) = ( 0g ‘ 𝑀 ) )
43	37 42	eqtr4id	⊢ ( 𝜑 → ( 𝑀 Σg ∅ ) = ( ( 0g ‘ 𝑀 ) + ( 0g ‘ 𝑀 ) ) )
44	29 31 34 36 43	2rspcedvdw	⊢ ( 𝜑 → ∃ 𝑒 ∈ 𝐸 ∃ 𝑓 ∈ 𝐹 ( 𝑀 Σg ∅ ) = ( 𝑒 + 𝑓 ) )
45		oveq1	⊢ ( 𝑖 = ( 𝑒 + 𝑥 ) → ( 𝑖 + 𝑗 ) = ( ( 𝑒 + 𝑥 ) + 𝑗 ) )
46	45	eqeq2d	⊢ ( 𝑖 = ( 𝑒 + 𝑥 ) → ( ( 𝑀 Σg ( 𝑤 ++ ⟨“ 𝑥 ”⟩ ) ) = ( 𝑖 + 𝑗 ) ↔ ( 𝑀 Σg ( 𝑤 ++ ⟨“ 𝑥 ”⟩ ) ) = ( ( 𝑒 + 𝑥 ) + 𝑗 ) ) )
47		oveq2	⊢ ( 𝑗 = 𝑓 → ( ( 𝑒 + 𝑥 ) + 𝑗 ) = ( ( 𝑒 + 𝑥 ) + 𝑓 ) )
48	47	eqeq2d	⊢ ( 𝑗 = 𝑓 → ( ( 𝑀 Σg ( 𝑤 ++ ⟨“ 𝑥 ”⟩ ) ) = ( ( 𝑒 + 𝑥 ) + 𝑗 ) ↔ ( 𝑀 Σg ( 𝑤 ++ ⟨“ 𝑥 ”⟩ ) ) = ( ( 𝑒 + 𝑥 ) + 𝑓 ) ) )
49	3	ad6antr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) ∧ 𝑥 ∈ 𝐸 ) → 𝐸 ∈ ( SubMnd ‘ 𝑀 ) )
50		simp-4r	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) ∧ 𝑥 ∈ 𝐸 ) → 𝑒 ∈ 𝐸 )
51		simpr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) ∧ 𝑥 ∈ 𝐸 ) → 𝑥 ∈ 𝐸 )
52	1 49 50 51	submcld	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) ∧ 𝑥 ∈ 𝐸 ) → ( 𝑒 + 𝑥 ) ∈ 𝐸 )
53		simpllr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) ∧ 𝑥 ∈ 𝐸 ) → 𝑓 ∈ 𝐹 )
54	38	ad5antr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) → 𝑀 ∈ Mnd )
55	39	submss	⊢ ( 𝐸 ∈ ( SubMnd ‘ 𝑀 ) → 𝐸 ⊆ ( Base ‘ 𝑀 ) )
56	3 55	syl	⊢ ( 𝜑 → 𝐸 ⊆ ( Base ‘ 𝑀 ) )
57	39	submss	⊢ ( 𝐹 ∈ ( SubMnd ‘ 𝑀 ) → 𝐹 ⊆ ( Base ‘ 𝑀 ) )
58	4 57	syl	⊢ ( 𝜑 → 𝐹 ⊆ ( Base ‘ 𝑀 ) )
59	56 58	unssd	⊢ ( 𝜑 → ( 𝐸 ∪ 𝐹 ) ⊆ ( Base ‘ 𝑀 ) )
60		sswrd	⊢ ( ( 𝐸 ∪ 𝐹 ) ⊆ ( Base ‘ 𝑀 ) → Word ( 𝐸 ∪ 𝐹 ) ⊆ Word ( Base ‘ 𝑀 ) )
61	59 60	syl	⊢ ( 𝜑 → Word ( 𝐸 ∪ 𝐹 ) ⊆ Word ( Base ‘ 𝑀 ) )
62	61	sselda	⊢ ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) → 𝑤 ∈ Word ( Base ‘ 𝑀 ) )
63	62	ad4antr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) → 𝑤 ∈ Word ( Base ‘ 𝑀 ) )
64	59	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) → ( 𝐸 ∪ 𝐹 ) ⊆ ( Base ‘ 𝑀 ) )
65	64	sselda	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) → 𝑥 ∈ ( Base ‘ 𝑀 ) )
66	65	ad3antrrr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) → 𝑥 ∈ ( Base ‘ 𝑀 ) )
67	39 1	gsumccatsn	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑤 ∈ Word ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑀 Σg ( 𝑤 ++ ⟨“ 𝑥 ”⟩ ) ) = ( ( 𝑀 Σg 𝑤 ) + 𝑥 ) )
68	54 63 66 67	syl3anc	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) → ( 𝑀 Σg ( 𝑤 ++ ⟨“ 𝑥 ”⟩ ) ) = ( ( 𝑀 Σg 𝑤 ) + 𝑥 ) )
69		simpr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) → ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) )
70	69	oveq1d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) → ( ( 𝑀 Σg 𝑤 ) + 𝑥 ) = ( ( 𝑒 + 𝑓 ) + 𝑥 ) )
71	56	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) → 𝐸 ⊆ ( Base ‘ 𝑀 ) )
72	71	sselda	⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) → 𝑒 ∈ ( Base ‘ 𝑀 ) )
73	72	ad2antrr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) → 𝑒 ∈ ( Base ‘ 𝑀 ) )
74	58	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) → 𝐹 ⊆ ( Base ‘ 𝑀 ) )
75	74	sselda	⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) → 𝑓 ∈ ( Base ‘ 𝑀 ) )
76	75	adantr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) → 𝑓 ∈ ( Base ‘ 𝑀 ) )
77	2	ad5antr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) → 𝑀 ∈ CMnd )
78	39 1	cmncom	⊢ ( ( 𝑀 ∈ CMnd ∧ 𝑓 ∈ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑓 + 𝑥 ) = ( 𝑥 + 𝑓 ) )
79	77 76 66 78	syl3anc	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) → ( 𝑓 + 𝑥 ) = ( 𝑥 + 𝑓 ) )
80	39 1 54 73 76 66 79	mnd32g	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) → ( ( 𝑒 + 𝑓 ) + 𝑥 ) = ( ( 𝑒 + 𝑥 ) + 𝑓 ) )
81	68 70 80	3eqtrd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) → ( 𝑀 Σg ( 𝑤 ++ ⟨“ 𝑥 ”⟩ ) ) = ( ( 𝑒 + 𝑥 ) + 𝑓 ) )
82	81	adantr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) ∧ 𝑥 ∈ 𝐸 ) → ( 𝑀 Σg ( 𝑤 ++ ⟨“ 𝑥 ”⟩ ) ) = ( ( 𝑒 + 𝑥 ) + 𝑓 ) )
83	46 48 52 53 82	2rspcedvdw	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) ∧ 𝑥 ∈ 𝐸 ) → ∃ 𝑖 ∈ 𝐸 ∃ 𝑗 ∈ 𝐹 ( 𝑀 Σg ( 𝑤 ++ ⟨“ 𝑥 ”⟩ ) ) = ( 𝑖 + 𝑗 ) )
84		oveq1	⊢ ( 𝑖 = 𝑒 → ( 𝑖 + 𝑗 ) = ( 𝑒 + 𝑗 ) )
85	84	eqeq2d	⊢ ( 𝑖 = 𝑒 → ( ( 𝑀 Σg ( 𝑤 ++ ⟨“ 𝑥 ”⟩ ) ) = ( 𝑖 + 𝑗 ) ↔ ( 𝑀 Σg ( 𝑤 ++ ⟨“ 𝑥 ”⟩ ) ) = ( 𝑒 + 𝑗 ) ) )
86		oveq2	⊢ ( 𝑗 = ( 𝑓 + 𝑥 ) → ( 𝑒 + 𝑗 ) = ( 𝑒 + ( 𝑓 + 𝑥 ) ) )
87	86	eqeq2d	⊢ ( 𝑗 = ( 𝑓 + 𝑥 ) → ( ( 𝑀 Σg ( 𝑤 ++ ⟨“ 𝑥 ”⟩ ) ) = ( 𝑒 + 𝑗 ) ↔ ( 𝑀 Σg ( 𝑤 ++ ⟨“ 𝑥 ”⟩ ) ) = ( 𝑒 + ( 𝑓 + 𝑥 ) ) ) )
88		simp-4r	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) ∧ 𝑥 ∈ 𝐹 ) → 𝑒 ∈ 𝐸 )
89	4	ad6antr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) ∧ 𝑥 ∈ 𝐹 ) → 𝐹 ∈ ( SubMnd ‘ 𝑀 ) )
90		simpllr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) ∧ 𝑥 ∈ 𝐹 ) → 𝑓 ∈ 𝐹 )
91		simpr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) ∧ 𝑥 ∈ 𝐹 ) → 𝑥 ∈ 𝐹 )
92	1 89 90 91	submcld	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) ∧ 𝑥 ∈ 𝐹 ) → ( 𝑓 + 𝑥 ) ∈ 𝐹 )
93	39 1 54 73 76 66	mndassd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) → ( ( 𝑒 + 𝑓 ) + 𝑥 ) = ( 𝑒 + ( 𝑓 + 𝑥 ) ) )
94	68 70 93	3eqtrd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) → ( 𝑀 Σg ( 𝑤 ++ ⟨“ 𝑥 ”⟩ ) ) = ( 𝑒 + ( 𝑓 + 𝑥 ) ) )
95	94	adantr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) ∧ 𝑥 ∈ 𝐹 ) → ( 𝑀 Σg ( 𝑤 ++ ⟨“ 𝑥 ”⟩ ) ) = ( 𝑒 + ( 𝑓 + 𝑥 ) ) )
96	85 87 88 92 95	2rspcedvdw	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) ∧ 𝑥 ∈ 𝐹 ) → ∃ 𝑖 ∈ 𝐸 ∃ 𝑗 ∈ 𝐹 ( 𝑀 Σg ( 𝑤 ++ ⟨“ 𝑥 ”⟩ ) ) = ( 𝑖 + 𝑗 ) )
97		elun	⊢ ( 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ↔ ( 𝑥 ∈ 𝐸 ∨ 𝑥 ∈ 𝐹 ) )
98	97	biimpi	⊢ ( 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) → ( 𝑥 ∈ 𝐸 ∨ 𝑥 ∈ 𝐹 ) )
99	98	ad4antlr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) → ( 𝑥 ∈ 𝐸 ∨ 𝑥 ∈ 𝐹 ) )
100	83 96 99	mpjaodan	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) → ∃ 𝑖 ∈ 𝐸 ∃ 𝑗 ∈ 𝐹 ( 𝑀 Σg ( 𝑤 ++ ⟨“ 𝑥 ”⟩ ) ) = ( 𝑖 + 𝑗 ) )
101	100	r19.29ffa	⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) ∧ ∃ 𝑒 ∈ 𝐸 ∃ 𝑓 ∈ 𝐹 ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) → ∃ 𝑖 ∈ 𝐸 ∃ 𝑗 ∈ 𝐹 ( 𝑀 Σg ( 𝑤 ++ ⟨“ 𝑥 ”⟩ ) ) = ( 𝑖 + 𝑗 ) )
102	101	ex	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) → ( ∃ 𝑒 ∈ 𝐸 ∃ 𝑓 ∈ 𝐹 ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) → ∃ 𝑖 ∈ 𝐸 ∃ 𝑗 ∈ 𝐹 ( 𝑀 Σg ( 𝑤 ++ ⟨“ 𝑥 ”⟩ ) ) = ( 𝑖 + 𝑗 ) ) )
103	102	expl	⊢ ( 𝜑 → ( ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) → ( ∃ 𝑒 ∈ 𝐸 ∃ 𝑓 ∈ 𝐹 ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) → ∃ 𝑖 ∈ 𝐸 ∃ 𝑗 ∈ 𝐹 ( 𝑀 Σg ( 𝑤 ++ ⟨“ 𝑥 ”⟩ ) ) = ( 𝑖 + 𝑗 ) ) ) )
104	103	com12	⊢ ( ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) → ( 𝜑 → ( ∃ 𝑒 ∈ 𝐸 ∃ 𝑓 ∈ 𝐹 ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) → ∃ 𝑖 ∈ 𝐸 ∃ 𝑗 ∈ 𝐹 ( 𝑀 Σg ( 𝑤 ++ ⟨“ 𝑥 ”⟩ ) ) = ( 𝑖 + 𝑗 ) ) ) )
105	104	a2d	⊢ ( ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ∧ 𝑥 ∈ ( 𝐸 ∪ 𝐹 ) ) → ( ( 𝜑 → ∃ 𝑒 ∈ 𝐸 ∃ 𝑓 ∈ 𝐹 ( 𝑀 Σg 𝑤 ) = ( 𝑒 + 𝑓 ) ) → ( 𝜑 → ∃ 𝑖 ∈ 𝐸 ∃ 𝑗 ∈ 𝐹 ( 𝑀 Σg ( 𝑤 ++ ⟨“ 𝑥 ”⟩ ) ) = ( 𝑖 + 𝑗 ) ) ) )
106	9 13 23 27 44 105	wrdind	⊢ ( 𝑊 ∈ Word ( 𝐸 ∪ 𝐹 ) → ( 𝜑 → ∃ 𝑒 ∈ 𝐸 ∃ 𝑓 ∈ 𝐹 ( 𝑀 Σg 𝑊 ) = ( 𝑒 + 𝑓 ) ) )
107	5 106	mpcom	⊢ ( 𝜑 → ∃ 𝑒 ∈ 𝐸 ∃ 𝑓 ∈ 𝐹 ( 𝑀 Σg 𝑊 ) = ( 𝑒 + 𝑓 ) )