Theorem rnghmmul

Description: A homomorphism of non-unital rings preserves multiplication. (Contributed by AV, 23-Feb-2020)

	Ref	Expression
Hypotheses	rnghmmul.x	$$⊢X={\mathrm{Base}}_R$$
	rnghmmul.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	rnghmmul.n	$$⊢\underset{\dot{}}{\times }={\cdot }_S$$
Assertion	rnghmmul	$$⊢\left(F\in \left(R\mathrm{RngHomo}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		rnghmmul.x	$$⊢X={\mathrm{Base}}_R$$
2		rnghmmul.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		rnghmmul.n	$$⊢\underset{\dot{}}{\times }={\cdot }_S$$
4	1 2 3	isrnghm	$$⊢F\in \left(R\mathrm{RngHomo}S\right)\leftrightarrow \left(\left(R\in \mathrm{Rng}\wedge S\in \mathrm{Rng}\right)\wedge \left(F\in \left(R\mathrm{GrpHom}S\right)\wedge \forall x\in X\forall y\in XF\left(x\underset{\dot{}}{·}y\right)=F\left(x\right)\underset{\dot{}}{\times }F\left(y\right)\right)\right)$$
5		fvoveq1	$$⊢x=A\to F\left(x\underset{\dot{}}{·}y\right)=F\left(A\underset{\dot{}}{·}y\right)$$
6		fveq2	$$⊢x=A\to F\left(x\right)=F\left(A\right)$$
7	6	oveq1d	$$⊢x=A\to F\left(x\right)\underset{\dot{}}{\times }F\left(y\right)=F\left(A\right)\underset{\dot{}}{\times }F\left(y\right)$$
8	5 7	eqeq12d	$$⊢x=A\to \left(F\left(x\underset{\dot{}}{·}y\right)=F\left(x\right)\underset{\dot{}}{\times }F\left(y\right)\leftrightarrow F\left(A\underset{\dot{}}{·}y\right)=F\left(A\right)\underset{\dot{}}{\times }F\left(y\right)\right)$$
9		oveq2	$$⊢y=B\to A\underset{\dot{}}{·}y=A\underset{\dot{}}{·}B$$
10	9	fveq2d	$$⊢y=B\to F\left(A\underset{\dot{}}{·}y\right)=F\left(A\underset{\dot{}}{·}B\right)$$
11		fveq2	$$⊢y=B\to F\left(y\right)=F\left(B\right)$$
12	11	oveq2d	$$⊢y=B\to F\left(A\right)\underset{\dot{}}{\times }F\left(y\right)=F\left(A\right)\underset{\dot{}}{\times }F\left(B\right)$$
13	10 12	eqeq12d	$$⊢y=B\to \left(F\left(A\underset{\dot{}}{·}y\right)=F\left(A\right)\underset{\dot{}}{\times }F\left(y\right)\leftrightarrow F\left(A\underset{\dot{}}{·}B\right)=F\left(A\right)\underset{\dot{}}{\times }F\left(B\right)\right)$$
14	8 13	rspc2va	$$⊢\left(\left(A\in X\wedge B\in X\right)\wedge \forall x\in X\forall y\in XF\left(x\underset{\dot{}}{·}y\right)=F\left(x\right)\underset{\dot{}}{\times }F\left(y\right)\right)\to F\left(A\underset{\dot{}}{·}B\right)=F\left(A\right)\underset{\dot{}}{\times }F\left(B\right)$$
15	14	expcom	$$⊢\forall x\in X\forall y\in XF\left(x\underset{\dot{}}{·}y\right)=F\left(x\right)\underset{\dot{}}{\times }F\left(y\right)\to \left(\left(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)\right)$$
16	15	ad2antll	$$⊢\left(\left(R\in \mathrm{Rng}\wedge S\in \mathrm{Rng}\right)\wedge \left(F\in \left(R\mathrm{GrpHom}S\right)\wedge \forall x\in X\forall y\in XF\left(x\underset{\dot{}}{·}y\right)=F\left(x\right)\underset{\dot{}}{\times }F\left(y\right)\right)\right)\to \left(\left(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)\right)$$
17	4 16	sylbi	$$⊢F\in \left(R\mathrm{RngHomo}S\right)\to \left(\left(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)\right)$$
18	17	3impib	$$⊢\left(F\in \left(R\mathrm{RngHomo}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)$$