Metamath Proof Explorer

Theorem idmhm

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

Ref Expression
Hypothesis idmhm.b ⊢B=BaseM
Assertion idmhm ⊢M∈Mnd→I↾B∈MMndHomM

Proof

Step Hyp Ref Expression
1 idmhm.b ⊢B=BaseM
2 id ⊢M∈Mnd→M∈Mnd
3 f1oi ⊢I↾B:B⟶1-1 ontoB
4 f1of ⊢I↾B:B⟶1-1 ontoB→I↾B:B⟶B
5 3 4 mp1i ⊢M∈Mnd→I↾B:B⟶B
6 eqid ⊢+M=+M
7 1 6 mndcl ⊢M∈Mnd∧a∈B∧b∈B→a+Mb∈B
8 7 3expb ⊢M∈Mnd∧a∈B∧b∈B→a+Mb∈B
9 fvresi ⊢a+Mb∈B→I↾B⁡a+Mb=a+Mb
10 8 9 syl ⊢M∈Mnd∧a∈B∧b∈B→I↾B⁡a+Mb=a+Mb
11 fvresi ⊢a∈B→I↾B⁡a=a
12 fvresi ⊢b∈B→I↾B⁡b=b
13 11 12 oveqan12d ⊢a∈B∧b∈B→I↾B⁡a+MI↾B⁡b=a+Mb
14 13 adantl ⊢M∈Mnd∧a∈B∧b∈B→I↾B⁡a+MI↾B⁡b=a+Mb
15 10 14 eqtr4d ⊢M∈Mnd∧a∈B∧b∈B→I↾B⁡a+Mb=I↾B⁡a+MI↾B⁡b
16 15 ralrimivva ⊢M∈Mnd→∀a∈B∀b∈BI↾B⁡a+Mb=I↾B⁡a+MI↾B⁡b
17 eqid ⊢0M=0M
18 1 17 mndidcl ⊢M∈Mnd→0M∈B
19 fvresi ⊢0M∈B→I↾B⁡0M=0M
20 18 19 syl ⊢M∈Mnd→I↾B⁡0M=0M
21 5 16 20 3jca ⊢M∈Mnd→I↾B:B⟶B∧∀a∈B∀b∈BI↾B⁡a+Mb=I↾B⁡a+MI↾B⁡b∧I↾B⁡0M=0M
22 1 1 6 6 17 17 ismhm ⊢I↾B∈MMndHomM↔M∈Mnd∧M∈Mnd∧I↾B:B⟶B∧∀a∈B∀b∈BI↾B⁡a+Mb=I↾B⁡a+MI↾B⁡b∧I↾B⁡0M=0M
23 2 2 21 22 syl21anbrc ⊢M∈Mnd→I↾B∈MMndHomM