Metamath Proof Explorer


Theorem frgpuptf

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 )
Assertion frgpuptf
|- ( ph -> T : ( I X. 2o ) --> B )

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 6 ffvelrnda
 |-  ( ( ph /\ y e. I ) -> ( F ` y ) e. B )
8 7 adantrr
 |-  ( ( ph /\ ( y e. I /\ z e. 2o ) ) -> ( F ` y ) e. B )
9 1 2 grpinvcl
 |-  ( ( H e. Grp /\ ( F ` y ) e. B ) -> ( N ` ( F ` y ) ) e. B )
10 4 8 9 syl2an2r
 |-  ( ( ph /\ ( y e. I /\ z e. 2o ) ) -> ( N ` ( F ` y ) ) e. B )
11 8 10 ifcld
 |-  ( ( ph /\ ( y e. I /\ z e. 2o ) ) -> if ( z = (/) , ( F ` y ) , ( N ` ( F ` y ) ) ) e. B )
12 11 ralrimivva
 |-  ( ph -> A. y e. I A. z e. 2o if ( z = (/) , ( F ` y ) , ( N ` ( F ` y ) ) ) e. B )
13 3 fmpo
 |-  ( A. y e. I A. z e. 2o if ( z = (/) , ( F ` y ) , ( N ` ( F ` y ) ) ) e. B <-> T : ( I X. 2o ) --> B )
14 12 13 sylib
 |-  ( ph -> T : ( I X. 2o ) --> B )