rhmmul

Description: A homomorphism of rings preserves multiplication. (Contributed by Mario Carneiro, 12-Jun-2015)

	Ref	Expression
Hypotheses	rhmmul.x	$⊢ X = {Base}_{R}$
	rhmmul.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	rhmmul.n	$⊢ \underset{˙}{\times} = \cdot_{S}$
Assertion	rhmmul	$⊢ (F \in (R RingHom S) \land A \in X \land B \in X) \to F (A \underset{˙}{\cdot} B) = F (A) \underset{˙}{\times} F (B)$

Step	Hyp	Ref	Expression
1		rhmmul.x	$⊢ X = {Base}_{R}$
2		rhmmul.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		rhmmul.n	$⊢ \underset{˙}{\times} = \cdot_{S}$
4		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
5		eqid	$⊢ {mulGrp}_{S} = {mulGrp}_{S}$
6	4 5	rhmmhm	$⊢ F \in (R RingHom S) \to F \in ({mulGrp}_{R} MndHom {mulGrp}_{S})$
7	4 1	mgpbas	$⊢ X = {Base}_{{mulGrp}_{R}}$
8	4 2	mgpplusg	$⊢ \underset{˙}{\cdot} = +_{{mulGrp}_{R}}$
9	5 3	mgpplusg	$⊢ \underset{˙}{\times} = +_{{mulGrp}_{S}}$
10	7 8 9	mhmlin	$⊢ (F \in ({mulGrp}_{R} MndHom {mulGrp}_{S}) \land A \in X \land B \in X) \to F (A \underset{˙}{\cdot} B) = F (A) \underset{˙}{\times} F (B)$
11	6 10	syl3an1	$⊢ (F \in (R RingHom S) \land A \in X \land B \in X) \to F (A \underset{˙}{\cdot} B) = F (A) \underset{˙}{\times} F (B)$

Metamath Proof Explorer