Metamath Proof Explorer

Theorem idmgmhm

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

Ref Expression
Hypothesis idmgmhm.b ⊢B=BaseM
Assertion idmgmhm ⊢M∈Mgm→I↾B∈MMgmHomM

Proof

Step Hyp Ref Expression
1 idmgmhm.b ⊢B=BaseM
2 id ⊢M∈Mgm→M∈Mgm
3 2 ancri ⊢M∈Mgm→M∈Mgm∧M∈Mgm
4 f1oi ⊢I↾B:B⟶1-1 ontoB
5 f1of ⊢I↾B:B⟶1-1 ontoB→I↾B:B⟶B
6 4 5 mp1i ⊢M∈Mgm→I↾B:B⟶B
7 eqid ⊢+M=+M
8 1 7 mgmcl ⊢M∈Mgm∧a∈B∧b∈B→a+Mb∈B
9 8 3expb ⊢M∈Mgm∧a∈B∧b∈B→a+Mb∈B
10 fvresi ⊢a+Mb∈B→I↾B⁡a+Mb=a+Mb
11 9 10 syl ⊢M∈Mgm∧a∈B∧b∈B→I↾B⁡a+Mb=a+Mb
12 fvresi ⊢a∈B→I↾B⁡a=a
13 fvresi ⊢b∈B→I↾B⁡b=b
14 12 13 oveqan12d ⊢a∈B∧b∈B→I↾B⁡a+MI↾B⁡b=a+Mb
15 14 adantl ⊢M∈Mgm∧a∈B∧b∈B→I↾B⁡a+MI↾B⁡b=a+Mb
16 11 15 eqtr4d ⊢M∈Mgm∧a∈B∧b∈B→I↾B⁡a+Mb=I↾B⁡a+MI↾B⁡b
17 16 ralrimivva ⊢M∈Mgm→∀a∈B∀b∈BI↾B⁡a+Mb=I↾B⁡a+MI↾B⁡b
18 6 17 jca ⊢M∈Mgm→I↾B:B⟶B∧∀a∈B∀b∈BI↾B⁡a+Mb=I↾B⁡a+MI↾B⁡b
19 1 1 7 7 ismgmhm ⊢I↾B∈MMgmHomM↔M∈Mgm∧M∈Mgm∧I↾B:B⟶B∧∀a∈B∀b∈BI↾B⁡a+Mb=I↾B⁡a+MI↾B⁡b
20 3 18 19 sylanbrc ⊢M∈Mgm→I↾B∈MMgmHomM