Theorem subrgdvds

Description: If an element divides another in a subring, then it also divides the other in the parent ring. (Contributed by Mario Carneiro, 4-Dec-2014)

	Ref	Expression
Hypotheses	subrgdvds.1	$$⊢S=R{\upharpoonright }_{𝑠}A$$
	subrgdvds.2	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
	subrgdvds.3	$$⊢E={\parallel }_r\left(S\right)$$
Assertion	subrgdvds	$$⊢A\in \mathrm{SubRing}\left(R\right)\to E\subseteq \underset{\dot{}}{\parallel }$$

Proof

Step	Hyp	Ref	Expression
1		subrgdvds.1	$$⊢S=R{\upharpoonright }_{𝑠}A$$
2		subrgdvds.2	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
3		subrgdvds.3	$$⊢E={\parallel }_r\left(S\right)$$
4	3	reldvdsr	$$⊢\mathrm{Rel}E$$
5	4	a1i	$$⊢A\in \mathrm{SubRing}\left(R\right)\to \mathrm{Rel}E$$
6	1	subrgbas	$$⊢A\in \mathrm{SubRing}\left(R\right)\to A={\mathrm{Base}}_S$$
7		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
8	7	subrgss	$$⊢A\in \mathrm{SubRing}\left(R\right)\to A\subseteq {\mathrm{Base}}_R$$
9	6 8	eqsstrrd	$$⊢A\in \mathrm{SubRing}\left(R\right)\to {\mathrm{Base}}_S\subseteq {\mathrm{Base}}_R$$
10	9	sseld	$$⊢A\in \mathrm{SubRing}\left(R\right)\to \left(x\in {\mathrm{Base}}_S\to x\in {\mathrm{Base}}_R\right)$$
11		eqid	$$⊢{\cdot }_R={\cdot }_R$$
12	1 11	ressmulr	$$⊢A\in \mathrm{SubRing}\left(R\right)\to {\cdot }_R={\cdot }_S$$
13	12	oveqd	$$⊢A\in \mathrm{SubRing}\left(R\right)\to z{\cdot }_{R}x=z{\cdot }_{S}x$$
14	13	eqeq1d	$$⊢A\in \mathrm{SubRing}\left(R\right)\to \left(z{\cdot }_{R}x=y\leftrightarrow z{\cdot }_{S}x=y\right)$$
15	14	rexbidv	$$⊢A\in \mathrm{SubRing}\left(R\right)\to \left(\exists z\in {\mathrm{Base}}_{S}z{\cdot }_{R}x=y\leftrightarrow \exists z\in {\mathrm{Base}}_{S}z{\cdot }_{S}x=y\right)$$
16		ssrexv	$$⊢{\mathrm{Base}}_S\subseteq {\mathrm{Base}}_R\to \left(\exists z\in {\mathrm{Base}}_{S}z{\cdot }_{R}x=y\to \exists z\in {\mathrm{Base}}_{R}z{\cdot }_{R}x=y\right)$$
17	9 16	syl	$$⊢A\in \mathrm{SubRing}\left(R\right)\to \left(\exists z\in {\mathrm{Base}}_{S}z{\cdot }_{R}x=y\to \exists z\in {\mathrm{Base}}_{R}z{\cdot }_{R}x=y\right)$$
18	15 17	sylbird	$$⊢A\in \mathrm{SubRing}\left(R\right)\to \left(\exists z\in {\mathrm{Base}}_{S}z{\cdot }_{S}x=y\to \exists z\in {\mathrm{Base}}_{R}z{\cdot }_{R}x=y\right)$$
19	10 18	anim12d	$$⊢A\in \mathrm{SubRing}\left(R\right)\to \left(\left(x\in {\mathrm{Base}}_S\wedge \exists z\in {\mathrm{Base}}_{S}z{\cdot }_{S}x=y\right)\to \left(x\in {\mathrm{Base}}_R\wedge \exists z\in {\mathrm{Base}}_{R}z{\cdot }_{R}x=y\right)\right)$$
20		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
21		eqid	$$⊢{\cdot }_S={\cdot }_S$$
22	20 3 21	dvdsr	$$⊢xEy\leftrightarrow \left(x\in {\mathrm{Base}}_S\wedge \exists z\in {\mathrm{Base}}_{S}z{\cdot }_{S}x=y\right)$$
23	7 2 11	dvdsr	$$⊢x\underset{\dot{}}{\parallel }y\leftrightarrow \left(x\in {\mathrm{Base}}_R\wedge \exists z\in {\mathrm{Base}}_{R}z{\cdot }_{R}x=y\right)$$
24	19 22 23	3imtr4g	$$⊢A\in \mathrm{SubRing}\left(R\right)\to \left(xEy\to x\underset{\dot{}}{\parallel }y\right)$$
25		df-br	$$⊢xEy\leftrightarrow ⟨x,y⟩\in E$$
26		df-br	$$⊢x\underset{\dot{}}{\parallel }y\leftrightarrow ⟨x,y⟩\in \underset{\dot{}}{\parallel }$$
27	24 25 26	3imtr3g	$$⊢A\in \mathrm{SubRing}\left(R\right)\to \left(⟨x,y⟩\in E\to ⟨x,y⟩\in \underset{\dot{}}{\parallel }\right)$$
28	5 27	relssdv	$$⊢A\in \mathrm{SubRing}\left(R\right)\to E\subseteq \underset{\dot{}}{\parallel }$$