# Metamath Proof Explorer

## Theorem ismgmhm

Description: Property of a magma homomorphism. (Contributed by AV, 25-Feb-2020)

Ref Expression
Hypotheses ismgmhm.b ${⊢}{B}={\mathrm{Base}}_{{S}}$
ismgmhm.c ${⊢}{C}={\mathrm{Base}}_{{T}}$
ismgmhm.p
ismgmhm.q
Assertion ismgmhm

### Proof

Step Hyp Ref Expression
1 ismgmhm.b ${⊢}{B}={\mathrm{Base}}_{{S}}$
2 ismgmhm.c ${⊢}{C}={\mathrm{Base}}_{{T}}$
3 ismgmhm.p
4 ismgmhm.q
5 mgmhmrcl ${⊢}{F}\in \left({S}\mathrm{MgmHom}{T}\right)\to \left({S}\in \mathrm{Mgm}\wedge {T}\in \mathrm{Mgm}\right)$
6 fveq2 ${⊢}{t}={T}\to {\mathrm{Base}}_{{t}}={\mathrm{Base}}_{{T}}$
7 6 2 syl6eqr ${⊢}{t}={T}\to {\mathrm{Base}}_{{t}}={C}$
8 fveq2 ${⊢}{s}={S}\to {\mathrm{Base}}_{{s}}={\mathrm{Base}}_{{S}}$
9 8 1 syl6eqr ${⊢}{s}={S}\to {\mathrm{Base}}_{{s}}={B}$
10 7 9 oveqan12rd ${⊢}\left({s}={S}\wedge {t}={T}\right)\to {{\mathrm{Base}}_{{t}}}^{{\mathrm{Base}}_{{s}}}={{C}}^{{B}}$
11 9 adantr ${⊢}\left({s}={S}\wedge {t}={T}\right)\to {\mathrm{Base}}_{{s}}={B}$
12 fveq2 ${⊢}{s}={S}\to {+}_{{s}}={+}_{{S}}$
13 12 3 syl6eqr
14 13 oveqd
15 14 fveq2d
16 fveq2 ${⊢}{t}={T}\to {+}_{{t}}={+}_{{T}}$
17 16 4 syl6eqr
18 17 oveqd
19 15 18 eqeqan12d
20 11 19 raleqbidv
21 11 20 raleqbidv
22 10 21 rabeqbidv
23 df-mgmhm ${⊢}\mathrm{MgmHom}=\left({s}\in \mathrm{Mgm},{t}\in \mathrm{Mgm}⟼\left\{{f}\in \left({{\mathrm{Base}}_{{t}}}^{{\mathrm{Base}}_{{s}}}\right)|\forall {x}\in {\mathrm{Base}}_{{s}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{s}}\phantom{\rule{.4em}{0ex}}{f}\left({x}{+}_{{s}}{y}\right)={f}\left({x}\right){+}_{{t}}{f}\left({y}\right)\right\}\right)$
24 ovex ${⊢}{{C}}^{{B}}\in \mathrm{V}$
25 24 rabex
26 22 23 25 ovmpoa
27 26 eleq2d
28 fveq1
29 fveq1 ${⊢}{f}={F}\to {f}\left({x}\right)={F}\left({x}\right)$
30 fveq1 ${⊢}{f}={F}\to {f}\left({y}\right)={F}\left({y}\right)$
31 29 30 oveq12d
32 28 31 eqeq12d
33 32 2ralbidv
34 33 elrab
35 2 fvexi ${⊢}{C}\in \mathrm{V}$
36 1 fvexi ${⊢}{B}\in \mathrm{V}$
37 35 36 elmap ${⊢}{F}\in \left({{C}}^{{B}}\right)↔{F}:{B}⟶{C}$
38 37 anbi1i
39 34 38 bitri
40 27 39 syl6bb