# Metamath Proof Explorer

## Theorem c0snmgmhm

Description: The constant mapping to zero is a magma homomorphism from a magma with one element to any monoid. (Contributed by AV, 17-Apr-2020)

Ref Expression
Hypotheses zrrhm.b ${⊢}{B}={\mathrm{Base}}_{{T}}$
zrrhm.0
zrrhm.h
Assertion c0snmgmhm ${⊢}\left({S}\in \mathrm{Mnd}\wedge {T}\in \mathrm{Mgm}\wedge \left|{B}\right|=1\right)\to {H}\in \left({T}\mathrm{MgmHom}{S}\right)$

### Proof

Step Hyp Ref Expression
1 zrrhm.b ${⊢}{B}={\mathrm{Base}}_{{T}}$
2 zrrhm.0
3 zrrhm.h
4 mndmgm ${⊢}{S}\in \mathrm{Mnd}\to {S}\in \mathrm{Mgm}$
5 4 anim1i ${⊢}\left({S}\in \mathrm{Mnd}\wedge {T}\in \mathrm{Mgm}\right)\to \left({S}\in \mathrm{Mgm}\wedge {T}\in \mathrm{Mgm}\right)$
6 5 3adant3 ${⊢}\left({S}\in \mathrm{Mnd}\wedge {T}\in \mathrm{Mgm}\wedge \left|{B}\right|=1\right)\to \left({S}\in \mathrm{Mgm}\wedge {T}\in \mathrm{Mgm}\right)$
7 6 ancomd ${⊢}\left({S}\in \mathrm{Mnd}\wedge {T}\in \mathrm{Mgm}\wedge \left|{B}\right|=1\right)\to \left({T}\in \mathrm{Mgm}\wedge {S}\in \mathrm{Mgm}\right)$
8 1 fvexi ${⊢}{B}\in \mathrm{V}$
9 hash1snb ${⊢}{B}\in \mathrm{V}\to \left(\left|{B}\right|=1↔\exists {b}\phantom{\rule{.4em}{0ex}}{B}=\left\{{b}\right\}\right)$
10 8 9 ax-mp ${⊢}\left|{B}\right|=1↔\exists {b}\phantom{\rule{.4em}{0ex}}{B}=\left\{{b}\right\}$
11 eqid ${⊢}{\mathrm{Base}}_{{S}}={\mathrm{Base}}_{{S}}$
12 11 2 mndidcl
16 15 3 fmptd ${⊢}\left(\left({S}\in \mathrm{Mnd}\wedge {T}\in \mathrm{Mgm}\right)\wedge {B}=\left\{{b}\right\}\right)\to {H}:{B}⟶{\mathrm{Base}}_{{S}}$
17 3 a1i
18 eqidd
19 vsnid ${⊢}{b}\in \left\{{b}\right\}$
20 19 a1i ${⊢}{B}=\left\{{b}\right\}\to {b}\in \left\{{b}\right\}$
21 eleq2 ${⊢}{B}=\left\{{b}\right\}\to \left({b}\in {B}↔{b}\in \left\{{b}\right\}\right)$
22 20 21 mpbird ${⊢}{B}=\left\{{b}\right\}\to {b}\in {B}$
23 22 adantl ${⊢}\left(\left({S}\in \mathrm{Mnd}\wedge {T}\in \mathrm{Mgm}\right)\wedge {B}=\left\{{b}\right\}\right)\to {b}\in {B}$
24 17 18 23 14 fvmptd
25 simpr
26 25 25 oveq12d
27 eqid ${⊢}{+}_{{S}}={+}_{{S}}$
28 11 27 2 mndlid
29 12 28 mpdan
33 simpr ${⊢}\left({S}\in \mathrm{Mnd}\wedge {T}\in \mathrm{Mgm}\right)\to {T}\in \mathrm{Mgm}$
34 33 adantr ${⊢}\left(\left({S}\in \mathrm{Mnd}\wedge {T}\in \mathrm{Mgm}\right)\wedge {B}=\left\{{b}\right\}\right)\to {T}\in \mathrm{Mgm}$
35 34 adantr ${⊢}\left(\left(\left({S}\in \mathrm{Mnd}\wedge {T}\in \mathrm{Mgm}\right)\wedge {B}=\left\{{b}\right\}\right)\wedge {b}\in {B}\right)\to {T}\in \mathrm{Mgm}$
36 simpr ${⊢}\left(\left(\left({S}\in \mathrm{Mnd}\wedge {T}\in \mathrm{Mgm}\right)\wedge {B}=\left\{{b}\right\}\right)\wedge {b}\in {B}\right)\to {b}\in {B}$
37 eqid ${⊢}{+}_{{T}}={+}_{{T}}$
38 1 37 mgmcl ${⊢}\left({T}\in \mathrm{Mgm}\wedge {b}\in {B}\wedge {b}\in {B}\right)\to {b}{+}_{{T}}{b}\in {B}$
39 35 36 36 38 syl3anc ${⊢}\left(\left(\left({S}\in \mathrm{Mnd}\wedge {T}\in \mathrm{Mgm}\right)\wedge {B}=\left\{{b}\right\}\right)\wedge {b}\in {B}\right)\to {b}{+}_{{T}}{b}\in {B}$
40 eleq2 ${⊢}{B}=\left\{{b}\right\}\to \left({b}{+}_{{T}}{b}\in {B}↔{b}{+}_{{T}}{b}\in \left\{{b}\right\}\right)$
41 elsni ${⊢}{b}{+}_{{T}}{b}\in \left\{{b}\right\}\to {b}{+}_{{T}}{b}={b}$
42 40 41 syl6bi ${⊢}{B}=\left\{{b}\right\}\to \left({b}{+}_{{T}}{b}\in {B}\to {b}{+}_{{T}}{b}={b}\right)$
43 42 adantl ${⊢}\left(\left({S}\in \mathrm{Mnd}\wedge {T}\in \mathrm{Mgm}\right)\wedge {B}=\left\{{b}\right\}\right)\to \left({b}{+}_{{T}}{b}\in {B}\to {b}{+}_{{T}}{b}={b}\right)$
44 43 adantr ${⊢}\left(\left(\left({S}\in \mathrm{Mnd}\wedge {T}\in \mathrm{Mgm}\right)\wedge {B}=\left\{{b}\right\}\right)\wedge {b}\in {B}\right)\to \left({b}{+}_{{T}}{b}\in {B}\to {b}{+}_{{T}}{b}={b}\right)$
45 39 44 mpd ${⊢}\left(\left(\left({S}\in \mathrm{Mnd}\wedge {T}\in \mathrm{Mgm}\right)\wedge {B}=\left\{{b}\right\}\right)\wedge {b}\in {B}\right)\to {b}{+}_{{T}}{b}={b}$
46 23 45 mpdan ${⊢}\left(\left({S}\in \mathrm{Mnd}\wedge {T}\in \mathrm{Mgm}\right)\wedge {B}=\left\{{b}\right\}\right)\to {b}{+}_{{T}}{b}={b}$
47 46 fveq2d ${⊢}\left(\left({S}\in \mathrm{Mnd}\wedge {T}\in \mathrm{Mgm}\right)\wedge {B}=\left\{{b}\right\}\right)\to {H}\left({b}{+}_{{T}}{b}\right)={H}\left({b}\right)$
49 48 25 eqtr2d
50 26 32 49 3eqtrrd
51 24 50 mpdan ${⊢}\left(\left({S}\in \mathrm{Mnd}\wedge {T}\in \mathrm{Mgm}\right)\wedge {B}=\left\{{b}\right\}\right)\to {H}\left({b}{+}_{{T}}{b}\right)={H}\left({b}\right){+}_{{S}}{H}\left({b}\right)$
52 id ${⊢}{B}=\left\{{b}\right\}\to {B}=\left\{{b}\right\}$
53 52 raleqdv ${⊢}{B}=\left\{{b}\right\}\to \left(\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}{H}\left({a}{+}_{{T}}{c}\right)={H}\left({a}\right){+}_{{S}}{H}\left({c}\right)↔\forall {c}\in \left\{{b}\right\}\phantom{\rule{.4em}{0ex}}{H}\left({a}{+}_{{T}}{c}\right)={H}\left({a}\right){+}_{{S}}{H}\left({c}\right)\right)$
54 52 53 raleqbidv ${⊢}{B}=\left\{{b}\right\}\to \left(\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}{H}\left({a}{+}_{{T}}{c}\right)={H}\left({a}\right){+}_{{S}}{H}\left({c}\right)↔\forall {a}\in \left\{{b}\right\}\phantom{\rule{.4em}{0ex}}\forall {c}\in \left\{{b}\right\}\phantom{\rule{.4em}{0ex}}{H}\left({a}{+}_{{T}}{c}\right)={H}\left({a}\right){+}_{{S}}{H}\left({c}\right)\right)$
55 54 adantl ${⊢}\left(\left({S}\in \mathrm{Mnd}\wedge {T}\in \mathrm{Mgm}\right)\wedge {B}=\left\{{b}\right\}\right)\to \left(\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}{H}\left({a}{+}_{{T}}{c}\right)={H}\left({a}\right){+}_{{S}}{H}\left({c}\right)↔\forall {a}\in \left\{{b}\right\}\phantom{\rule{.4em}{0ex}}\forall {c}\in \left\{{b}\right\}\phantom{\rule{.4em}{0ex}}{H}\left({a}{+}_{{T}}{c}\right)={H}\left({a}\right){+}_{{S}}{H}\left({c}\right)\right)$
56 fvoveq1 ${⊢}{a}={b}\to {H}\left({a}{+}_{{T}}{c}\right)={H}\left({b}{+}_{{T}}{c}\right)$
57 fveq2 ${⊢}{a}={b}\to {H}\left({a}\right)={H}\left({b}\right)$
58 57 oveq1d ${⊢}{a}={b}\to {H}\left({a}\right){+}_{{S}}{H}\left({c}\right)={H}\left({b}\right){+}_{{S}}{H}\left({c}\right)$
59 56 58 eqeq12d ${⊢}{a}={b}\to \left({H}\left({a}{+}_{{T}}{c}\right)={H}\left({a}\right){+}_{{S}}{H}\left({c}\right)↔{H}\left({b}{+}_{{T}}{c}\right)={H}\left({b}\right){+}_{{S}}{H}\left({c}\right)\right)$
60 oveq2 ${⊢}{c}={b}\to {b}{+}_{{T}}{c}={b}{+}_{{T}}{b}$
61 60 fveq2d ${⊢}{c}={b}\to {H}\left({b}{+}_{{T}}{c}\right)={H}\left({b}{+}_{{T}}{b}\right)$
62 fveq2 ${⊢}{c}={b}\to {H}\left({c}\right)={H}\left({b}\right)$
63 62 oveq2d ${⊢}{c}={b}\to {H}\left({b}\right){+}_{{S}}{H}\left({c}\right)={H}\left({b}\right){+}_{{S}}{H}\left({b}\right)$
64 61 63 eqeq12d ${⊢}{c}={b}\to \left({H}\left({b}{+}_{{T}}{c}\right)={H}\left({b}\right){+}_{{S}}{H}\left({c}\right)↔{H}\left({b}{+}_{{T}}{b}\right)={H}\left({b}\right){+}_{{S}}{H}\left({b}\right)\right)$
65 59 64 2ralsng ${⊢}\left({b}\in \mathrm{V}\wedge {b}\in \mathrm{V}\right)\to \left(\forall {a}\in \left\{{b}\right\}\phantom{\rule{.4em}{0ex}}\forall {c}\in \left\{{b}\right\}\phantom{\rule{.4em}{0ex}}{H}\left({a}{+}_{{T}}{c}\right)={H}\left({a}\right){+}_{{S}}{H}\left({c}\right)↔{H}\left({b}{+}_{{T}}{b}\right)={H}\left({b}\right){+}_{{S}}{H}\left({b}\right)\right)$
66 65 el2v ${⊢}\forall {a}\in \left\{{b}\right\}\phantom{\rule{.4em}{0ex}}\forall {c}\in \left\{{b}\right\}\phantom{\rule{.4em}{0ex}}{H}\left({a}{+}_{{T}}{c}\right)={H}\left({a}\right){+}_{{S}}{H}\left({c}\right)↔{H}\left({b}{+}_{{T}}{b}\right)={H}\left({b}\right){+}_{{S}}{H}\left({b}\right)$
67 55 66 syl6bb ${⊢}\left(\left({S}\in \mathrm{Mnd}\wedge {T}\in \mathrm{Mgm}\right)\wedge {B}=\left\{{b}\right\}\right)\to \left(\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}{H}\left({a}{+}_{{T}}{c}\right)={H}\left({a}\right){+}_{{S}}{H}\left({c}\right)↔{H}\left({b}{+}_{{T}}{b}\right)={H}\left({b}\right){+}_{{S}}{H}\left({b}\right)\right)$
68 51 67 mpbird ${⊢}\left(\left({S}\in \mathrm{Mnd}\wedge {T}\in \mathrm{Mgm}\right)\wedge {B}=\left\{{b}\right\}\right)\to \forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}{H}\left({a}{+}_{{T}}{c}\right)={H}\left({a}\right){+}_{{S}}{H}\left({c}\right)$
69 16 68 jca ${⊢}\left(\left({S}\in \mathrm{Mnd}\wedge {T}\in \mathrm{Mgm}\right)\wedge {B}=\left\{{b}\right\}\right)\to \left({H}:{B}⟶{\mathrm{Base}}_{{S}}\wedge \forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}{H}\left({a}{+}_{{T}}{c}\right)={H}\left({a}\right){+}_{{S}}{H}\left({c}\right)\right)$
70 69 ex ${⊢}\left({S}\in \mathrm{Mnd}\wedge {T}\in \mathrm{Mgm}\right)\to \left({B}=\left\{{b}\right\}\to \left({H}:{B}⟶{\mathrm{Base}}_{{S}}\wedge \forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}{H}\left({a}{+}_{{T}}{c}\right)={H}\left({a}\right){+}_{{S}}{H}\left({c}\right)\right)\right)$
71 70 exlimdv ${⊢}\left({S}\in \mathrm{Mnd}\wedge {T}\in \mathrm{Mgm}\right)\to \left(\exists {b}\phantom{\rule{.4em}{0ex}}{B}=\left\{{b}\right\}\to \left({H}:{B}⟶{\mathrm{Base}}_{{S}}\wedge \forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}{H}\left({a}{+}_{{T}}{c}\right)={H}\left({a}\right){+}_{{S}}{H}\left({c}\right)\right)\right)$
72 10 71 syl5bi ${⊢}\left({S}\in \mathrm{Mnd}\wedge {T}\in \mathrm{Mgm}\right)\to \left(\left|{B}\right|=1\to \left({H}:{B}⟶{\mathrm{Base}}_{{S}}\wedge \forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}{H}\left({a}{+}_{{T}}{c}\right)={H}\left({a}\right){+}_{{S}}{H}\left({c}\right)\right)\right)$
73 72 3impia ${⊢}\left({S}\in \mathrm{Mnd}\wedge {T}\in \mathrm{Mgm}\wedge \left|{B}\right|=1\right)\to \left({H}:{B}⟶{\mathrm{Base}}_{{S}}\wedge \forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}{H}\left({a}{+}_{{T}}{c}\right)={H}\left({a}\right){+}_{{S}}{H}\left({c}\right)\right)$
74 1 11 37 27 ismgmhm ${⊢}{H}\in \left({T}\mathrm{MgmHom}{S}\right)↔\left(\left({T}\in \mathrm{Mgm}\wedge {S}\in \mathrm{Mgm}\right)\wedge \left({H}:{B}⟶{\mathrm{Base}}_{{S}}\wedge \forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}{H}\left({a}{+}_{{T}}{c}\right)={H}\left({a}\right){+}_{{S}}{H}\left({c}\right)\right)\right)$
75 7 73 74 sylanbrc ${⊢}\left({S}\in \mathrm{Mnd}\wedge {T}\in \mathrm{Mgm}\wedge \left|{B}\right|=1\right)\to {H}\in \left({T}\mathrm{MgmHom}{S}\right)$