This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑊 ) = ( 𝑒 + 𝑓 ) )