Metamath Proof Explorer

Theorem frgpupval

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)

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 frgpupval
`|- ( ( ph /\ A e. W ) -> ( E ` [ A ] .~ ) = ( H gsum ( T o. A ) ) )`

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 ovexd
` |-  ( ( ph /\ g e. W ) -> ( H gsum ( T o. g ) ) e. _V )`
13 7 8 efger
` |-  .~ Er W`
14 13 a1i
` |-  ( ph -> .~ Er W )`
15 7 fvexi
` |-  W e. _V`
16 15 a1i
` |-  ( ph -> W e. _V )`
17 coeq2
` |-  ( g = A -> ( T o. g ) = ( T o. A ) )`
18 17 oveq2d
` |-  ( g = A -> ( H gsum ( T o. g ) ) = ( H gsum ( T o. A ) ) )`
19 1 2 3 4 5 6 7 8 9 10 11 frgpupf
` |-  ( ph -> E : X --> B )`
20 19 ffund
` |-  ( ph -> Fun E )`
21 11 12 14 16 18 20 qliftval
` |-  ( ( ph /\ A e. W ) -> ( E ` [ A ] .~ ) = ( H gsum ( T o. A ) ) )`