Theorem rhmmul

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

	Ref	Expression
Hypotheses	rhmmul.x	$$⊢X={\mathrm{Base}}_R$$
	rhmmul.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	rhmmul.n	$$⊢\underset{\dot{}}{\times }={\cdot }_S$$
Assertion	rhmmul	$$⊢\left(F\in \left(R\mathrm{RingHom}S\right)\wedge A\in X\wedge B\in X\right)\to F\left(A\underset{\dot{}}{·}B\right)=F\left(A\right)\underset{\dot{}}{\times }F\left(B\right)$$

Proof

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