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 ) ) )