# Metamath Proof Explorer

## Theorem idmgmhm

Description: The identity homomorphism on a magma. (Contributed by AV, 27-Feb-2020)

Ref Expression
Hypothesis idmgmhm.b ${⊢}{B}={\mathrm{Base}}_{{M}}$
Assertion idmgmhm ${⊢}{M}\in \mathrm{Mgm}\to {\mathrm{I}↾}_{{B}}\in \left({M}\mathrm{MgmHom}{M}\right)$

### Proof

Step Hyp Ref Expression
1 idmgmhm.b ${⊢}{B}={\mathrm{Base}}_{{M}}$
2 id ${⊢}{M}\in \mathrm{Mgm}\to {M}\in \mathrm{Mgm}$
3 2 ancri ${⊢}{M}\in \mathrm{Mgm}\to \left({M}\in \mathrm{Mgm}\wedge {M}\in \mathrm{Mgm}\right)$
4 f1oi ${⊢}\left({\mathrm{I}↾}_{{B}}\right):{B}\underset{1-1 onto}{⟶}{B}$
5 f1of ${⊢}\left({\mathrm{I}↾}_{{B}}\right):{B}\underset{1-1 onto}{⟶}{B}\to \left({\mathrm{I}↾}_{{B}}\right):{B}⟶{B}$
6 4 5 mp1i ${⊢}{M}\in \mathrm{Mgm}\to \left({\mathrm{I}↾}_{{B}}\right):{B}⟶{B}$
7 eqid ${⊢}{+}_{{M}}={+}_{{M}}$
8 1 7 mgmcl ${⊢}\left({M}\in \mathrm{Mgm}\wedge {a}\in {B}\wedge {b}\in {B}\right)\to {a}{+}_{{M}}{b}\in {B}$
9 8 3expb ${⊢}\left({M}\in \mathrm{Mgm}\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to {a}{+}_{{M}}{b}\in {B}$
10 fvresi ${⊢}{a}{+}_{{M}}{b}\in {B}\to \left({\mathrm{I}↾}_{{B}}\right)\left({a}{+}_{{M}}{b}\right)={a}{+}_{{M}}{b}$
11 9 10 syl ${⊢}\left({M}\in \mathrm{Mgm}\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to \left({\mathrm{I}↾}_{{B}}\right)\left({a}{+}_{{M}}{b}\right)={a}{+}_{{M}}{b}$
12 fvresi ${⊢}{a}\in {B}\to \left({\mathrm{I}↾}_{{B}}\right)\left({a}\right)={a}$
13 fvresi ${⊢}{b}\in {B}\to \left({\mathrm{I}↾}_{{B}}\right)\left({b}\right)={b}$
14 12 13 oveqan12d ${⊢}\left({a}\in {B}\wedge {b}\in {B}\right)\to \left({\mathrm{I}↾}_{{B}}\right)\left({a}\right){+}_{{M}}\left({\mathrm{I}↾}_{{B}}\right)\left({b}\right)={a}{+}_{{M}}{b}$
15 14 adantl ${⊢}\left({M}\in \mathrm{Mgm}\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to \left({\mathrm{I}↾}_{{B}}\right)\left({a}\right){+}_{{M}}\left({\mathrm{I}↾}_{{B}}\right)\left({b}\right)={a}{+}_{{M}}{b}$
16 11 15 eqtr4d ${⊢}\left({M}\in \mathrm{Mgm}\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to \left({\mathrm{I}↾}_{{B}}\right)\left({a}{+}_{{M}}{b}\right)=\left({\mathrm{I}↾}_{{B}}\right)\left({a}\right){+}_{{M}}\left({\mathrm{I}↾}_{{B}}\right)\left({b}\right)$
17 16 ralrimivva ${⊢}{M}\in \mathrm{Mgm}\to \forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\left({\mathrm{I}↾}_{{B}}\right)\left({a}{+}_{{M}}{b}\right)=\left({\mathrm{I}↾}_{{B}}\right)\left({a}\right){+}_{{M}}\left({\mathrm{I}↾}_{{B}}\right)\left({b}\right)$
18 6 17 jca ${⊢}{M}\in \mathrm{Mgm}\to \left(\left({\mathrm{I}↾}_{{B}}\right):{B}⟶{B}\wedge \forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\left({\mathrm{I}↾}_{{B}}\right)\left({a}{+}_{{M}}{b}\right)=\left({\mathrm{I}↾}_{{B}}\right)\left({a}\right){+}_{{M}}\left({\mathrm{I}↾}_{{B}}\right)\left({b}\right)\right)$
19 1 1 7 7 ismgmhm ${⊢}{\mathrm{I}↾}_{{B}}\in \left({M}\mathrm{MgmHom}{M}\right)↔\left(\left({M}\in \mathrm{Mgm}\wedge {M}\in \mathrm{Mgm}\right)\wedge \left(\left({\mathrm{I}↾}_{{B}}\right):{B}⟶{B}\wedge \forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\left({\mathrm{I}↾}_{{B}}\right)\left({a}{+}_{{M}}{b}\right)=\left({\mathrm{I}↾}_{{B}}\right)\left({a}\right){+}_{{M}}\left({\mathrm{I}↾}_{{B}}\right)\left({b}\right)\right)\right)$
20 3 18 19 sylanbrc ${⊢}{M}\in \mathrm{Mgm}\to {\mathrm{I}↾}_{{B}}\in \left({M}\mathrm{MgmHom}{M}\right)$