Metamath Proof Explorer

Theorem frgpup1

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, 2-Oct-2015) (Revised by Mario Carneiro, 28-Feb-2016)

Ref Expression
Hypotheses frgpup.b 
|- B = ( Base ` H )
frgpup.n 
|- N = ( invg ` H )
frgpup.t 
|- T = ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( N ` ( F ` y ) ) ) )
frgpup.h 
|- ( ph -> H e. Grp )
frgpup.i 
|- ( ph -> I e. V )
frgpup.a 
|- ( ph -> F : I --> B )
frgpup.w 
|- W = ( _I ` Word ( I X. 2o ) )
frgpup.r 
|- .~ = ( ~FG ` I )
frgpup.g 
|- G = ( freeGrp ` I )
frgpup.x 
|- X = ( Base ` G )
frgpup.e 
|- E = ran ( g e. W |-> <. [ g ] .~ , ( H gsum ( T o. g ) ) >. )
Assertion frgpup1 
|- ( ph -> E e. ( G GrpHom H ) )

Proof

Step Hyp Ref Expression
1 frgpup.b 
 |-  B = ( Base ` H )
2 frgpup.n 
 |-  N = ( invg ` H )
3 frgpup.t 
 |-  T = ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( N ` ( F ` y ) ) ) )
4 frgpup.h 
 |-  ( ph -> H e. Grp )
5 frgpup.i 
 |-  ( ph -> I e. V )
6 frgpup.a 
 |-  ( ph -> F : I --> B )
7 frgpup.w 
 |-  W = ( _I ` Word ( I X. 2o ) )
8 frgpup.r 
 |-  .~ = ( ~FG ` I )
9 frgpup.g 
 |-  G = ( freeGrp ` I )
10 frgpup.x 
 |-  X = ( Base ` G )
11 frgpup.e 
 |-  E = ran ( g e. W |-> <. [ g ] .~ , ( H gsum ( T o. g ) ) >. )
12 eqid 
 |-  ( +g ` G ) = ( +g ` G )
13 eqid 
 |-  ( +g ` H ) = ( +g ` H )
14 9 frgpgrp 
 |-  ( I e. V -> G e. Grp )
15 5 14 syl 
 |-  ( ph -> G e. Grp )
16 1 2 3 4 5 6 7 8 9 10 11 frgpupf 
 |-  ( ph -> E : X --> B )
17 eqid 
 |-  ( freeMnd ` ( I X. 2o ) ) = ( freeMnd ` ( I X. 2o ) )
18 9 17 8 frgpval 
 |-  ( I e. V -> G = ( ( freeMnd ` ( I X. 2o ) ) /s .~ ) )
19 5 18 syl 
 |-  ( ph -> G = ( ( freeMnd ` ( I X. 2o ) ) /s .~ ) )
20 2on 
 |-  2o e. On
21 xpexg 
 |-  ( ( I e. V /\ 2o e. On ) -> ( I X. 2o ) e. _V )
22 5 20 21 sylancl 
 |-  ( ph -> ( I X. 2o ) e. _V )
23 wrdexg 
 |-  ( ( I X. 2o ) e. _V -> Word ( I X. 2o ) e. _V )
24 fvi 
 |-  ( Word ( I X. 2o ) e. _V -> ( _I ` Word ( I X. 2o ) ) = Word ( I X. 2o ) )
25 22 23 24 3syl 
 |-  ( ph -> ( _I ` Word ( I X. 2o ) ) = Word ( I X. 2o ) )
26 7 25 syl5eq 
 |-  ( ph -> W = Word ( I X. 2o ) )
27 eqid 
 |-  ( Base ` ( freeMnd ` ( I X. 2o ) ) ) = ( Base ` ( freeMnd ` ( I X. 2o ) ) )
28 17 27 frmdbas 
 |-  ( ( I X. 2o ) e. _V -> ( Base ` ( freeMnd ` ( I X. 2o ) ) ) = Word ( I X. 2o ) )
29 22 28 syl 
 |-  ( ph -> ( Base ` ( freeMnd ` ( I X. 2o ) ) ) = Word ( I X. 2o ) )
30 26 29 eqtr4d 
 |-  ( ph -> W = ( Base ` ( freeMnd ` ( I X. 2o ) ) ) )
31 8 fvexi 
 |-  .~ e. _V
