Metamath Proof Explorer

Theorem frgpup3

Description: Universal property of the free monoid by existential uniqueness. (Contributed by Mario Carneiro, 2-Oct-2015) (Revised by Mario Carneiro, 28-Feb-2016)

Ref Expression
Hypotheses frgpup3.g 
|- G = ( freeGrp ` I )
frgpup3.b 
|- B = ( Base ` H )
frgpup3.u 
|- U = ( varFGrp ` I )
Assertion frgpup3 
|- ( ( H e. Grp /\ I e. V /\ F : I --> B ) -> E! m e. ( G GrpHom H ) ( m o. U ) = F )

Proof

Step Hyp Ref Expression
1 frgpup3.g 
 |-  G = ( freeGrp ` I )
2 frgpup3.b 
 |-  B = ( Base ` H )
3 frgpup3.u 
 |-  U = ( varFGrp ` I )
4 eqid 
 |-  ( invg ` H ) = ( invg ` H )
5 eqid 
 |-  ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( ( invg ` H ) ` ( F ` y ) ) ) ) = ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( ( invg ` H ) ` ( F ` y ) ) ) )
6 simp1 
 |-  ( ( H e. Grp /\ I e. V /\ F : I --> B ) -> H e. Grp )
7 simp2 
 |-  ( ( H e. Grp /\ I e. V /\ F : I --> B ) -> I e. V )
8 simp3 
 |-  ( ( H e. Grp /\ I e. V /\ F : I --> B ) -> F : I --> B )
9 eqid 
 |-  ( _I ` Word ( I X. 2o ) ) = ( _I ` Word ( I X. 2o ) )
10 eqid 
 |-  ( ~FG ` I ) = ( ~FG ` I )
11 eqid 
 |-  ( Base ` G ) = ( Base ` G )
12 eqid 
 |-  ran ( g e. ( _I ` Word ( I X. 2o ) ) |-> <. [ g ] ( ~FG ` I ) , ( H gsum ( ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( ( invg ` H ) ` ( F ` y ) ) ) ) o. g ) ) >. ) = ran ( g e. ( _I ` Word ( I X. 2o ) ) |-> <. [ g ] ( ~FG ` I ) , ( H gsum ( ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( ( invg ` H ) ` ( F ` y ) ) ) ) o. g ) ) >. )
