rhmval

Description: The ring homomorphisms between two rings. (Contributed by AV, 1-Mar-2020)

		Ref	Expression
	Assertion	rhmval	$⊢ (R \in Ring \land S \in Ring) \to R RingHom S = (R GrpHom S) \cap ({mulGrp}_{R} MndHom {mulGrp}_{S})$

Step	Hyp	Ref	Expression
1		dfrhm2	$⊢ RingHom = (r \in Ring, s \in Ring ⟼ (r GrpHom s) \cap ({mulGrp}_{r} MndHom {mulGrp}_{s}))$
2	1	a1i	$⊢ (R \in Ring \land S \in Ring) \to RingHom = (r \in Ring, s \in Ring ⟼ (r GrpHom s) \cap ({mulGrp}_{r} MndHom {mulGrp}_{s}))$
3		oveq12	$⊢ (r = R \land s = S) \to r GrpHom s = R GrpHom S$
4		fveq2	$⊢ r = R \to {mulGrp}_{r} = {mulGrp}_{R}$
5		fveq2	$⊢ s = S \to {mulGrp}_{s} = {mulGrp}_{S}$
6	4 5	oveqan12d	$⊢ (r = R \land s = S) \to {mulGrp}_{r} MndHom {mulGrp}_{s} = {mulGrp}_{R} MndHom {mulGrp}_{S}$
7	3 6	ineq12d	$⊢ (r = R \land s = S) \to (r GrpHom s) \cap ({mulGrp}_{r} MndHom {mulGrp}_{s}) = (R GrpHom S) \cap ({mulGrp}_{R} MndHom {mulGrp}_{S})$
8	7	adantl	$⊢ ((R \in Ring \land S \in Ring) \land (r = R \land s = S)) \to (r GrpHom s) \cap ({mulGrp}_{r} MndHom {mulGrp}_{s}) = (R GrpHom S) \cap ({mulGrp}_{R} MndHom {mulGrp}_{S})$
9		simpl	$⊢ (R \in Ring \land S \in Ring) \to R \in Ring$
10		simpr	$⊢ (R \in Ring \land S \in Ring) \to S \in Ring$
11		ovex	$⊢ R GrpHom S \in V$
12	11	inex1	$⊢ (R GrpHom S) \cap ({mulGrp}_{R} MndHom {mulGrp}_{S}) \in V$
13	12	a1i	$⊢ (R \in Ring \land S \in Ring) \to (R GrpHom S) \cap ({mulGrp}_{R} MndHom {mulGrp}_{S}) \in V$
14	2 8 9 10 13	ovmpod	$⊢ (R \in Ring \land S \in Ring) \to R RingHom S = (R GrpHom S) \cap ({mulGrp}_{R} MndHom {mulGrp}_{S})$

Metamath Proof Explorer