32 31 a1i 
 |-  ( ph -> .~ e. _V )
33 fvexd 
 |-  ( ph -> ( freeMnd ` ( I X. 2o ) ) e. _V )
34 19 30 32 33 qusbas 
 |-  ( ph -> ( W /. .~ ) = ( Base ` G ) )
35 10 34 eqtr4id 
 |-  ( ph -> X = ( W /. .~ ) )
36 eqimss 
 |-  ( X = ( W /. .~ ) -> X C_ ( W /. .~ ) )
37 35 36 syl 
 |-  ( ph -> X C_ ( W /. .~ ) )
38 37 adantr 
 |-  ( ( ph /\ a e. X ) -> X C_ ( W /. .~ ) )
39 38 sselda 
 |-  ( ( ( ph /\ a e. X ) /\ c e. X ) -> c e. ( W /. .~ ) )
40 eqid 
 |-  ( W /. .~ ) = ( W /. .~ )
41 oveq2 
 |-  ( [ u ] .~ = c -> ( a ( +g ` G ) [ u ] .~ ) = ( a ( +g ` G ) c ) )
42 41 fveq2d 
 |-  ( [ u ] .~ = c -> ( E ` ( a ( +g ` G ) [ u ] .~ ) ) = ( E ` ( a ( +g ` G ) c ) ) )
43 fveq2 
 |-  ( [ u ] .~ = c -> ( E ` [ u ] .~ ) = ( E ` c ) )
44 43 oveq2d 
 |-  ( [ u ] .~ = c -> ( ( E ` a ) ( +g ` H ) ( E ` [ u ] .~ ) ) = ( ( E ` a ) ( +g ` H ) ( E ` c ) ) )
45 42 44 eqeq12d 
 |-  ( [ u ] .~ = c -> ( ( E ` ( a ( +g ` G ) [ u ] .~ ) ) = ( ( E ` a ) ( +g ` H ) ( E ` [ u ] .~ ) ) <-> ( E ` ( a ( +g ` G ) c ) ) = ( ( E ` a ) ( +g ` H ) ( E ` c ) ) ) )
46 37 sselda 
 |-  ( ( ph /\ a e. X ) -> a e. ( W /. .~ ) )
47 46 adantlr 
 |-  ( ( ( ph /\ u e. W ) /\ a e. X ) -> a e. ( W /. .~ ) )
48 fvoveq1 
 |-  ( [ t ] .~ = a -> ( E ` ( [ t ] .~ ( +g ` G ) [ u ] .~ ) ) = ( E ` ( a ( +g ` G ) [ u ] .~ ) ) )
49 fveq2 
 |-  ( [ t ] .~ = a -> ( E ` [ t ] .~ ) = ( E ` a ) )
50 49 oveq1d 
 |-  ( [ t ] .~ = a -> ( ( E ` [ t ] .~ ) ( +g ` H ) ( E ` [ u ] .~ ) ) = ( ( E ` a ) ( +g ` H ) ( E ` [ u ] .~ ) ) )
51 48 50 eqeq12d 
 |-  ( [ t ] .~ = a -> ( ( E ` ( [ t ] .~ ( +g ` G ) [ u ] .~ ) ) = ( ( E ` [ t ] .~ ) ( +g ` H ) ( E ` [ u ] .~ ) ) <-> ( E ` ( a ( +g ` G ) [ u ] .~ ) ) = ( ( E ` a ) ( +g ` H ) ( E ` [ u ] .~ ) ) ) )
52 fviss 
 |-  ( _I ` Word ( I X. 2o ) ) C_ Word ( I X. 2o )
53 7 52 eqsstri 
 |-  W C_ Word ( I X. 2o )
54 53 sseli 
 |-  ( t e. W -> t e. Word ( I X. 2o ) )
55 53 sseli 
 |-  ( u e. W -> u e. Word ( I X. 2o ) )
56 ccatcl 
 |-  ( ( t e. Word ( I X. 2o ) /\ u e. Word ( I X. 2o ) ) -> ( t ++ u ) e. Word ( I X. 2o ) )
57 54 55 56 syl2an 
 |-  ( ( t e. W /\ u e. W ) -> ( t ++ u ) e. Word ( I X. 2o ) )
58 7 efgrcl 
 |-  ( t e. W -> ( I e. _V /\ W = Word ( I X. 2o ) ) )
59 58 adantr 
 |-  ( ( t e. W /\ u e. W ) -> ( I e. _V /\ W = Word ( I X. 2o ) ) )
60 59 simprd 
 |-  ( ( t e. W /\ u e. W ) -> W = Word ( I X. 2o ) )
61 57 60 eleqtrrd 
 |-  ( ( t e. W /\ u e. W ) -> ( t ++ u ) e. W )
62 1 2 3 4 5 6 7 8 9 10 11 frgpupval 
 |-  ( ( ph /\ ( t ++ u ) e. W ) -> ( E ` [ ( t ++ u ) ] .~ ) = ( H gsum ( T o. ( t ++ u ) ) ) )