13 2 4 5 6 7 8 9 10 1 11 12 frgpup1 
 |-  ( ( H e. Grp /\ I e. V /\ F : I --> B ) -> ran ( g e. ( _I ` Word ( I X. 2o ) ) |-> <. [ g ] ( ~FG ` I ) , ( H gsum ( ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( ( invg ` H ) ` ( F ` y ) ) ) ) o. g ) ) >. ) e. ( G GrpHom H ) )
14 6 adantr 
 |-  ( ( ( H e. Grp /\ I e. V /\ F : I --> B ) /\ k e. I ) -> H e. Grp )
15 7 adantr 
 |-  ( ( ( H e. Grp /\ I e. V /\ F : I --> B ) /\ k e. I ) -> I e. V )
16 8 adantr 
 |-  ( ( ( H e. Grp /\ I e. V /\ F : I --> B ) /\ k e. I ) -> F : I --> B )
17 simpr 
 |-  ( ( ( H e. Grp /\ I e. V /\ F : I --> B ) /\ k e. I ) -> k e. I )
18 2 4 5 14 15 16 9 10 1 11 12 3 17 frgpup2 
 |-  ( ( ( H e. Grp /\ I e. V /\ F : I --> B ) /\ k e. I ) -> ( ran ( g e. ( _I ` Word ( I X. 2o ) ) |-> <. [ g ] ( ~FG ` I ) , ( H gsum ( ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( ( invg ` H ) ` ( F ` y ) ) ) ) o. g ) ) >. ) ` ( U ` k ) ) = ( F ` k ) )
19 18 mpteq2dva 
 |-  ( ( H e. Grp /\ I e. V /\ F : I --> B ) -> ( k e. I |-> ( ran ( g e. ( _I ` Word ( I X. 2o ) ) |-> <. [ g ] ( ~FG ` I ) , ( H gsum ( ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( ( invg ` H ) ` ( F ` y ) ) ) ) o. g ) ) >. ) ` ( U ` k ) ) ) = ( k e. I |-> ( F ` k ) ) )
20 11 2 ghmf 
 |-  ( ran ( g e. ( _I ` Word ( I X. 2o ) ) |-> <. [ g ] ( ~FG ` I ) , ( H gsum ( ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( ( invg ` H ) ` ( F ` y ) ) ) ) o. g ) ) >. ) e. ( G GrpHom H ) -> ran ( g e. ( _I ` Word ( I X. 2o ) ) |-> <. [ g ] ( ~FG ` I ) , ( H gsum ( ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( ( invg ` H ) ` ( F ` y ) ) ) ) o. g ) ) >. ) : ( Base ` G ) --> B )
21 13 20 syl 
 |-  ( ( H e. Grp /\ I e. V /\ F : I --> B ) -> ran ( g e. ( _I ` Word ( I X. 2o ) ) |-> <. [ g ] ( ~FG ` I ) , ( H gsum ( ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( ( invg ` H ) ` ( F ` y ) ) ) ) o. g ) ) >. ) : ( Base ` G ) --> B )
22 10 3 1 11 vrgpf 
 |-  ( I e. V -> U : I --> ( Base ` G ) )
23 7 22 syl 
 |-  ( ( H e. Grp /\ I e. V /\ F : I --> B ) -> U : I --> ( Base ` G ) )
24 fcompt 
 |-  ( ( ran ( g e. ( _I ` Word ( I X. 2o ) ) |-> <. [ g ] ( ~FG ` I ) , ( H gsum ( ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( ( invg ` H ) ` ( F ` y ) ) ) ) o. g ) ) >. ) : ( Base ` G ) --> B /\ U : I --> ( Base ` G ) ) -> ( ran ( g e. ( _I ` Word ( I X. 2o ) ) |-> <. [ g ] ( ~FG ` I ) , ( H gsum ( ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( ( invg ` H ) ` ( F ` y ) ) ) ) o. g ) ) >. ) o. U ) = ( k e. I |-> ( ran ( g e. ( _I ` Word ( I X. 2o ) ) |-> <. [ g ] ( ~FG ` I ) , ( H gsum ( ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( ( invg ` H ) ` ( F ` y ) ) ) ) o. g ) ) >. ) ` ( U ` k ) ) ) )
25 21 23 24 syl2anc 
 |-  ( ( H e. Grp /\ I e. V /\ F : I --> B ) -> ( ran ( g e. ( _I ` Word ( I X. 2o ) ) |-> <. [ g ] ( ~FG ` I ) , ( H gsum ( ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( ( invg ` H ) ` ( F ` y ) ) ) ) o. g ) ) >. ) o. U ) = ( k e. I |-> ( ran ( g e. ( _I ` Word ( I X. 2o ) ) |-> <. [ g ] ( ~FG ` I ) , ( H gsum ( ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( ( invg ` H ) ` ( F ` y ) ) ) ) o. g ) ) >. ) ` ( U ` k ) ) ) )
26 8 feqmptd 
 |-  ( ( H e. Grp /\ I e. V /\ F : I --> B ) -> F = ( k e. I |-> ( F ` k ) ) )
27 19 25 26 3eqtr4d 
 |-  ( ( H e. Grp /\ I e. V /\ F : I --> B ) -> ( ran ( g e. ( _I ` Word ( I X. 2o ) ) |-> <. [ g ] ( ~FG ` I ) , ( H gsum ( ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( ( invg ` H ) ` ( F ` y ) ) ) ) o. g ) ) >. ) o. U ) = F )
28 6 adantr 
 |-  ( ( ( H e. Grp /\ I e. V /\ F : I --> B ) /\ ( m e. ( G GrpHom H ) /\ ( m o. U ) = F ) ) -> H e. Grp )
29 7 adantr 
 |-  ( ( ( H e. Grp /\ I e. V /\ F : I --> B ) /\ ( m e. ( G GrpHom H ) /\ ( m o. U ) = F ) ) -> I e. V )
30 8 adantr 
 |-  ( ( ( H e. Grp /\ I e. V /\ F : I --> B ) /\ ( m e. ( G GrpHom H ) /\ ( m o. U ) = F ) ) -> F : I --> B )
31 simprl 
 |-  ( ( ( H e. Grp /\ I e. V /\ F : I --> B ) /\ ( m e. ( G GrpHom H ) /\ ( m o. U ) = F ) ) -> m e. ( G GrpHom H ) )
32 simprr 
 |-  ( ( ( H e. Grp /\ I e. V /\ F : I --> B ) /\ ( m e. ( G GrpHom H ) /\ ( m o. U ) = F ) ) -> ( m o. U ) = F )
33 2 4 5 28 29 30 9 10 1 11 12 3 31 32 frgpup3lem 
 |-  ( ( ( H e. Grp /\ I e. V /\ F : I --> B ) /\ ( m e. ( G GrpHom H ) /\ ( m o. U ) = F ) ) -> m = ran ( g e. ( _I ` Word ( I X. 2o ) ) |-> <. [ g ] ( ~FG ` I ) , ( H gsum ( ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( ( invg ` H ) ` ( F ` y ) ) ) ) o. g ) ) >. ) )
34 33 expr 
 |-  ( ( ( H e. Grp /\ I e. V /\ F : I --> B ) /\ m e. ( G GrpHom H ) ) -> ( ( m o. U ) = F -> m = ran ( g e. ( _I ` Word ( I X. 2o ) ) |-> <. [ g ] ( ~FG ` I ) , ( H gsum ( ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( ( invg ` H ) ` ( F ` y ) ) ) ) o. g ) ) >. ) ) )
35 34 ralrimiva 
 |-  ( ( H e. Grp /\ I e. V /\ F : I --> B ) -> A. m e. ( G GrpHom H ) ( ( m o. U ) = F -> m = ran ( g e. ( _I ` Word ( I X. 2o ) ) |-> <. [ g ] ( ~FG ` I ) , ( H gsum ( ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( ( invg ` H ) ` ( F ` y ) ) ) ) o. g ) ) >. ) ) )
36 coeq1 
 |-  ( m = ran ( g e. ( _I ` Word ( I X. 2o ) ) |-> <. [ g ] ( ~FG ` I ) , ( H gsum ( ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( ( invg ` H ) ` ( F ` y ) ) ) ) o. g ) ) >. ) -> ( m o. U ) = ( ran ( g e. ( _I ` Word ( I X. 2o ) ) |-> <. [ g ] ( ~FG ` I ) , ( H gsum ( ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( ( invg ` H ) ` ( F ` y ) ) ) ) o. g ) ) >. ) o. U ) )
37 36 eqeq1d 
 |-  ( m = ran ( g e. ( _I ` Word ( I X. 2o ) ) |-> <. [ g ] ( ~FG ` I ) , ( H gsum ( ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( ( invg ` H ) ` ( F ` y ) ) ) ) o. g ) ) >. ) -> ( ( m o. U ) = F <-> ( ran ( g e. ( _I ` Word ( I X. 2o ) ) |-> <. [ g ] ( ~FG ` I ) , ( H gsum ( ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( ( invg ` H ) ` ( F ` y ) ) ) ) o. g ) ) >. ) o. U ) = F ) )
38 37 eqreu 
 |-  ( ( ran ( g e. ( _I ` Word ( I X. 2o ) ) |-> <. [ g ] ( ~FG ` I ) , ( H gsum ( ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( ( invg ` H ) ` ( F ` y ) ) ) ) o. g ) ) >. ) e. ( G GrpHom H ) /\ ( ran ( g e. ( _I ` Word ( I X. 2o ) ) |-> <. [ g ] ( ~FG ` I ) , ( H gsum ( ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( ( invg ` H ) ` ( F ` y ) ) ) ) o. g ) ) >. ) o. U ) = F /\ A. m e. ( G GrpHom H ) ( ( m o. U ) = F -> m = ran ( g e. ( _I ` Word ( I X. 2o ) ) |-> <. [ g ] ( ~FG ` I ) , ( H gsum ( ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( ( invg ` H ) ` ( F ` y ) ) ) ) o. g ) ) >. ) ) ) -> E! m e. ( G GrpHom H ) ( m o. U ) = F )
39 13 27 35 38 syl3anc 
 |-  ( ( H e. Grp /\ I e. V /\ F : I --> B ) -> E! m e. ( G GrpHom H ) ( m o. U ) = F )