![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > mhmf | Structured version Unicode version |
Description: A monoid homomorphism is a function. (Contributed by Mario Carneiro, 7-Mar-2015.) |
Ref | Expression |
---|---|
mhmf.b |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mhmf.c |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mhmf |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mhmf.b |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | mhmf.c |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | eqid 2450 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | eqid 2450 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | eqid 2450 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | eqid 2450 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 1, 2, 3, 4, 5, 6 | ismhm 15554 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 7 | simprbi 464 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 8 | simp1d 1000 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
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 |
Copyright terms: Public domain | W3C validator |