# Metamath Proof Explorer

## Theorem idmgmhm

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

Ref Expression
Hypothesis idmgmhm.b 𝐵 = ( Base ‘ 𝑀 )
Assertion idmgmhm ( 𝑀 ∈ Mgm → ( I ↾ 𝐵 ) ∈ ( 𝑀 MgmHom 𝑀 ) )

### Proof

Step Hyp Ref Expression
1 idmgmhm.b 𝐵 = ( Base ‘ 𝑀 )
2 id ( 𝑀 ∈ Mgm → 𝑀 ∈ Mgm )
3 2 ancri ( 𝑀 ∈ Mgm → ( 𝑀 ∈ Mgm ∧ 𝑀 ∈ Mgm ) )
4 f1oi ( I ↾ 𝐵 ) : 𝐵1-1-onto𝐵
5 f1of ( ( I ↾ 𝐵 ) : 𝐵1-1-onto𝐵 → ( I ↾ 𝐵 ) : 𝐵𝐵 )
6 4 5 mp1i ( 𝑀 ∈ Mgm → ( I ↾ 𝐵 ) : 𝐵𝐵 )
7 eqid ( +g𝑀 ) = ( +g𝑀 )
8 1 7 mgmcl ( ( 𝑀 ∈ Mgm ∧ 𝑎𝐵𝑏𝐵 ) → ( 𝑎 ( +g𝑀 ) 𝑏 ) ∈ 𝐵 )
9 8 3expb ( ( 𝑀 ∈ Mgm ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( 𝑎 ( +g𝑀 ) 𝑏 ) ∈ 𝐵 )
10 fvresi ( ( 𝑎 ( +g𝑀 ) 𝑏 ) ∈ 𝐵 → ( ( I ↾ 𝐵 ) ‘ ( 𝑎 ( +g𝑀 ) 𝑏 ) ) = ( 𝑎 ( +g𝑀 ) 𝑏 ) )
11 9 10 syl ( ( 𝑀 ∈ Mgm ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( ( I ↾ 𝐵 ) ‘ ( 𝑎 ( +g𝑀 ) 𝑏 ) ) = ( 𝑎 ( +g𝑀 ) 𝑏 ) )
12 fvresi ( 𝑎𝐵 → ( ( I ↾ 𝐵 ) ‘ 𝑎 ) = 𝑎 )
13 fvresi ( 𝑏𝐵 → ( ( I ↾ 𝐵 ) ‘ 𝑏 ) = 𝑏 )
14 12 13 oveqan12d ( ( 𝑎𝐵𝑏𝐵 ) → ( ( ( I ↾ 𝐵 ) ‘ 𝑎 ) ( +g𝑀 ) ( ( I ↾ 𝐵 ) ‘ 𝑏 ) ) = ( 𝑎 ( +g𝑀 ) 𝑏 ) )
15 14 adantl ( ( 𝑀 ∈ Mgm ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( ( ( I ↾ 𝐵 ) ‘ 𝑎 ) ( +g𝑀 ) ( ( I ↾ 𝐵 ) ‘ 𝑏 ) ) = ( 𝑎 ( +g𝑀 ) 𝑏 ) )
16 11 15 eqtr4d ( ( 𝑀 ∈ Mgm ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( ( I ↾ 𝐵 ) ‘ ( 𝑎 ( +g𝑀 ) 𝑏 ) ) = ( ( ( I ↾ 𝐵 ) ‘ 𝑎 ) ( +g𝑀 ) ( ( I ↾ 𝐵 ) ‘ 𝑏 ) ) )
17 16 ralrimivva ( 𝑀 ∈ Mgm → ∀ 𝑎𝐵𝑏𝐵 ( ( I ↾ 𝐵 ) ‘ ( 𝑎 ( +g𝑀 ) 𝑏 ) ) = ( ( ( I ↾ 𝐵 ) ‘ 𝑎 ) ( +g𝑀 ) ( ( I ↾ 𝐵 ) ‘ 𝑏 ) ) )
18 6 17 jca ( 𝑀 ∈ Mgm → ( ( I ↾ 𝐵 ) : 𝐵𝐵 ∧ ∀ 𝑎𝐵𝑏𝐵 ( ( I ↾ 𝐵 ) ‘ ( 𝑎 ( +g𝑀 ) 𝑏 ) ) = ( ( ( I ↾ 𝐵 ) ‘ 𝑎 ) ( +g𝑀 ) ( ( I ↾ 𝐵 ) ‘ 𝑏 ) ) ) )
19 1 1 7 7 ismgmhm ( ( I ↾ 𝐵 ) ∈ ( 𝑀 MgmHom 𝑀 ) ↔ ( ( 𝑀 ∈ Mgm ∧ 𝑀 ∈ Mgm ) ∧ ( ( I ↾ 𝐵 ) : 𝐵𝐵 ∧ ∀ 𝑎𝐵𝑏𝐵 ( ( I ↾ 𝐵 ) ‘ ( 𝑎 ( +g𝑀 ) 𝑏 ) ) = ( ( ( I ↾ 𝐵 ) ‘ 𝑎 ) ( +g𝑀 ) ( ( I ↾ 𝐵 ) ‘ 𝑏 ) ) ) ) )
20 3 18 19 sylanbrc ( 𝑀 ∈ Mgm → ( I ↾ 𝐵 ) ∈ ( 𝑀 MgmHom 𝑀 ) )