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 )