Theorem mhmf 15557

Description: A monoid homomorphism is a function. (Contributed by Mario Carneiro, 7-Mar-2015.)

Hypotheses

Ref	Expression
mhmf.b	|- B = ( Base ` S )
mhmf.c	|- C = ( Base ` T )

Assertion

Ref	Expression
mhmf	|- ( F e. ( S MndHom T ) -> F : B --> C )

Proof of Theorem mhmf

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mhmf.b	. . . 4 |- B = ( Base ` S )
2		mhmf.c	. . . 4 |- C = ( Base ` T )
3		eqid 2450	. . . 4 |- ( +g ` S ) = ( +g ` S )
4		eqid 2450	. . . 4 |- ( +g ` T ) = ( +g ` T )
5		eqid 2450	. . . 4 |- ( 0g ` S ) = ( 0g ` S )
6		eqid 2450	. . . 4 |- ( 0g ` T ) = ( 0g ` T )
7	1, 2, 3, 4, 5, 6	ismhm 15554	. . 3 |- ( F e. ( S MndHom T ) <-> ( ( S e. Mnd /\ T e. Mnd ) /\ ( F : B --> C /\ A. x e. B A. y e. B ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) /\ ( F ` ( 0g ` S ) ) = ( 0g ` T ) ) ) )
8	7	simprbi 464	. 2 |- ( F e. ( S MndHom T ) -> ( F : B --> C /\ A. x e. B A. y e. B ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) /\ ( F ` ( 0g ` S ) ) = ( 0g ` T ) ) )
9	8	simp1d 1000	1 |- ( F e. ( S MndHom T ) -> F : B --> C )

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 965   = wceq 1370   e. wcel 1757   A.wral 2792   -->wf 5498   ` cfv 5502  (class class class)co 6176   Basecbs 14262   +g cplusg 14326   0gc0g 14466   Mndcmnd 15497   MndHom cmhm 15550

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-sep 4497  ax-nul 4505  ax-pow 4554  ax-pr 4615  ax-un 6458

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-eu 2263  df-mo 2264  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-ral 2797  df-rex 2798  df-rab 2801  df-v 3056  df-sbc 3271  df-dif 3415  df-un 3417  df-in 3419  df-ss 3426  df-nul 3722  df-if 3876  df-pw 3946  df-sn 3962  df-pr 3964  df-op 3968  df-uni 4176  df-br 4377  df-opab 4435  df-id 4720  df-xp 4930  df-rel 4931  df-cnv 4932  df-co 4933  df-dm 4934  df-rn 4935  df-iota 5465  df-fun 5504  df-fn 5505  df-f 5506  df-fv 5510  df-ov 6179  df-oprab 6180  df-mpt2 6181  df-map 7302  df-mhm 15552

This theorem is referenced by:  mhmf1o  15561  resmhm  15575  resmhm2  15576  resmhm2b  15577  mhmco  15578  mhmima  15579  mhmeql  15580  pwsco2mhm  15587  gsumwmhm  15611  frmdup3  15632  mhmmulg  15747  ghmmhmb  15846  cntzmhm  15944  cntzmhm2  15945  frgpup3lem  16364  gsumzmhm  16521  gsumzmhmOLD  16522  gsummhm2  16525  gsummhm2OLD  16526  gsummptmhm  16527  mhmvlin  18392  mdetleib2  18496  mdetf  18503  mdetdiaglem  18506  mdetrlin  18510  mdetrsca  18511  mdetralt  18516  mdetunilem7  18526  mdetunilem8  18527  dchrelbas2  22678  dchrn0  22691  mhmhmeotmd  26477