Metamath Proof Explorer

Theorem frmdup1

Description: Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 27-Sep-2015)

Ref Expression
Hypotheses frmdup.m 
|- M = ( freeMnd ` I )
frmdup.b 
|- B = ( Base ` G )
frmdup.e 
|- E = ( x e. Word I |-> ( G gsum ( A o. x ) ) )
frmdup.g 
|- ( ph -> G e. Mnd )
frmdup.i 
|- ( ph -> I e. X )
frmdup.a 
|- ( ph -> A : I --> B )
Assertion frmdup1 
|- ( ph -> E e. ( M MndHom G ) )

Proof

Step Hyp Ref Expression
1 frmdup.m 
 |-  M = ( freeMnd ` I )
2 frmdup.b 
 |-  B = ( Base ` G )
3 frmdup.e 
 |-  E = ( x e. Word I |-> ( G gsum ( A o. x ) ) )
4 frmdup.g 
 |-  ( ph -> G e. Mnd )
5 frmdup.i 
 |-  ( ph -> I e. X )
6 frmdup.a 
 |-  ( ph -> A : I --> B )
7 1 frmdmnd 
 |-  ( I e. X -> M e. Mnd )
8 5 7 syl 
 |-  ( ph -> M e. Mnd )
9 4 adantr 
 |-  ( ( ph /\ x e. Word I ) -> G e. Mnd )
10 simpr 
 |-  ( ( ph /\ x e. Word I ) -> x e. Word I )
11 6 adantr 
 |-  ( ( ph /\ x e. Word I ) -> A : I --> B )
12 wrdco 
 |-  ( ( x e. Word I /\ A : I --> B ) -> ( A o. x ) e. Word B )
13 10 11 12 syl2anc 
 |-  ( ( ph /\ x e. Word I ) -> ( A o. x ) e. Word B )
14 2 gsumwcl 
 |-  ( ( G e. Mnd /\ ( A o. x ) e. Word B ) -> ( G gsum ( A o. x ) ) e. B )
15 9 13 14 syl2anc 
 |-  ( ( ph /\ x e. Word I ) -> ( G gsum ( A o. x ) ) e. B )
16 15 3 fmptd 
 |-  ( ph -> E : Word I --> B )
17 eqid 
 |-  ( Base ` M ) = ( Base ` M )
18 1 17 frmdbas 
 |-  ( I e. X -> ( Base ` M ) = Word I )
19 5 18 syl 
 |-  ( ph -> ( Base ` M ) = Word I )
