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 ˙=rR
subrgdvds.3 E=rS
Assertion subrgdvds ASubRingRE˙

Proof

Step Hyp Ref Expression
1 subrgdvds.1 S=R𝑠A
2 subrgdvds.2 ˙=rR
3 subrgdvds.3 E=rS
4 3 reldvdsr RelE
5 4 a1i ASubRingRRelE
6 1 subrgbas ASubRingRA=BaseS
7 eqid BaseR=BaseR
8 7 subrgss ASubRingRABaseR
9 6 8 eqsstrrd ASubRingRBaseSBaseR
10 9 sseld ASubRingRxBaseSxBaseR
11 eqid R=R
12 1 11 ressmulr ASubRingRR=S
13 12 oveqd ASubRingRzRx=zSx
14 13 eqeq1d ASubRingRzRx=yzSx=y
15 14 rexbidv ASubRingRzBaseSzRx=yzBaseSzSx=y
16 ssrexv BaseSBaseRzBaseSzRx=yzBaseRzRx=y
17 9 16 syl ASubRingRzBaseSzRx=yzBaseRzRx=y
18 15 17 sylbird ASubRingRzBaseSzSx=yzBaseRzRx=y
19 10 18 anim12d ASubRingRxBaseSzBaseSzSx=yxBaseRzBaseRzRx=y
20 eqid BaseS=BaseS
21 eqid S=S
22 20 3 21 dvdsr xEyxBaseSzBaseSzSx=y
23 7 2 11 dvdsr x˙yxBaseRzBaseRzRx=y
24 19 22 23 3imtr4g ASubRingRxEyx˙y
25 df-br xEyxyE
26 df-br x˙yxy˙
27 24 25 26 3imtr3g ASubRingRxyExy˙
28 5 27 relssdv ASubRingRE˙