idrhm

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

		Ref	Expression
	Hypothesis	idrhm.b	$⊢ B = {Base}_{R}$
	Assertion	idrhm	$⊢ R \in Ring \to {I ↾}_{B} \in (R RingHom R)$

Step	Hyp	Ref	Expression
1		idrhm.b	$⊢ B = {Base}_{R}$
2		id	$⊢ R \in Ring \to R \in Ring$
3		ringgrp	$⊢ R \in Ring \to R \in Grp$
4	1	idghm	$⊢ R \in Grp \to {I ↾}_{B} \in (R GrpHom R)$
5	3 4	syl	$⊢ R \in Ring \to {I ↾}_{B} \in (R GrpHom R)$
6		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
7	6	ringmgp	$⊢ R \in Ring \to {mulGrp}_{R} \in Mnd$
8	6 1	mgpbas	$⊢ B = {Base}_{{mulGrp}_{R}}$
9	8	idmhm	$⊢ {mulGrp}_{R} \in Mnd \to {I ↾}_{B} \in ({mulGrp}_{R} MndHom {mulGrp}_{R})$
10	7 9	syl	$⊢ R \in Ring \to {I ↾}_{B} \in ({mulGrp}_{R} MndHom {mulGrp}_{R})$
11	5 10	jca	$⊢ R \in Ring \to ({I ↾}_{B} \in (R GrpHom R) \land {I ↾}_{B} \in ({mulGrp}_{R} MndHom {mulGrp}_{R}))$
12	6 6	isrhm	$⊢ {I ↾}_{B} \in (R RingHom R) \leftrightarrow ((R \in Ring \land R \in Ring) \land ({I ↾}_{B} \in (R GrpHom R) \land {I ↾}_{B} \in ({mulGrp}_{R} MndHom {mulGrp}_{R})))$
13	2 2 11 12	syl21anbrc	$⊢ R \in Ring \to {I ↾}_{B} \in (R RingHom R)$

Metamath Proof Explorer