Metamath Proof Explorer

Theorem frmdup3

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

Ref Expression
Hypotheses frmdup3.m 
|- M = ( freeMnd ` I )
frmdup3.b 
|- B = ( Base ` G )
frmdup3.u 
|- U = ( varFMnd ` I )
Assertion frmdup3 
|- ( ( G e. Mnd /\ I e. V /\ A : I --> B ) -> E! m e. ( M MndHom G ) ( m o. U ) = A )

Proof

Step Hyp Ref Expression
1 frmdup3.m 
 |-  M = ( freeMnd ` I )
2 frmdup3.b 
 |-  B = ( Base ` G )
3 frmdup3.u 
 |-  U = ( varFMnd ` I )
4 eqid 
 |-  ( x e. Word I |-> ( G gsum ( A o. x ) ) ) = ( x e. Word I |-> ( G gsum ( A o. x ) ) )
5 simp1 
 |-  ( ( G e. Mnd /\ I e. V /\ A : I --> B ) -> G e. Mnd )
6 simp2 
 |-  ( ( G e. Mnd /\ I e. V /\ A : I --> B ) -> I e. V )
7 simp3 
 |-  ( ( G e. Mnd /\ I e. V /\ A : I --> B ) -> A : I --> B )
8 1 2 4 5 6 7 frmdup1 
 |-  ( ( G e. Mnd /\ I e. V /\ A : I --> B ) -> ( x e. Word I |-> ( G gsum ( A o. x ) ) ) e. ( M MndHom G ) )
9 5 adantr 
 |-  ( ( ( G e. Mnd /\ I e. V /\ A : I --> B ) /\ y e. I ) -> G e. Mnd )
10 6 adantr 
 |-  ( ( ( G e. Mnd /\ I e. V /\ A : I --> B ) /\ y e. I ) -> I e. V )
11 7 adantr 
 |-  ( ( ( G e. Mnd /\ I e. V /\ A : I --> B ) /\ y e. I ) -> A : I --> B )
12 simpr 
 |-  ( ( ( G e. Mnd /\ I e. V /\ A : I --> B ) /\ y e. I ) -> y e. I )
13 1 2 4 9 10 11 3 12 frmdup2 
 |-  ( ( ( G e. Mnd /\ I e. V /\ A : I --> B ) /\ y e. I ) -> ( ( x e. Word I |-> ( G gsum ( A o. x ) ) ) ` ( U ` y ) ) = ( A ` y ) )
14 13 mpteq2dva 
 |-  ( ( G e. Mnd /\ I e. V /\ A : I --> B ) -> ( y e. I |-> ( ( x e. Word I |-> ( G gsum ( A o. x ) ) ) ` ( U ` y ) ) ) = ( y e. I |-> ( A ` y ) ) )
15 eqid 
 |-  ( Base ` M ) = ( Base ` M )
16 15 2 mhmf 
 |-  ( ( x e. Word I |-> ( G gsum ( A o. x ) ) ) e. ( M MndHom G ) -> ( x e. Word I |-> ( G gsum ( A o. x ) ) ) : ( Base ` M ) --> B )
17 8 16 syl 
 |-  ( ( G e. Mnd /\ I e. V /\ A : I --> B ) -> ( x e. Word I |-> ( G gsum ( A o. x ) ) ) : ( Base ` M ) --> B )
18 3 vrmdf 
 |-  ( I e. V -> U : I --> Word I )
19 18 3ad2ant2 
 |-  ( ( G e. Mnd /\ I e. V /\ A : I --> B ) -> U : I --> Word I )
20 1 15 frmdbas 
 |-  ( I e. V -> ( Base ` M ) = Word I )
21 20 3ad2ant2 
 |-  ( ( G e. Mnd /\ I e. V /\ A : I --> B ) -> ( Base ` M ) = Word I )
22 21 feq3d 
 |-  ( ( G e. Mnd /\ I e. V /\ A : I --> B ) -> ( U : I --> ( Base ` M ) <-> U : I --> Word I ) )
23 19 22 mpbird 
 |-  ( ( G e. Mnd /\ I e. V /\ A : I --> B ) -> U : I --> ( Base ` M ) )
24 fcompt 
 |-  ( ( ( x e. Word I |-> ( G gsum ( A o. x ) ) ) : ( Base ` M ) --> B /\ U : I --> ( Base ` M ) ) -> ( ( x e. Word I |-> ( G gsum ( A o. x ) ) ) o. U ) = ( y e. I |-> ( ( x e. Word I |-> ( G gsum ( A o. x ) ) ) ` ( U ` y ) ) ) )
25 17 23 24 syl2anc 
 |-  ( ( G e. Mnd /\ I e. V /\ A : I --> B ) -> ( ( x e. Word I |-> ( G gsum ( A o. x ) ) ) o. U ) = ( y e. I |-> ( ( x e. Word I |-> ( G gsum ( A o. x ) ) ) ` ( U ` y ) ) ) )
26 7 feqmptd 
 |-  ( ( G e. Mnd /\ I e. V /\ A : I --> B ) -> A = ( y e. I |-> ( A ` y ) ) )
27 14 25 26 3eqtr4d 
 |-  ( ( G e. Mnd /\ I e. V /\ A : I --> B ) -> ( ( x e. Word I |-> ( G gsum ( A o. x ) ) ) o. U ) = A )
28 1 2 3 frmdup3lem 
 |-  ( ( ( G e. Mnd /\ I e. V /\ A : I --> B ) /\ ( m e. ( M MndHom G ) /\ ( m o. U ) = A ) ) -> m = ( x e. Word I |-> ( G gsum ( A o. x ) ) ) )
29 28 expr 
 |-  ( ( ( G e. Mnd /\ I e. V /\ A : I --> B ) /\ m e. ( M MndHom G ) ) -> ( ( m o. U ) = A -> m = ( x e. Word I |-> ( G gsum ( A o. x ) ) ) ) )
30 29 ralrimiva 
 |-  ( ( G e. Mnd /\ I e. V /\ A : I --> B ) -> A. m e. ( M MndHom G ) ( ( m o. U ) = A -> m = ( x e. Word I |-> ( G gsum ( A o. x ) ) ) ) )
31 coeq1 
 |-  ( m = ( x e. Word I |-> ( G gsum ( A o. x ) ) ) -> ( m o. U ) = ( ( x e. Word I |-> ( G gsum ( A o. x ) ) ) o. U ) )
32 31 eqeq1d 
 |-  ( m = ( x e. Word I |-> ( G gsum ( A o. x ) ) ) -> ( ( m o. U ) = A <-> ( ( x e. Word I |-> ( G gsum ( A o. x ) ) ) o. U ) = A ) )
33 32 eqreu 
 |-  ( ( ( x e. Word I |-> ( G gsum ( A o. x ) ) ) e. ( M MndHom G ) /\ ( ( x e. Word I |-> ( G gsum ( A o. x ) ) ) o. U ) = A /\ A. m e. ( M MndHom G ) ( ( m o. U ) = A -> m = ( x e. Word I |-> ( G gsum ( A o. x ) ) ) ) ) -> E! m e. ( M MndHom G ) ( m o. U ) = A )
34 8 27 30 33 syl3anc 
 |-  ( ( G e. Mnd /\ I e. V /\ A : I --> B ) -> E! m e. ( M MndHom G ) ( m o. U ) = A )