Metamath Proof Explorer

Theorem idmhm

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

Ref Expression
Hypothesis idmhm.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
Assertion idmhm ( 𝑀 ∈ Mnd → ( I ↾ 𝐵 ) ∈ ( 𝑀 MndHom 𝑀 ) )

Proof

Step Hyp Ref Expression
1 idmhm.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 id ⊢ ( 𝑀 ∈ Mnd → 𝑀 ∈ Mnd )
3 f1oi ⊢ ( I ↾ 𝐵 ) : 𝐵 –1-1-onto→ 𝐵
4 f1of ⊢ ( ( I ↾ 𝐵 ) : 𝐵 –1-1-onto→ 𝐵 → ( I ↾ 𝐵 ) : 𝐵 ⟶ 𝐵 )
5 3 4 mp1i ⊢ ( 𝑀 ∈ Mnd → ( I ↾ 𝐵 ) : 𝐵 ⟶ 𝐵 )
6 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
7 1 6 mndcl ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 )
8 7 3expb ⊢ ( ( 𝑀 ∈ Mnd ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 )
9 fvresi ⊢ ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 → ( ( I ↾ 𝐵 ) ‘ ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ) = ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) )
10 8 9 syl ⊢ ( ( 𝑀 ∈ Mnd ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( I ↾ 𝐵 ) ‘ ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ) = ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) )
11 fvresi ⊢ ( 𝑎 ∈ 𝐵 → ( ( I ↾ 𝐵 ) ‘ 𝑎 ) = 𝑎 )
12 fvresi ⊢ ( 𝑏 ∈ 𝐵 → ( ( I ↾ 𝐵 ) ‘ 𝑏 ) = 𝑏 )
13 11 12 oveqan12d ⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( ( ( I ↾ 𝐵 ) ‘ 𝑎 ) ( +g ‘ 𝑀 ) ( ( I ↾ 𝐵 ) ‘ 𝑏 ) ) = ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) )
14 13 adantl ⊢ ( ( 𝑀 ∈ Mnd ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( ( I ↾ 𝐵 ) ‘ 𝑎 ) ( +g ‘ 𝑀 ) ( ( I ↾ 𝐵 ) ‘ 𝑏 ) ) = ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) )
15 10 14 eqtr4d ⊢ ( ( 𝑀 ∈ Mnd ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( I ↾ 𝐵 ) ‘ ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ) = ( ( ( I ↾ 𝐵 ) ‘ 𝑎 ) ( +g ‘ 𝑀 ) ( ( I ↾ 𝐵 ) ‘ 𝑏 ) ) )
16 15 ralrimivva ⊢ ( 𝑀 ∈ Mnd → ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( I ↾ 𝐵 ) ‘ ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ) = ( ( ( I ↾ 𝐵 ) ‘ 𝑎 ) ( +g ‘ 𝑀 ) ( ( I ↾ 𝐵 ) ‘ 𝑏 ) ) )
17 eqid ⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
18 1 17 mndidcl ⊢ ( 𝑀 ∈ Mnd → ( 0g ‘ 𝑀 ) ∈ 𝐵 )
19 fvresi ⊢ ( ( 0g ‘ 𝑀 ) ∈ 𝐵 → ( ( I ↾ 𝐵 ) ‘ ( 0g ‘ 𝑀 ) ) = ( 0g ‘ 𝑀 ) )
20 18 19 syl ⊢ ( 𝑀 ∈ Mnd → ( ( I ↾ 𝐵 ) ‘ ( 0g ‘ 𝑀 ) ) = ( 0g ‘ 𝑀 ) )
21 5 16 20 3jca ⊢ ( 𝑀 ∈ Mnd → ( ( I ↾ 𝐵 ) : 𝐵 ⟶ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( I ↾ 𝐵 ) ‘ ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ) = ( ( ( I ↾ 𝐵 ) ‘ 𝑎 ) ( +g ‘ 𝑀 ) ( ( I ↾ 𝐵 ) ‘ 𝑏 ) ) ∧ ( ( I ↾ 𝐵 ) ‘ ( 0g ‘ 𝑀 ) ) = ( 0g ‘ 𝑀 ) ) )
22 1 1 6 6 17 17 ismhm ⊢ ( ( I ↾ 𝐵 ) ∈ ( 𝑀 MndHom 𝑀 ) ↔ ( ( 𝑀 ∈ Mnd ∧ 𝑀 ∈ Mnd ) ∧ ( ( I ↾ 𝐵 ) : 𝐵 ⟶ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( I ↾ 𝐵 ) ‘ ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ) = ( ( ( I ↾ 𝐵 ) ‘ 𝑎 ) ( +g ‘ 𝑀 ) ( ( I ↾ 𝐵 ) ‘ 𝑏 ) ) ∧ ( ( I ↾ 𝐵 ) ‘ ( 0g ‘ 𝑀 ) ) = ( 0g ‘ 𝑀 ) ) ) )
23 2 2 21 22 syl21anbrc ⊢ ( 𝑀 ∈ Mnd → ( I ↾ 𝐵 ) ∈ ( 𝑀 MndHom 𝑀 ) )