63 61 62 sylan2 
 |-  ( ( ph /\ ( t e. W /\ u e. W ) ) -> ( E ` [ ( t ++ u ) ] .~ ) = ( H gsum ( T o. ( t ++ u ) ) ) )
64 54 ad2antrl 
 |-  ( ( ph /\ ( t e. W /\ u e. W ) ) -> t e. Word ( I X. 2o ) )
65 55 ad2antll 
 |-  ( ( ph /\ ( t e. W /\ u e. W ) ) -> u e. Word ( I X. 2o ) )
66 1 2 3 4 5 6 frgpuptf 
 |-  ( ph -> T : ( I X. 2o ) --> B )
67 66 adantr 
 |-  ( ( ph /\ ( t e. W /\ u e. W ) ) -> T : ( I X. 2o ) --> B )
68 ccatco 
 |-  ( ( t e. Word ( I X. 2o ) /\ u e. Word ( I X. 2o ) /\ T : ( I X. 2o ) --> B ) -> ( T o. ( t ++ u ) ) = ( ( T o. t ) ++ ( T o. u ) ) )
69 64 65 67 68 syl3anc 
 |-  ( ( ph /\ ( t e. W /\ u e. W ) ) -> ( T o. ( t ++ u ) ) = ( ( T o. t ) ++ ( T o. u ) ) )
70 69 oveq2d 
 |-  ( ( ph /\ ( t e. W /\ u e. W ) ) -> ( H gsum ( T o. ( t ++ u ) ) ) = ( H gsum ( ( T o. t ) ++ ( T o. u ) ) ) )
71 grpmnd 
 |-  ( H e. Grp -> H e. Mnd )
72 4 71 syl 
 |-  ( ph -> H e. Mnd )
73 72 adantr 
 |-  ( ( ph /\ ( t e. W /\ u e. W ) ) -> H e. Mnd )
74 wrdco 
 |-  ( ( t e. Word ( I X. 2o ) /\ T : ( I X. 2o ) --> B ) -> ( T o. t ) e. Word B )
75 54 66 74 syl2anr 
 |-  ( ( ph /\ t e. W ) -> ( T o. t ) e. Word B )
76 75 adantrr 
 |-  ( ( ph /\ ( t e. W /\ u e. W ) ) -> ( T o. t ) e. Word B )
77 wrdco 
 |-  ( ( u e. Word ( I X. 2o ) /\ T : ( I X. 2o ) --> B ) -> ( T o. u ) e. Word B )
78 65 67 77 syl2anc 
 |-  ( ( ph /\ ( t e. W /\ u e. W ) ) -> ( T o. u ) e. Word B )
79 1 13 gsumccat 
 |-  ( ( H e. Mnd /\ ( T o. t ) e. Word B /\ ( T o. u ) e. Word B ) -> ( H gsum ( ( T o. t ) ++ ( T o. u ) ) ) = ( ( H gsum ( T o. t ) ) ( +g ` H ) ( H gsum ( T o. u ) ) ) )
