Theorem mhmf 18723

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

Hypotheses

Ref	Expression
mhmf.b	⊢ 𝐵 = (Base‘𝑆)
mhmf.c	⊢ 𝐶 = (Base‘𝑇)

Assertion

Ref	Expression
mhmf	⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝐹:𝐵⟶𝐶)

Proof of Theorem mhmf

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mhmf.b	. . . 4 ⊢ 𝐵 = (Base‘𝑆)
2		mhmf.c	. . . 4 ⊢ 𝐶 = (Base‘𝑇)
3		eqid 2730	. . . 4 ⊢ (+g‘𝑆) = (+g‘𝑆)
4		eqid 2730	. . . 4 ⊢ (+g‘𝑇) = (+g‘𝑇)
5		eqid 2730	. . . 4 ⊢ (0g‘𝑆) = (0g‘𝑆)
6		eqid 2730	. . . 4 ⊢ (0g‘𝑇) = (0g‘𝑇)
7	1, 2, 3, 4, 5, 6	ismhm 18719	. . 3 ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) ∧ (𝐹:𝐵⟶𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦)) ∧ (𝐹‘(0g‘𝑆)) = (0g‘𝑇))))
8	7	simprbi 496	. 2 ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → (𝐹:𝐵⟶𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦)) ∧ (𝐹‘(0g‘𝑆)) = (0g‘𝑇)))
9	8	simp1d 1142	1 ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝐹:𝐵⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ∀wral 3045  ⟶wf 6510  ‘cfv 6514  (class class class)co 7390  Basecbs 17186  +_gcplusg 17227  0_gc0g 17409  Mndcmnd 18668   MndHom cmhm 18715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-fv 6522  df-ov 7393  df-oprab 7394  df-mpo 7395  df-map 8804  df-mhm 18717

This theorem is referenced by:  mhmf1o  18730  mhmvlin  18735  resmhm  18754  resmhm2  18755  resmhm2b  18756  mhmco  18757  mhmimalem  18758  mhmima  18759  mhmeql  18760  pwsco2mhm  18767  gsumwmhm  18779  frmdup3lem  18800  frmdup3  18801  mhmmulg  19054  ghmmhmb  19166  cntzmhm  19280  cntzmhm2  19281  frgpup3lem  19714  gsumzmhm  19874  gsummhm2  19876  gsummptmhm  19877  rhmimasubrnglem  20481  mhmcompl  22274  mdetleib2  22482  mdetf  22489  mdetdiaglem  22492  mdetrlin  22496  mdetrsca  22497  mdetralt  22502  mdetunilem7  22512  mdetunilem8  22513  dchrelbas2  27155  dchrn0  27168  mhmhmeotmd  33924  mhmcopsr  42544