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 M = freeMnd I
frmdgsum.u U = var FMnd I
Assertion frmdgsum I V W Word I M U W = W

Proof

Step Hyp Ref Expression
1 frmdmnd.m M = freeMnd I
2 frmdgsum.u U = var FMnd I
3 coeq2 x = U x = U
4 co02 U =
5 3 4 eqtrdi x = U x =
6 5 oveq2d x = M U x = M
7 id x = x =
8 6 7 eqeq12d x = M U x = x M =
9 8 imbi2d x = I V M U x = x I V M =
10 coeq2 x = y U x = U y
11 10 oveq2d x = y M U x = M U y
12 id x = y x = y
13 11 12 eqeq12d x = y M U x = x M U y = y
14 13 imbi2d x = y I V M U x = x I V M U y = y
15 coeq2 x = y ++ ⟨“ z ”⟩ U x = U y ++ ⟨“ z ”⟩
16 15 oveq2d x = y ++ ⟨“ z ”⟩ M U x = M U y ++ ⟨“ z ”⟩
17 id x = y ++ ⟨“ z ”⟩ x = y ++ ⟨“ z ”⟩
18 16 17 eqeq12d x = y ++ ⟨“ z ”⟩ M U x = x M U y ++ ⟨“ z ”⟩ = y ++ ⟨“ z ”⟩
19 18 imbi2d x = y ++ ⟨“ z ”⟩ I V M U x = x I V M U y ++ ⟨“ z ”⟩ = y ++ ⟨“ z ”⟩
20 coeq2 x = W U x = U W
21 20 oveq2d x = W M U x = M U W
22 id x = W x = W
23 21 22 eqeq12d x = W M U x = x M U W = W
24 23 imbi2d x = W I V M U x = x I V M U W = W
25 1 frmd0 = 0 M
26 25 gsum0 M =
27 26 a1i I V M =
28 oveq1 M U y = y M U y ++ ⟨“ z ”⟩ = y ++ ⟨“ z ”⟩
29 simprl I V y Word I z I y Word I
30 simprr I V y Word I z I z I
31 30 s1cld I V y Word I z I ⟨“ z ”⟩ Word I
32 2 vrmdf I V U : I Word I
33 32 adantr I V y Word I z I U : I Word I
34 ccatco y Word I ⟨“ z ”⟩ Word I U : I Word I U y ++ ⟨“ z ”⟩ = U y ++ U ⟨“ z ”⟩
35 29 31 33 34 syl3anc I V y Word I z I U y ++ ⟨“ z ”⟩ = U y ++ U ⟨“ z ”⟩
36 s1co z I U : I Word I U ⟨“ z ”⟩ = ⟨“ U z ”⟩
37 30 33 36 syl2anc I V y Word I z I U ⟨“ z ”⟩ = ⟨“ U z ”⟩
38 2 vrmdval I V z I U z = ⟨“ z ”⟩
39 38 adantrl I V y Word I z I U z = ⟨“ z ”⟩
40 39 s1eqd I V y Word I z I ⟨“ U z ”⟩ = ⟨“ ⟨“ z ”⟩ ”⟩
41 37 40 eqtrd I V y Word I z I U ⟨“ z ”⟩ = ⟨“ ⟨“ z ”⟩ ”⟩
42 41 oveq2d I V y Word I z I U y ++ U ⟨“ z ”⟩ = U y ++ ⟨“ ⟨“ z ”⟩ ”⟩
43 35 42 eqtrd I V y Word I z I U y ++ ⟨“ z ”⟩ = U y ++ ⟨“ ⟨“ z ”⟩ ”⟩
44 43 oveq2d I V y Word I z I M U y ++ ⟨“ z ”⟩ = M U y ++ ⟨“ ⟨“ z ”⟩ ”⟩
45 1 frmdmnd I V M Mnd
46 45 adantr I V y Word I z I M Mnd
47 wrdco y Word I U : I Word I U y Word Word I
48 29 33 47 syl2anc I V y Word I z I U y Word Word I
49 eqid Base M = Base M
50 1 49 frmdbas I V Base M = Word I
51 50 adantr I V y Word I z I Base M = Word I
52 wrdeq Base M = Word I Word Base M = Word Word I
53 51 52 syl I V y Word I z I Word Base M = Word Word I
54 48 53 eleqtrrd I V y Word I z I U y Word Base M
55 31 51 eleqtrrd I V y Word I z I ⟨“ z ”⟩ Base M
56 55 s1cld I V y Word I z I ⟨“ ⟨“ z ”⟩ ”⟩ Word Base M
57 eqid + M = + M
58 49 57 gsumccat M Mnd U y Word Base M ⟨“ ⟨“ z ”⟩ ”⟩ Word Base M M U y ++ ⟨“ ⟨“ z ”⟩ ”⟩ = M U y + M M ⟨“ ⟨“ z ”⟩ ”⟩
59 46 54 56 58 syl3anc I V y Word I z I M U y ++ ⟨“ ⟨“ z ”⟩ ”⟩ = M U y + M M ⟨“ ⟨“ z ”⟩ ”⟩
60 49 gsumws1 ⟨“ z ”⟩ Base M M ⟨“ ⟨“ z ”⟩ ”⟩ = ⟨“ z ”⟩
61 55 60 syl I V y Word I z I M ⟨“ ⟨“ z ”⟩ ”⟩ = ⟨“ z ”⟩
62 61 oveq2d I V y Word I z I M U y + M M ⟨“ ⟨“ z ”⟩ ”⟩ = M U y + M ⟨“ z ”⟩
63 49 gsumwcl M Mnd U y Word Base M M U y Base M
64 46 54 63 syl2anc I V y Word I z I M U y Base M
65 1 49 57 frmdadd M U y Base M ⟨“ z ”⟩ Base M M U y + M ⟨“ z ”⟩ = M U y ++ ⟨“ z ”⟩
66 64 55 65 syl2anc I V y Word I z I M U y + M ⟨“ z ”⟩ = M U y ++ ⟨“ z ”⟩
67 62 66 eqtrd I V y Word I z I M U y + M M ⟨“ ⟨“ z ”⟩ ”⟩ = M U y ++ ⟨“ z ”⟩
68 59 67 eqtrd I V y Word I z I M U y ++ ⟨“ ⟨“ z ”⟩ ”⟩ = M U y ++ ⟨“ z ”⟩
69 44 68 eqtrd I V y Word I z I M U y ++ ⟨“ z ”⟩ = M U y ++ ⟨“ z ”⟩
70 69 eqeq1d I V y Word I z I M U y ++ ⟨“ z ”⟩ = y ++ ⟨“ z ”⟩ M U y ++ ⟨“ z ”⟩ = y ++ ⟨“ z ”⟩
71 28 70 syl5ibr I V y Word I z I M U y = y M U y ++ ⟨“ z ”⟩ = y ++ ⟨“ z ”⟩
72 71 expcom y Word I z I I V M U y = y M U y ++ ⟨“ z ”⟩ = y ++ ⟨“ z ”⟩
73 72 a2d y Word I z I I V M U y = y I V M U y ++ ⟨“ z ”⟩ = y ++ ⟨“ z ”⟩
74 9 14 19 24 27 73 wrdind W Word I I V M U W = W
75 74 impcom I V W Word I M U W = W