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 = ( varFMnd ` I )
Assertion frmdgsum 
|- ( ( I e. V /\ W e. Word I ) -> ( M gsum ( U o. W ) ) = W )

Proof

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