This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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