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 | |
|
subrgdvds.2 | |
||
subrgdvds.3 | |
||
Assertion | subrgdvds | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | subrgdvds.1 | |
|
2 | subrgdvds.2 | |
|
3 | subrgdvds.3 | |
|
4 | 3 | reldvdsr | |
5 | 4 | a1i | |
6 | 1 | subrgbas | |
7 | eqid | |
|
8 | 7 | subrgss | |
9 | 6 8 | eqsstrrd | |
10 | 9 | sseld | |
11 | eqid | |
|
12 | 1 11 | ressmulr | |
13 | 12 | oveqd | |
14 | 13 | eqeq1d | |
15 | 14 | rexbidv | |
16 | ssrexv | |
|
17 | 9 16 | syl | |
18 | 15 17 | sylbird | |
19 | 10 18 | anim12d | |
20 | eqid | |
|
21 | eqid | |
|
22 | 20 3 21 | dvdsr | |
23 | 7 2 11 | dvdsr | |
24 | 19 22 23 | 3imtr4g | |
25 | df-br | |
|
26 | df-br | |
|
27 | 24 25 26 | 3imtr3g | |
28 | 5 27 | relssdv | |