20 19 feq2d 
 |-  ( ph -> ( E : ( Base ` M ) --> B <-> E : Word I --> B ) )
21 16 20 mpbird 
 |-  ( ph -> E : ( Base ` M ) --> B )
22 1 17 frmdelbas 
 |-  ( y e. ( Base ` M ) -> y e. Word I )
23 22 ad2antrl 
 |-  ( ( ph /\ ( y e. ( Base ` M ) /\ z e. ( Base ` M ) ) ) -> y e. Word I )
24 1 17 frmdelbas 
 |-  ( z e. ( Base ` M ) -> z e. Word I )
25 24 ad2antll 
 |-  ( ( ph /\ ( y e. ( Base ` M ) /\ z e. ( Base ` M ) ) ) -> z e. Word I )
26 6 adantr 
 |-  ( ( ph /\ ( y e. ( Base ` M ) /\ z e. ( Base ` M ) ) ) -> A : I --> B )
27 ccatco 
 |-  ( ( y e. Word I /\ z e. Word I /\ A : I --> B ) -> ( A o. ( y ++ z ) ) = ( ( A o. y ) ++ ( A o. z ) ) )
28 23 25 26 27 syl3anc 
 |-  ( ( ph /\ ( y e. ( Base ` M ) /\ z e. ( Base ` M ) ) ) -> ( A o. ( y ++ z ) ) = ( ( A o. y ) ++ ( A o. z ) ) )
29 28 oveq2d 
 |-  ( ( ph /\ ( y e. ( Base ` M ) /\ z e. ( Base ` M ) ) ) -> ( G gsum ( A o. ( y ++ z ) ) ) = ( G gsum ( ( A o. y ) ++ ( A o. z ) ) ) )
30 4 adantr 
 |-  ( ( ph /\ ( y e. ( Base ` M ) /\ z e. ( Base ` M ) ) ) -> G e. Mnd )
31 wrdco 
 |-  ( ( y e. Word I /\ A : I --> B ) -> ( A o. y ) e. Word B )
32 23 26 31 syl2anc 
 |-  ( ( ph /\ ( y e. ( Base ` M ) /\ z e. ( Base ` M ) ) ) -> ( A o. y ) e. Word B )
33 wrdco 
 |-  ( ( z e. Word I /\ A : I --> B ) -> ( A o. z ) e. Word B )
34 25 26 33 syl2anc 
 |-  ( ( ph /\ ( y e. ( Base ` M ) /\ z e. ( Base ` M ) ) ) -> ( A o. z ) e. Word B )
35 eqid 
 |-  ( +g ` G ) = ( +g ` G )
36 2 35 gsumccat 
 |-  ( ( G e. Mnd /\ ( A o. y ) e. Word B /\ ( A o. z ) e. Word B ) -> ( G gsum ( ( A o. y ) ++ ( A o. z ) ) ) = ( ( G gsum ( A o. y ) ) ( +g ` G ) ( G gsum ( A o. z ) ) ) )
37 30 32 34 36 syl3anc 
 |-  ( ( ph /\ ( y e. ( Base ` M ) /\ z e. ( Base ` M ) ) ) -> ( G gsum ( ( A o. y ) ++ ( A o. z ) ) ) = ( ( G gsum ( A o. y ) ) ( +g ` G ) ( G gsum ( A o. z ) ) ) )
38 29 37 eqtrd 
 |-  ( ( ph /\ ( y e. ( Base ` M ) /\ z e. ( Base ` M ) ) ) -> ( G gsum ( A o. ( y ++ z ) ) ) = ( ( G gsum ( A o. y ) ) ( +g ` G ) ( G gsum ( A o. z ) ) ) )
39 eqid 
 |-  ( +g ` M ) = ( +g ` M )
40 1 17 39 frmdadd 
 |-  ( ( y e. ( Base ` M ) /\ z e. ( Base ` M ) ) -> ( y ( +g ` M ) z ) = ( y ++ z ) )
41 40 adantl 
 |-  ( ( ph /\ ( y e. ( Base ` M ) /\ z e. ( Base ` M ) ) ) -> ( y ( +g ` M ) z ) = ( y ++ z ) )
42 41 fveq2d 
 |-  ( ( ph /\ ( y e. ( Base ` M ) /\ z e. ( Base ` M ) ) ) -> ( E ` ( y ( +g ` M ) z ) ) = ( E ` ( y ++ z ) ) )
43 ccatcl 
 |-  ( ( y e. Word I /\ z e. Word I ) -> ( y ++ z ) e. Word I )
44 23 25 43 syl2anc 
 |-  ( ( ph /\ ( y e. ( Base ` M ) /\ z e. ( Base ` M ) ) ) -> ( y ++ z ) e. Word I )
45 coeq2 
 |-  ( x = ( y ++ z ) -> ( A o. x ) = ( A o. ( y ++ z ) ) )
46 45 oveq2d 
 |-  ( x = ( y ++ z ) -> ( G gsum ( A o. x ) ) = ( G gsum ( A o. ( y ++ z ) ) ) )
47 ovex 
 |-  ( G gsum ( A o. x ) ) e. _V
48 46 3 47 fvmpt3i 
 |-  ( ( y ++ z ) e. Word I -> ( E ` ( y ++ z ) ) = ( G gsum ( A o. ( y ++ z ) ) ) )
49 44 48 syl 
 |-  ( ( ph /\ ( y e. ( Base ` M ) /\ z e. ( Base ` M ) ) ) -> ( E ` ( y ++ z ) ) = ( G gsum ( A o. ( y ++ z ) ) ) )
50 42 49 eqtrd 
 |-  ( ( ph /\ ( y e. ( Base ` M ) /\ z e. ( Base ` M ) ) ) -> ( E ` ( y ( +g ` M ) z ) ) = ( G gsum ( A o. ( y ++ z ) ) ) )
51 coeq2 
 |-  ( x = y -> ( A o. x ) = ( A o. y ) )
52 51 oveq2d 
 |-  ( x = y -> ( G gsum ( A o. x ) ) = ( G gsum ( A o. y ) ) )
53 52 3 47 fvmpt3i 
 |-  ( y e. Word I -> ( E ` y ) = ( G gsum ( A o. y ) ) )
54 coeq2 
 |-  ( x = z -> ( A o. x ) = ( A o. z ) )
55 54 oveq2d 
 |-  ( x = z -> ( G gsum ( A o. x ) ) = ( G gsum ( A o. z ) ) )
56 55 3 47 fvmpt3i 
 |-  ( z e. Word I -> ( E ` z ) = ( G gsum ( A o. z ) ) )
57 53 56 oveqan12d 
 |-  ( ( y e. Word I /\ z e. Word I ) -> ( ( E ` y ) ( +g ` G ) ( E ` z ) ) = ( ( G gsum ( A o. y ) ) ( +g ` G ) ( G gsum ( A o. z ) ) ) )
58 23 25 57 syl2anc 
 |-  ( ( ph /\ ( y e. ( Base ` M ) /\ z e. ( Base ` M ) ) ) -> ( ( E ` y ) ( +g ` G ) ( E ` z ) ) = ( ( G gsum ( A o. y ) ) ( +g ` G ) ( G gsum ( A o. z ) ) ) )
59 38 50 58 3eqtr4d 
 |-  ( ( ph /\ ( y e. ( Base ` M ) /\ z e. ( Base ` M ) ) ) -> ( E ` ( y ( +g ` M ) z ) ) = ( ( E ` y ) ( +g ` G ) ( E ` z ) ) )
60 59 ralrimivva 
 |-  ( ph -> A. y e. ( Base ` M ) A. z e. ( Base ` M ) ( E ` ( y ( +g ` M ) z ) ) = ( ( E ` y ) ( +g ` G ) ( E ` z ) ) )
61 wrd0 
 |-  (/) e. Word I
62 coeq2 
 |-  ( x = (/) -> ( A o. x ) = ( A o. (/) ) )
63 co02 
 |-  ( A o. (/) ) = (/)
64 62 63 eqtrdi 
 |-  ( x = (/) -> ( A o. x ) = (/) )
65 64 oveq2d 
 |-  ( x = (/) -> ( G gsum ( A o. x ) ) = ( G gsum (/) ) )
66 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
67 66 gsum0 
 |-  ( G gsum (/) ) = ( 0g ` G )
68 65 67 eqtrdi 
 |-  ( x = (/) -> ( G gsum ( A o. x ) ) = ( 0g ` G ) )
69 68 3 47 fvmpt3i 
 |-  ( (/) e. Word I -> ( E ` (/) ) = ( 0g ` G ) )
70 61 69 mp1i 
 |-  ( ph -> ( E ` (/) ) = ( 0g ` G ) )
71 21 60 70 3jca 
 |-  ( ph -> ( E : ( Base ` M ) --> B /\ A. y e. ( Base ` M ) A. z e. ( Base ` M ) ( E ` ( y ( +g ` M ) z ) ) = ( ( E ` y ) ( +g ` G ) ( E ` z ) ) /\ ( E ` (/) ) = ( 0g ` G ) ) )
72 1 frmd0 
 |-  (/) = ( 0g ` M )
73 17 2 39 35 72 66 ismhm 
 |-  ( E e. ( M MndHom G ) <-> ( ( M e. Mnd /\ G e. Mnd ) /\ ( E : ( Base ` M ) --> B /\ A. y e. ( Base ` M ) A. z e. ( Base ` M ) ( E ` ( y ( +g ` M ) z ) ) = ( ( E ` y ) ( +g ` G ) ( E ` z ) ) /\ ( E ` (/) ) = ( 0g ` G ) ) ) )
74 8 4 71 73 syl21anbrc 
 |-  ( ph -> E e. ( M MndHom G ) )