80 73 76 78 79 syl3anc 
 |-  ( ( ph /\ ( t e. W /\ u e. W ) ) -> ( H gsum ( ( T o. t ) ++ ( T o. u ) ) ) = ( ( H gsum ( T o. t ) ) ( +g ` H ) ( H gsum ( T o. u ) ) ) )
81 63 70 80 3eqtrd 
 |-  ( ( ph /\ ( t e. W /\ u e. W ) ) -> ( E ` [ ( t ++ u ) ] .~ ) = ( ( H gsum ( T o. t ) ) ( +g ` H ) ( H gsum ( T o. u ) ) ) )
82 7 9 8 12 frgpadd 
 |-  ( ( t e. W /\ u e. W ) -> ( [ t ] .~ ( +g ` G ) [ u ] .~ ) = [ ( t ++ u ) ] .~ )
83 82 adantl 
 |-  ( ( ph /\ ( t e. W /\ u e. W ) ) -> ( [ t ] .~ ( +g ` G ) [ u ] .~ ) = [ ( t ++ u ) ] .~ )
84 83 fveq2d 
 |-  ( ( ph /\ ( t e. W /\ u e. W ) ) -> ( E ` ( [ t ] .~ ( +g ` G ) [ u ] .~ ) ) = ( E ` [ ( t ++ u ) ] .~ ) )
85 1 2 3 4 5 6 7 8 9 10 11 frgpupval 
 |-  ( ( ph /\ t e. W ) -> ( E ` [ t ] .~ ) = ( H gsum ( T o. t ) ) )
86 85 adantrr 
 |-  ( ( ph /\ ( t e. W /\ u e. W ) ) -> ( E ` [ t ] .~ ) = ( H gsum ( T o. t ) ) )
87 1 2 3 4 5 6 7 8 9 10 11 frgpupval 
 |-  ( ( ph /\ u e. W ) -> ( E ` [ u ] .~ ) = ( H gsum ( T o. u ) ) )
88 87 adantrl 
 |-  ( ( ph /\ ( t e. W /\ u e. W ) ) -> ( E ` [ u ] .~ ) = ( H gsum ( T o. u ) ) )
89 86 88 oveq12d 
 |-  ( ( ph /\ ( t e. W /\ u e. W ) ) -> ( ( E ` [ t ] .~ ) ( +g ` H ) ( E ` [ u ] .~ ) ) = ( ( H gsum ( T o. t ) ) ( +g ` H ) ( H gsum ( T o. u ) ) ) )
90 81 84 89 3eqtr4d 
 |-  ( ( ph /\ ( t e. W /\ u e. W ) ) -> ( E ` ( [ t ] .~ ( +g ` G ) [ u ] .~ ) ) = ( ( E ` [ t ] .~ ) ( +g ` H ) ( E ` [ u ] .~ ) ) )
91 90 anass1rs 
 |-  ( ( ( ph /\ u e. W ) /\ t e. W ) -> ( E ` ( [ t ] .~ ( +g ` G ) [ u ] .~ ) ) = ( ( E ` [ t ] .~ ) ( +g ` H ) ( E ` [ u ] .~ ) ) )
92 40 51 91 ectocld 
 |-  ( ( ( ph /\ u e. W ) /\ a e. ( W /. .~ ) ) -> ( E ` ( a ( +g ` G ) [ u ] .~ ) ) = ( ( E ` a ) ( +g ` H ) ( E ` [ u ] .~ ) ) )
93 47 92 syldan 
 |-  ( ( ( ph /\ u e. W ) /\ a e. X ) -> ( E ` ( a ( +g ` G ) [ u ] .~ ) ) = ( ( E ` a ) ( +g ` H ) ( E ` [ u ] .~ ) ) )
94 93 an32s 
 |-  ( ( ( ph /\ a e. X ) /\ u e. W ) -> ( E ` ( a ( +g ` G ) [ u ] .~ ) ) = ( ( E ` a ) ( +g ` H ) ( E ` [ u ] .~ ) ) )
95 40 45 94 ectocld 
 |-  ( ( ( ph /\ a e. X ) /\ c e. ( W /. .~ ) ) -> ( E ` ( a ( +g ` G ) c ) ) = ( ( E ` a ) ( +g ` H ) ( E ` c ) ) )
96 39 95 syldan 
 |-  ( ( ( ph /\ a e. X ) /\ c e. X ) -> ( E ` ( a ( +g ` G ) c ) ) = ( ( E ` a ) ( +g ` H ) ( E ` c ) ) )
97 96 anasss 
 |-  ( ( ph /\ ( a e. X /\ c e. X ) ) -> ( E ` ( a ( +g ` G ) c ) ) = ( ( E ` a ) ( +g ` H ) ( E ` c ) ) )
98 10 1 12 13 15 4 16 97 isghmd 
 |-  ( ph -> E e. ( G GrpHom H ) )