Theorem rhmdvdsr

Description: A ring homomorphism preserves the divisibility relation. (Contributed by Thierry Arnoux, 22-Oct-2017)

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

Proof

Step	Hyp	Ref	Expression
1		rhmdvdsr.x	$$⊢X={\mathrm{Base}}_R$$
2		rhmdvdsr.m	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
3		rhmdvdsr.n	$$⊢\underset{\dot{}}{\times }={\parallel }_r\left(S\right)$$
4		simpl1	$$⊢\left(\left(F\in \left(R\mathrm{RingHom}S\right)\wedge A\in X\wedge B\in X\right)\wedge A\underset{\dot{}}{\parallel }B\right)\to F\in \left(R\mathrm{RingHom}S\right)$$
5		simpl2	$$⊢\left(\left(F\in \left(R\mathrm{RingHom}S\right)\wedge A\in X\wedge B\in X\right)\wedge A\underset{\dot{}}{\parallel }B\right)\to A\in X$$
6		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
7	1 6	rhmf	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to F:X⟶{\mathrm{Base}}_S$$
8	7	ffvelcdmda	$$⊢\left(F\in \left(R\mathrm{RingHom}S\right)\wedge A\in X\right)\to F\left(A\right)\in {\mathrm{Base}}_S$$
9	4 5 8	syl2anc	$$⊢\left(\left(F\in \left(R\mathrm{RingHom}S\right)\wedge A\in X\wedge B\in X\right)\wedge A\underset{\dot{}}{\parallel }B\right)\to F\left(A\right)\in {\mathrm{Base}}_S$$
10		simpll1	$$⊢\left(\left(\left(F\in \left(R\mathrm{RingHom}S\right)\wedge A\in X\wedge B\in X\right)\wedge A\underset{\dot{}}{\parallel }B\right)\wedge c\in X\right)\to F\in \left(R\mathrm{RingHom}S\right)$$
11		simpr	$$⊢\left(\left(\left(F\in \left(R\mathrm{RingHom}S\right)\wedge A\in X\wedge B\in X\right)\wedge A\underset{\dot{}}{\parallel }B\right)\wedge c\in X\right)\to c\in X$$
12	7	ffvelcdmda	$$⊢\left(F\in \left(R\mathrm{RingHom}S\right)\wedge c\in X\right)\to F\left(c\right)\in {\mathrm{Base}}_S$$
13	10 11 12	syl2anc	$$⊢\left(\left(\left(F\in \left(R\mathrm{RingHom}S\right)\wedge A\in X\wedge B\in X\right)\wedge A\underset{\dot{}}{\parallel }B\right)\wedge c\in X\right)\to F\left(c\right)\in {\mathrm{Base}}_S$$
14	13	ralrimiva	$$⊢\left(\left(F\in \left(R\mathrm{RingHom}S\right)\wedge A\in X\wedge B\in X\right)\wedge A\underset{\dot{}}{\parallel }B\right)\to \forall c\in XF\left(c\right)\in {\mathrm{Base}}_S$$
15	5	adantr	$$⊢\left(\left(\left(F\in \left(R\mathrm{RingHom}S\right)\wedge A\in X\wedge B\in X\right)\wedge A\underset{\dot{}}{\parallel }B\right)\wedge c\in X\right)\to A\in X$$
16		eqid	$$⊢{\cdot }_R={\cdot }_R$$
17		eqid	$$⊢{\cdot }_S={\cdot }_S$$
18	1 16 17	rhmmul	$$⊢\left(F\in \left(R\mathrm{RingHom}S\right)\wedge c\in X\wedge A\in X\right)\to F\left(c{\cdot }_{R}A\right)=F\left(c\right){\cdot }_{S}F\left(A\right)$$
19	10 11 15 18	syl3anc	$$⊢\left(\left(\left(F\in \left(R\mathrm{RingHom}S\right)\wedge A\in X\wedge B\in X\right)\wedge A\underset{\dot{}}{\parallel }B\right)\wedge c\in X\right)\to F\left(c{\cdot }_{R}A\right)=F\left(c\right){\cdot }_{S}F\left(A\right)$$
20	19	ralrimiva	$$⊢\left(\left(F\in \left(R\mathrm{RingHom}S\right)\wedge A\in X\wedge B\in X\right)\wedge A\underset{\dot{}}{\parallel }B\right)\to \forall c\in XF\left(c{\cdot }_{R}A\right)=F\left(c\right){\cdot }_{S}F\left(A\right)$$
21		simpr	$$⊢\left(\left(F\in \left(R\mathrm{RingHom}S\right)\wedge A\in X\wedge B\in X\right)\wedge A\underset{\dot{}}{\parallel }B\right)\to A\underset{\dot{}}{\parallel }B$$
22	1 2 16	dvdsr2	$$⊢A\in X\to \left(A\underset{\dot{}}{\parallel }B\leftrightarrow \exists c\in Xc{\cdot }_{R}A=B\right)$$
23	22	biimpac	$$⊢\left(A\underset{\dot{}}{\parallel }B\wedge A\in X\right)\to \exists c\in Xc{\cdot }_{R}A=B$$
24	21 5 23	syl2anc	$$⊢\left(\left(F\in \left(R\mathrm{RingHom}S\right)\wedge A\in X\wedge B\in X\right)\wedge A\underset{\dot{}}{\parallel }B\right)\to \exists c\in Xc{\cdot }_{R}A=B$$
25		r19.29	$$⊢\left(\forall c\in XF\left(c{\cdot }_{R}A\right)=F\left(c\right){\cdot }_{S}F\left(A\right)\wedge \exists c\in Xc{\cdot }_{R}A=B\right)\to \exists c\in X\left(F\left(c{\cdot }_{R}A\right)=F\left(c\right){\cdot }_{S}F\left(A\right)\wedge c{\cdot }_{R}A=B\right)$$
26		simpl	$$⊢\left(F\left(c{\cdot }_{R}A\right)=F\left(c\right){\cdot }_{S}F\left(A\right)\wedge c{\cdot }_{R}A=B\right)\to F\left(c{\cdot }_{R}A\right)=F\left(c\right){\cdot }_{S}F\left(A\right)$$
27		simpr	$$⊢\left(F\left(c{\cdot }_{R}A\right)=F\left(c\right){\cdot }_{S}F\left(A\right)\wedge c{\cdot }_{R}A=B\right)\to c{\cdot }_{R}A=B$$
28	27	fveq2d	$$⊢\left(F\left(c{\cdot }_{R}A\right)=F\left(c\right){\cdot }_{S}F\left(A\right)\wedge c{\cdot }_{R}A=B\right)\to F\left(c{\cdot }_{R}A\right)=F\left(B\right)$$
29	26 28	eqtr3d	$$⊢\left(F\left(c{\cdot }_{R}A\right)=F\left(c\right){\cdot }_{S}F\left(A\right)\wedge c{\cdot }_{R}A=B\right)\to F\left(c\right){\cdot }_{S}F\left(A\right)=F\left(B\right)$$
30	29	reximi	$$⊢\exists c\in X\left(F\left(c{\cdot }_{R}A\right)=F\left(c\right){\cdot }_{S}F\left(A\right)\wedge c{\cdot }_{R}A=B\right)\to \exists c\in XF\left(c\right){\cdot }_{S}F\left(A\right)=F\left(B\right)$$
31	25 30	syl	$$⊢\left(\forall c\in XF\left(c{\cdot }_{R}A\right)=F\left(c\right){\cdot }_{S}F\left(A\right)\wedge \exists c\in Xc{\cdot }_{R}A=B\right)\to \exists c\in XF\left(c\right){\cdot }_{S}F\left(A\right)=F\left(B\right)$$
32	20 24 31	syl2anc	$$⊢\left(\left(F\in \left(R\mathrm{RingHom}S\right)\wedge A\in X\wedge B\in X\right)\wedge A\underset{\dot{}}{\parallel }B\right)\to \exists c\in XF\left(c\right){\cdot }_{S}F\left(A\right)=F\left(B\right)$$
33		r19.29	$$⊢\left(\forall c\in XF\left(c\right)\in {\mathrm{Base}}_S\wedge \exists c\in XF\left(c\right){\cdot }_{S}F\left(A\right)=F\left(B\right)\right)\to \exists c\in X\left(F\left(c\right)\in {\mathrm{Base}}_S\wedge F\left(c\right){\cdot }_{S}F\left(A\right)=F\left(B\right)\right)$$
34	14 32 33	syl2anc	$$⊢\left(\left(F\in \left(R\mathrm{RingHom}S\right)\wedge A\in X\wedge B\in X\right)\wedge A\underset{\dot{}}{\parallel }B\right)\to \exists c\in X\left(F\left(c\right)\in {\mathrm{Base}}_S\wedge F\left(c\right){\cdot }_{S}F\left(A\right)=F\left(B\right)\right)$$
35		oveq1	$$⊢y=F\left(c\right)\to y{\cdot }_{S}F\left(A\right)=F\left(c\right){\cdot }_{S}F\left(A\right)$$
36	35	eqeq1d	$$⊢y=F\left(c\right)\to \left(y{\cdot }_{S}F\left(A\right)=F\left(B\right)\leftrightarrow F\left(c\right){\cdot }_{S}F\left(A\right)=F\left(B\right)\right)$$
37	36	rspcev	$$⊢\left(F\left(c\right)\in {\mathrm{Base}}_S\wedge F\left(c\right){\cdot }_{S}F\left(A\right)=F\left(B\right)\right)\to \exists y\in {\mathrm{Base}}_{S}y{\cdot }_{S}F\left(A\right)=F\left(B\right)$$
38	37	rexlimivw	$$⊢\exists c\in X\left(F\left(c\right)\in {\mathrm{Base}}_S\wedge F\left(c\right){\cdot }_{S}F\left(A\right)=F\left(B\right)\right)\to \exists y\in {\mathrm{Base}}_{S}y{\cdot }_{S}F\left(A\right)=F\left(B\right)$$
39	34 38	syl	$$⊢\left(\left(F\in \left(R\mathrm{RingHom}S\right)\wedge A\in X\wedge B\in X\right)\wedge A\underset{\dot{}}{\parallel }B\right)\to \exists y\in {\mathrm{Base}}_{S}y{\cdot }_{S}F\left(A\right)=F\left(B\right)$$
40	6 3 17	dvdsr	$$⊢F\left(A\right)\underset{\dot{}}{\times }F\left(B\right)\leftrightarrow \left(F\left(A\right)\in {\mathrm{Base}}_S\wedge \exists y\in {\mathrm{Base}}_{S}y{\cdot }_{S}F\left(A\right)=F\left(B\right)\right)$$
41	9 39 40	sylanbrc	$$⊢\left(\left(F\in \left(R\mathrm{RingHom}S\right)\wedge A\in X\wedge B\in X\right)\wedge A\underset{\dot{}}{\parallel }B\right)\to F\left(A\right)\underset{\dot{}}{\times }F\left(B\right)$$