isrhm

Description: A function is a ring homomorphism iff it preserves both addition and multiplication. (Contributed by Stefan O'Rear, 7-Mar-2015)

	Ref	Expression
Hypotheses	isrhm.m	$⊢ M = {mulGrp}_{R}$
	isrhm.n	$⊢ N = {mulGrp}_{S}$
Assertion	isrhm	$⊢ F \in (R RingHom S) \leftrightarrow ((R \in Ring \land S \in Ring) \land (F \in (R GrpHom S) \land F \in (M MndHom N)))$

Proof

Step	Hyp	Ref	Expression
1		isrhm.m	$⊢ M = {mulGrp}_{R}$
2		isrhm.n	$⊢ N = {mulGrp}_{S}$
3		dfrhm2	$⊢ RingHom = (r \in Ring, s \in Ring ⟼ (r GrpHom s) \cap ({mulGrp}_{r} MndHom {mulGrp}_{s}))$
4	3	elmpocl	$⊢ F \in (R RingHom S) \to (R \in Ring \land S \in Ring)$
5		oveq12	$⊢ (r = R \land s = S) \to r GrpHom s = R GrpHom S$
6		fveq2	$⊢ r = R \to {mulGrp}_{r} = {mulGrp}_{R}$
7		fveq2	$⊢ s = S \to {mulGrp}_{s} = {mulGrp}_{S}$
8	6 7	oveqan12d	$⊢ (r = R \land s = S) \to {mulGrp}_{r} MndHom {mulGrp}_{s} = {mulGrp}_{R} MndHom {mulGrp}_{S}$
9	5 8	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})$
10		ovex	$⊢ R GrpHom S \in V$
11	10	inex1	$⊢ (R GrpHom S) \cap ({mulGrp}_{R} MndHom {mulGrp}_{S}) \in V$
12	9 3 11	ovmpoa	$⊢ (R \in Ring \land S \in Ring) \to R RingHom S = (R GrpHom S) \cap ({mulGrp}_{R} MndHom {mulGrp}_{S})$
13	12	eleq2d	$⊢ (R \in Ring \land S \in Ring) \to (F \in (R RingHom S) \leftrightarrow F \in ((R GrpHom S) \cap ({mulGrp}_{R} MndHom {mulGrp}_{S})))$
14		elin	$⊢ F \in ((R GrpHom S) \cap ({mulGrp}_{R} MndHom {mulGrp}_{S})) \leftrightarrow (F \in (R GrpHom S) \land F \in ({mulGrp}_{R} MndHom {mulGrp}_{S}))$
15	1 2	oveq12i	$⊢ M MndHom N = {mulGrp}_{R} MndHom {mulGrp}_{S}$
16	15	eqcomi	$⊢ {mulGrp}_{R} MndHom {mulGrp}_{S} = M MndHom N$
17	16	eleq2i	$⊢ F \in ({mulGrp}_{R} MndHom {mulGrp}_{S}) \leftrightarrow F \in (M MndHom N)$
18	17	anbi2i	$⊢ (F \in (R GrpHom S) \land F \in ({mulGrp}_{R} MndHom {mulGrp}_{S})) \leftrightarrow (F \in (R GrpHom S) \land F \in (M MndHom N))$
19	14 18	bitri	$⊢ F \in ((R GrpHom S) \cap ({mulGrp}_{R} MndHom {mulGrp}_{S})) \leftrightarrow (F \in (R GrpHom S) \land F \in (M MndHom N))$
20	13 19	bitrdi	$⊢ (R \in Ring \land S \in Ring) \to (F \in (R RingHom S) \leftrightarrow (F \in (R GrpHom S) \land F \in (M MndHom N)))$
21	4 20	biadanii	$⊢ F \in (R RingHom S) \leftrightarrow ((R \in Ring \land S \in Ring) \land (F \in (R GrpHom S) \land F \in (M MndHom N)))$

Metamath Proof Explorer

Theorem isrhm

Proof