Metamath Proof Explorer

Theorem idmhm

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

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

Proof

Step Hyp Ref Expression
1 idmhm.b ⊢ B = Base M
2 id ⊢ M ∈ Mnd → M ∈ Mnd
3 f1oi ⊢ I ↾ B : B ⟶ 1-1 onto B
4 f1of ⊢ I ↾ B : B ⟶ 1-1 onto B → 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 + M b ∈ B
8 7 3expb ⊢ M ∈ Mnd ∧ a ∈ B ∧ b ∈ B → a + M b ∈ B
9 fvresi ⊢ a + M b ∈ B → I ↾ B ⁡ a + M b = a + M b
10 8 9 syl ⊢ M ∈ Mnd ∧ a ∈ B ∧ b ∈ B → I ↾ B ⁡ a + M b = a + M b
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 + M I ↾ B ⁡ b = a + M b
14 13 adantl ⊢ M ∈ Mnd ∧ a ∈ B ∧ b ∈ B → I ↾ B ⁡ a + M I ↾ B ⁡ b = a + M b
15 10 14 eqtr4d ⊢ M ∈ Mnd ∧ a ∈ B ∧ b ∈ B → I ↾ B ⁡ a + M b = I ↾ B ⁡ a + M I ↾ B ⁡ b
16 15 ralrimivva ⊢ M ∈ Mnd → ∀ a ∈ B ∀ b ∈ B I ↾ B ⁡ a + M b = I ↾ B ⁡ a + M I ↾ B ⁡ b
17 eqid ⊢ 0 M = 0 M
18 1 17 mndidcl ⊢ M ∈ Mnd → 0 M ∈ B
19 fvresi ⊢ 0 M ∈ B → I ↾ B ⁡ 0 M = 0 M
20 18 19 syl ⊢ M ∈ Mnd → I ↾ B ⁡ 0 M = 0 M
21 5 16 20 3jca ⊢ M ∈ Mnd → I ↾ B : B ⟶ B ∧ ∀ a ∈ B ∀ b ∈ B I ↾ B ⁡ a + M b = I ↾ B ⁡ a + M I ↾ B ⁡ b ∧ I ↾ B ⁡ 0 M = 0 M
22 1 1 6 6 17 17 ismhm ⊢ I ↾ B ∈ M MndHom M ↔ M ∈ Mnd ∧ M ∈ Mnd ∧ I ↾ B : B ⟶ B ∧ ∀ a ∈ B ∀ b ∈ B I ↾ B ⁡ a + M b = I ↾ B ⁡ a + M I ↾ B ⁡ b ∧ I ↾ B ⁡ 0 M = 0 M
23 2 2 21 22 syl21anbrc ⊢ M ∈ Mnd → I ↾ B ∈ M MndHom M