Metamath Proof Explorer

Theorem frmdgsum

Description: Any word in a free monoid can be expressed as the sum of the singletons composing it. (Contributed by Mario Carneiro, 27-Sep-2015)

Ref Expression
Hypotheses frmdmnd.m ⊢ 𝑀 = ( freeMnd ‘ 𝐼 )
frmdgsum.u ⊢ 𝑈 = ( varFMnd ‘ 𝐼 )
Assertion frmdgsum ( ( 𝐼 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝐼 ) → ( 𝑀 Σg ( 𝑈 ∘ 𝑊 ) ) = 𝑊 )

Proof

Step Hyp Ref Expression
1 frmdmnd.m ⊢ 𝑀 = ( freeMnd ‘ 𝐼 )
2 frmdgsum.u ⊢ 𝑈 = ( varFMnd ‘ 𝐼 )
3 coeq2 ⊢ ( 𝑥 = ∅ → ( 𝑈 ∘ 𝑥 ) = ( 𝑈 ∘ ∅ ) )
4 co02 ⊢ ( 𝑈 ∘ ∅ ) = ∅
5 3 4 eqtrdi ⊢ ( 𝑥 = ∅ → ( 𝑈 ∘ 𝑥 ) = ∅ )
6 5 oveq2d ⊢ ( 𝑥 = ∅ → ( 𝑀 Σg ( 𝑈 ∘ 𝑥 ) ) = ( 𝑀 Σg ∅ ) )
7 id ⊢ ( 𝑥 = ∅ → 𝑥 = ∅ )
8 6 7 eqeq12d ⊢ ( 𝑥 = ∅ → ( ( 𝑀 Σg ( 𝑈 ∘ 𝑥 ) ) = 𝑥 ↔ ( 𝑀 Σg ∅ ) = ∅ ) )
9 8 imbi2d ⊢ ( 𝑥 = ∅ → ( ( 𝐼 ∈ 𝑉 → ( 𝑀 Σg ( 𝑈 ∘ 𝑥 ) ) = 𝑥 ) ↔ ( 𝐼 ∈ 𝑉 → ( 𝑀 Σg ∅ ) = ∅ ) ) )
10 coeq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑈 ∘ 𝑥 ) = ( 𝑈 ∘ 𝑦 ) )
11 10 oveq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑀 Σg ( 𝑈 ∘ 𝑥 ) ) = ( 𝑀 Σg ( 𝑈 ∘ 𝑦 ) ) )
12 id ⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
13 11 12 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑀 Σg ( 𝑈 ∘ 𝑥 ) ) = 𝑥 ↔ ( 𝑀 Σg ( 𝑈 ∘ 𝑦 ) ) = 𝑦 ) )
14 13 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐼 ∈ 𝑉 → ( 𝑀 Σg ( 𝑈 ∘ 𝑥 ) ) = 𝑥 ) ↔ ( 𝐼 ∈ 𝑉 → ( 𝑀 Σg ( 𝑈 ∘ 𝑦 ) ) = 𝑦 ) ) )
15 coeq2 ⊢ ( 𝑥 = ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) → ( 𝑈 ∘ 𝑥 ) = ( 𝑈 ∘ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) )
16 15 oveq2d ⊢ ( 𝑥 = ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) → ( 𝑀 Σg ( 𝑈 ∘ 𝑥 ) ) = ( 𝑀 Σg ( 𝑈 ∘ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) ) )
17 id ⊢ ( 𝑥 = ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) → 𝑥 = ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) )
18 16 17 eqeq12d ⊢ ( 𝑥 = ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) → ( ( 𝑀 Σg ( 𝑈 ∘ 𝑥 ) ) = 𝑥 ↔ ( 𝑀 Σg ( 𝑈 ∘ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) ) = ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) )
19 18 imbi2d ⊢ ( 𝑥 = ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) → ( ( 𝐼 ∈ 𝑉 → ( 𝑀 Σg ( 𝑈 ∘ 𝑥 ) ) = 𝑥 ) ↔ ( 𝐼 ∈ 𝑉 → ( 𝑀 Σg ( 𝑈 ∘ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) ) = ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) ) )
20 coeq2 ⊢ ( 𝑥 = 𝑊 → ( 𝑈 ∘ 𝑥 ) = ( 𝑈 ∘ 𝑊 ) )
21 20 oveq2d ⊢ ( 𝑥 = 𝑊 → ( 𝑀 Σg ( 𝑈 ∘ 𝑥 ) ) = ( 𝑀 Σg ( 𝑈 ∘ 𝑊 ) ) )
22 id ⊢ ( 𝑥 = 𝑊 → 𝑥 = 𝑊 )
23 21 22 eqeq12d ⊢ ( 𝑥 = 𝑊 → ( ( 𝑀 Σg ( 𝑈 ∘ 𝑥 ) ) = 𝑥 ↔ ( 𝑀 Σg ( 𝑈 ∘ 𝑊 ) ) = 𝑊 ) )
24 23 imbi2d ⊢ ( 𝑥 = 𝑊 → ( ( 𝐼 ∈ 𝑉 → ( 𝑀 Σg ( 𝑈 ∘ 𝑥 ) ) = 𝑥 ) ↔ ( 𝐼 ∈ 𝑉 → ( 𝑀 Σg ( 𝑈 ∘ 𝑊 ) ) = 𝑊 ) ) )
25 1 frmd0 ⊢ ∅ = ( 0g ‘ 𝑀 )
26 25 gsum0 ⊢ ( 𝑀 Σg ∅ ) = ∅
27 26 a1i ⊢ ( 𝐼 ∈ 𝑉 → ( 𝑀 Σg ∅ ) = ∅ )
28 oveq1 ⊢ ( ( 𝑀 Σg ( 𝑈 ∘ 𝑦 ) ) = 𝑦 → ( ( 𝑀 Σg ( 𝑈 ∘ 𝑦 ) ) ++ ⟨“ 𝑧 ”⟩ ) = ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) )
29 simprl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼 ) ) → 𝑦 ∈ Word 𝐼 )
30 simprr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼 ) ) → 𝑧 ∈ 𝐼 )
31 30 s1cld ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼 ) ) → ⟨“ 𝑧 ”⟩ ∈ Word 𝐼 )
32 2 vrmdf ⊢ ( 𝐼 ∈ 𝑉 → 𝑈 : 𝐼 ⟶ Word 𝐼 )
33 32 adantr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼 ) ) → 𝑈 : 𝐼 ⟶ Word 𝐼 )
34 ccatco ⊢ ( ( 𝑦 ∈ Word 𝐼 ∧ ⟨“ 𝑧 ”⟩ ∈ Word 𝐼 ∧ 𝑈 : 𝐼 ⟶ Word 𝐼 ) → ( 𝑈 ∘ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) = ( ( 𝑈 ∘ 𝑦 ) ++ ( 𝑈 ∘ ⟨“ 𝑧 ”⟩ ) ) )
35 29 31 33 34 syl3anc ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼 ) ) → ( 𝑈 ∘ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) = ( ( 𝑈 ∘ 𝑦 ) ++ ( 𝑈 ∘ ⟨“ 𝑧 ”⟩ ) ) )
36 s1co ⊢ ( ( 𝑧 ∈ 𝐼 ∧ 𝑈 : 𝐼 ⟶ Word 𝐼 ) → ( 𝑈 ∘ ⟨“ 𝑧 ”⟩ ) = ⟨“ ( 𝑈 ‘ 𝑧 ) ”⟩ )
37 30 33 36 syl2anc ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼 ) ) → ( 𝑈 ∘ ⟨“ 𝑧 ”⟩ ) = ⟨“ ( 𝑈 ‘ 𝑧 ) ”⟩ )
38 2 vrmdval ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝐼 ) → ( 𝑈 ‘ 𝑧 ) = ⟨“ 𝑧 ”⟩ )
39 38 adantrl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼 ) ) → ( 𝑈 ‘ 𝑧 ) = ⟨“ 𝑧 ”⟩ )
40 39 s1eqd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼 ) ) → ⟨“ ( 𝑈 ‘ 𝑧 ) ”⟩ = ⟨“ ⟨“ 𝑧 ”⟩ ”⟩ )
41 37 40 eqtrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼 ) ) → ( 𝑈 ∘ ⟨“ 𝑧 ”⟩ ) = ⟨“ ⟨“ 𝑧 ”⟩ ”⟩ )
42 41 oveq2d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼 ) ) → ( ( 𝑈 ∘ 𝑦 ) ++ ( 𝑈 ∘ ⟨“ 𝑧 ”⟩ ) ) = ( ( 𝑈 ∘ 𝑦 ) ++ ⟨“ ⟨“ 𝑧 ”⟩ ”⟩ ) )
43 35 42 eqtrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼 ) ) → ( 𝑈 ∘ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) = ( ( 𝑈 ∘ 𝑦 ) ++ ⟨“ ⟨“ 𝑧 ”⟩ ”⟩ ) )
44 43 oveq2d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼 ) ) → ( 𝑀 Σg ( 𝑈 ∘ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) ) = ( 𝑀 Σg ( ( 𝑈 ∘ 𝑦 ) ++ ⟨“ ⟨“ 𝑧 ”⟩ ”⟩ ) ) )
45 1 frmdmnd ⊢ ( 𝐼 ∈ 𝑉 → 𝑀 ∈ Mnd )
46 45 adantr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼 ) ) → 𝑀 ∈ Mnd )
47 wrdco ⊢ ( ( 𝑦 ∈ Word 𝐼 ∧ 𝑈 : 𝐼 ⟶ Word 𝐼 ) → ( 𝑈 ∘ 𝑦 ) ∈ Word Word 𝐼 )
48 29 33 47 syl2anc ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼 ) ) → ( 𝑈 ∘ 𝑦 ) ∈ Word Word 𝐼 )
49 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
50 1 49 frmdbas ⊢ ( 𝐼 ∈ 𝑉 → ( Base ‘ 𝑀 ) = Word 𝐼 )
51 50 adantr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼 ) ) → ( Base ‘ 𝑀 ) = Word 𝐼 )
52 wrdeq ⊢ ( ( Base ‘ 𝑀 ) = Word 𝐼 → Word ( Base ‘ 𝑀 ) = Word Word 𝐼 )
53 51 52 syl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼 ) ) → Word ( Base ‘ 𝑀 ) = Word Word 𝐼 )
54 48 53 eleqtrrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼 ) ) → ( 𝑈 ∘ 𝑦 ) ∈ Word ( Base ‘ 𝑀 ) )
55 31 51 eleqtrrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼 ) ) → ⟨“ 𝑧 ”⟩ ∈ ( Base ‘ 𝑀 ) )
56 55 s1cld ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼 ) ) → ⟨“ ⟨“ 𝑧 ”⟩ ”⟩ ∈ Word ( Base ‘ 𝑀 ) )
57 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
58 49 57 gsumccat ⊢ ( ( 𝑀 ∈ Mnd ∧ ( 𝑈 ∘ 𝑦 ) ∈ Word ( Base ‘ 𝑀 ) ∧ ⟨“ ⟨“ 𝑧 ”⟩ ”⟩ ∈ Word ( Base ‘ 𝑀 ) ) → ( 𝑀 Σg ( ( 𝑈 ∘ 𝑦 ) ++ ⟨“ ⟨“ 𝑧 ”⟩ ”⟩ ) ) = ( ( 𝑀 Σg ( 𝑈 ∘ 𝑦 ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ⟨“ ⟨“ 𝑧 ”⟩ ”⟩ ) ) )
59 46 54 56 58 syl3anc ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼 ) ) → ( 𝑀 Σg ( ( 𝑈 ∘ 𝑦 ) ++ ⟨“ ⟨“ 𝑧 ”⟩ ”⟩ ) ) = ( ( 𝑀 Σg ( 𝑈 ∘ 𝑦 ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ⟨“ ⟨“ 𝑧 ”⟩ ”⟩ ) ) )
60 49 gsumws1 ⊢ ( ⟨“ 𝑧 ”⟩ ∈ ( Base ‘ 𝑀 ) → ( 𝑀 Σg ⟨“ ⟨“ 𝑧 ”⟩ ”⟩ ) = ⟨“ 𝑧 ”⟩ )
61 55 60 syl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼 ) ) → ( 𝑀 Σg ⟨“ ⟨“ 𝑧 ”⟩ ”⟩ ) = ⟨“ 𝑧 ”⟩ )
62 61 oveq2d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼 ) ) → ( ( 𝑀 Σg ( 𝑈 ∘ 𝑦 ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ⟨“ ⟨“ 𝑧 ”⟩ ”⟩ ) ) = ( ( 𝑀 Σg ( 𝑈 ∘ 𝑦 ) ) ( +g ‘ 𝑀 ) ⟨“ 𝑧 ”⟩ ) )
63 49 gsumwcl ⊢ ( ( 𝑀 ∈ Mnd ∧ ( 𝑈 ∘ 𝑦 ) ∈ Word ( Base ‘ 𝑀 ) ) → ( 𝑀 Σg ( 𝑈 ∘ 𝑦 ) ) ∈ ( Base ‘ 𝑀 ) )
64 46 54 63 syl2anc ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼 ) ) → ( 𝑀 Σg ( 𝑈 ∘ 𝑦 ) ) ∈ ( Base ‘ 𝑀 ) )
65 1 49 57 frmdadd ⊢ ( ( ( 𝑀 Σg ( 𝑈 ∘ 𝑦 ) ) ∈ ( Base ‘ 𝑀 ) ∧ ⟨“ 𝑧 ”⟩ ∈ ( Base ‘ 𝑀 ) ) → ( ( 𝑀 Σg ( 𝑈 ∘ 𝑦 ) ) ( +g ‘ 𝑀 ) ⟨“ 𝑧 ”⟩ ) = ( ( 𝑀 Σg ( 𝑈 ∘ 𝑦 ) ) ++ ⟨“ 𝑧 ”⟩ ) )
66 64 55 65 syl2anc ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼 ) ) → ( ( 𝑀 Σg ( 𝑈 ∘ 𝑦 ) ) ( +g ‘ 𝑀 ) ⟨“ 𝑧 ”⟩ ) = ( ( 𝑀 Σg ( 𝑈 ∘ 𝑦 ) ) ++ ⟨“ 𝑧 ”⟩ ) )
67 62 66 eqtrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼 ) ) → ( ( 𝑀 Σg ( 𝑈 ∘ 𝑦 ) ) ( +g ‘ 𝑀 ) ( 𝑀 Σg ⟨“ ⟨“ 𝑧 ”⟩ ”⟩ ) ) = ( ( 𝑀 Σg ( 𝑈 ∘ 𝑦 ) ) ++ ⟨“ 𝑧 ”⟩ ) )
68 59 67 eqtrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼 ) ) → ( 𝑀 Σg ( ( 𝑈 ∘ 𝑦 ) ++ ⟨“ ⟨“ 𝑧 ”⟩ ”⟩ ) ) = ( ( 𝑀 Σg ( 𝑈 ∘ 𝑦 ) ) ++ ⟨“ 𝑧 ”⟩ ) )
69 44 68 eqtrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼 ) ) → ( 𝑀 Σg ( 𝑈 ∘ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) ) = ( ( 𝑀 Σg ( 𝑈 ∘ 𝑦 ) ) ++ ⟨“ 𝑧 ”⟩ ) )
70 69 eqeq1d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼 ) ) → ( ( 𝑀 Σg ( 𝑈 ∘ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) ) = ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ↔ ( ( 𝑀 Σg ( 𝑈 ∘ 𝑦 ) ) ++ ⟨“ 𝑧 ”⟩ ) = ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) )
71 28 70 imbitrrid ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼 ) ) → ( ( 𝑀 Σg ( 𝑈 ∘ 𝑦 ) ) = 𝑦 → ( 𝑀 Σg ( 𝑈 ∘ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) ) = ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) )
72 71 expcom ⊢ ( ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼 ) → ( 𝐼 ∈ 𝑉 → ( ( 𝑀 Σg ( 𝑈 ∘ 𝑦 ) ) = 𝑦 → ( 𝑀 Σg ( 𝑈 ∘ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) ) = ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) ) )
73 72 a2d ⊢ ( ( 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ 𝐼 ) → ( ( 𝐼 ∈ 𝑉 → ( 𝑀 Σg ( 𝑈 ∘ 𝑦 ) ) = 𝑦 ) → ( 𝐼 ∈ 𝑉 → ( 𝑀 Σg ( 𝑈 ∘ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) ) = ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) ) )
74 9 14 19 24 27 73 wrdind ⊢ ( 𝑊 ∈ Word 𝐼 → ( 𝐼 ∈ 𝑉 → ( 𝑀 Σg ( 𝑈 ∘ 𝑊 ) ) = 𝑊 ) )
75 74 impcom ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝐼 ) → ( 𝑀 Σg ( 𝑈 ∘ 𝑊 ) ) = 𝑊 )