Metamath Proof Explorer

Theorem idghm

Description: The identity homomorphism on a group. (Contributed by Stefan O'Rear, 31-Dec-2014)

Ref Expression
Hypothesis idghm.b ⊢ B = Base G
Assertion idghm ⊢ G ∈ Grp → I ↾ B ∈ G GrpHom G

Proof

Step Hyp Ref Expression
1 idghm.b ⊢ B = Base G
2 id ⊢ G ∈ Grp → G ∈ Grp
3 eqid ⊢ + G = + G
4 1 3 grpcl ⊢ G ∈ Grp ∧ a ∈ B ∧ b ∈ B → a + G b ∈ B
5 4 3expb ⊢ G ∈ Grp ∧ a ∈ B ∧ b ∈ B → a + G b ∈ B
6 fvresi ⊢ a + G b ∈ B → I ↾ B ⁡ a + G b = a + G b
7 5 6 syl ⊢ G ∈ Grp ∧ a ∈ B ∧ b ∈ B → I ↾ B ⁡ a + G b = a + G b
8 fvresi ⊢ a ∈ B → I ↾ B ⁡ a = a
9 fvresi ⊢ b ∈ B → I ↾ B ⁡ b = b
10 8 9 oveqan12d ⊢ a ∈ B ∧ b ∈ B → I ↾ B ⁡ a + G I ↾ B ⁡ b = a + G b
11 10 adantl ⊢ G ∈ Grp ∧ a ∈ B ∧ b ∈ B → I ↾ B ⁡ a + G I ↾ B ⁡ b = a + G b
12 7 11 eqtr4d ⊢ G ∈ Grp ∧ a ∈ B ∧ b ∈ B → I ↾ B ⁡ a + G b = I ↾ B ⁡ a + G I ↾ B ⁡ b
13 12 ralrimivva ⊢ G ∈ Grp → ∀ a ∈ B ∀ b ∈ B I ↾ B ⁡ a + G b = I ↾ B ⁡ a + G I ↾ B ⁡ b
14 f1oi ⊢ I ↾ B : B ⟶ 1-1 onto B
15 f1of ⊢ I ↾ B : B ⟶ 1-1 onto B → I ↾ B : B ⟶ B
16 14 15 ax-mp ⊢ I ↾ B : B ⟶ B
17 13 16 jctil ⊢ G ∈ Grp → I ↾ B : B ⟶ B ∧ ∀ a ∈ B ∀ b ∈ B I ↾ B ⁡ a + G b = I ↾ B ⁡ a + G I ↾ B ⁡ b
18 1 1 3 3 isghm ⊢ I ↾ B ∈ G GrpHom G ↔ G ∈ Grp ∧ G ∈ Grp ∧ I ↾ B : B ⟶ B ∧ ∀ a ∈ B ∀ b ∈ B I ↾ B ⁡ a + G b = I ↾ B ⁡ a + G I ↾ B ⁡ b
19 2 2 17 18 syl21anbrc ⊢ G ∈ Grp → I ↾ B ∈ G GrpHom G