![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mhmf | Structured version Visualization 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 2462 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | eqid 2462 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | eqid 2462 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | eqid 2462 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 1, 2, 3, 4, 5, 6 | ismhm 16633 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 7 | simprbi 470 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 8 | simp1d 1026 |
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 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-8 1900 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-sep 4539 ax-nul 4548 ax-pow 4595 ax-pr 4653 ax-un 6610 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-ral 2754 df-rex 2755 df-rab 2758 df-v 3059 df-sbc 3280 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-nul 3744 df-if 3894 df-pw 3965 df-sn 3981 df-pr 3983 df-op 3987 df-uni 4213 df-br 4417 df-opab 4476 df-id 4768 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-fv 5609 df-ov 6318 df-oprab 6319 df-mpt2 6320 df-map 7500 df-mhm 16631 |
This theorem is referenced by: mhmf1o 16641 resmhm 16655 resmhm2 16656 resmhm2b 16657 mhmco 16658 mhmima 16659 mhmeql 16660 pwsco2mhm 16667 gsumwmhm 16678 frmdup3lem 16699 frmdup3 16700 mhmmulg 16839 ghmmhmb 16943 cntzmhm 17041 cntzmhm2 17042 frgpup3lem 17476 gsumzmhm 17619 gsummhm2 17621 gsummptmhm 17622 mhmvlin 19471 mdetleib2 19662 mdetf 19669 mdetdiaglem 19672 mdetrlin 19676 mdetrsca 19677 mdetralt 19682 mdetunilem7 19692 mdetunilem8 19693 dchrelbas2 24214 dchrn0 24227 mhmhmeotmd 28782 |
Copyright terms: Public domain | W3C validator |