# Metamath Proof Explorer

## 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}{↾}_{𝑠}{A}$
subrgdvds.2
subrgdvds.3 ${⊢}{E}={\parallel }_{r}\left({S}\right)$
Assertion subrgdvds

### Proof

Step Hyp Ref Expression
1 subrgdvds.1 ${⊢}{S}={R}{↾}_{𝑠}{A}$
2 subrgdvds.2
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}↔{z}{\cdot }_{{S}}{x}={y}\right)$
15 14 rexbidv ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to \left(\exists {z}\in {\mathrm{Base}}_{{S}}\phantom{\rule{.4em}{0ex}}{z}{\cdot }_{{R}}{x}={y}↔\exists {z}\in {\mathrm{Base}}_{{S}}\phantom{\rule{.4em}{0ex}}{z}{\cdot }_{{S}}{x}={y}\right)$
16 ssrexv ${⊢}{\mathrm{Base}}_{{S}}\subseteq {\mathrm{Base}}_{{R}}\to \left(\exists {z}\in {\mathrm{Base}}_{{S}}\phantom{\rule{.4em}{0ex}}{z}{\cdot }_{{R}}{x}={y}\to \exists {z}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}{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}}\phantom{\rule{.4em}{0ex}}{z}{\cdot }_{{R}}{x}={y}\to \exists {z}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}{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}}\phantom{\rule{.4em}{0ex}}{z}{\cdot }_{{S}}{x}={y}\to \exists {z}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}{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}}\phantom{\rule{.4em}{0ex}}{z}{\cdot }_{{S}}{x}={y}\right)\to \left({x}\in {\mathrm{Base}}_{{R}}\wedge \exists {z}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}{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 ${⊢}{x}{E}{y}↔\left({x}\in {\mathrm{Base}}_{{S}}\wedge \exists {z}\in {\mathrm{Base}}_{{S}}\phantom{\rule{.4em}{0ex}}{z}{\cdot }_{{S}}{x}={y}\right)$
23 7 2 11 dvdsr
24 19 22 23 3imtr4g
25 df-br ${⊢}{x}{E}{y}↔⟨{x},{y}⟩\in {E}$
26 df-br
27 24 25 26 3imtr3g
28 5 27 relssdv