Metamath Proof Explorer

Theorem idmgmhm

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

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

Proof

Step Hyp Ref Expression
1 idmgmhm.b ⊢ B = Base M
2 id ⊢ M ∈ Mgm → M ∈ Mgm
3 2 ancri ⊢ M ∈ Mgm → M ∈ Mgm ∧ M ∈ Mgm
4 f1oi ⊢ I ↾ B : B ⟶ 1-1 onto B
5 f1of ⊢ I ↾ B : B ⟶ 1-1 onto B → 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 + M b ∈ B
9 8 3expb ⊢ M ∈ Mgm ∧ a ∈ B ∧ b ∈ B → a + M b ∈ B
10 fvresi ⊢ a + M b ∈ B → I ↾ B ⁡ a + M b = a + M b
11 9 10 syl ⊢ M ∈ Mgm ∧ a ∈ B ∧ b ∈ B → I ↾ B ⁡ a + M b = a + M b
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 + M I ↾ B ⁡ b = a + M b
15 14 adantl ⊢ M ∈ Mgm ∧ a ∈ B ∧ b ∈ B → I ↾ B ⁡ a + M I ↾ B ⁡ b = a + M b
16 11 15 eqtr4d ⊢ M ∈ Mgm ∧ a ∈ B ∧ b ∈ B → I ↾ B ⁡ a + M b = I ↾ B ⁡ a + M I ↾ B ⁡ b
17 16 ralrimivva ⊢ M ∈ Mgm → ∀ a ∈ B ∀ b ∈ B I ↾ B ⁡ a + M b = I ↾ B ⁡ a + M I ↾ B ⁡ b
18 6 17 jca ⊢ M ∈ Mgm → I ↾ B : B ⟶ B ∧ ∀ a ∈ B ∀ b ∈ B I ↾ B ⁡ a + M b = I ↾ B ⁡ a + M I ↾ B ⁡ b
19 1 1 7 7 ismgmhm ⊢ I ↾ B ∈ M MgmHom M ↔ M ∈ Mgm ∧ M ∈ Mgm ∧ I ↾ B : B ⟶ B ∧ ∀ a ∈ B ∀ b ∈ B I ↾ B ⁡ a + M b = I ↾ B ⁡ a + M I ↾ B ⁡ b
20 3 18 19 sylanbrc ⊢ M ∈ Mgm → I ↾ B ∈ M MgmHom M