This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 |`s A )
subrgdvds.2 
|- .|| = ( ||r ` R )
subrgdvds.3 
|- E = ( ||r ` S )
Assertion subrgdvds 
|- ( A e. ( SubRing ` R ) -> E C_ .|| )

Proof

Step Hyp Ref Expression
1 subrgdvds.1 
 |-  S = ( R |`s A )
2 subrgdvds.2 
 |-  .|| = ( ||r ` R )
3 subrgdvds.3 
 |-  E = ( ||r ` S )
4 3 reldvdsr 
 |-  Rel E
5 4 a1i 
 |-  ( A e. ( SubRing ` R ) -> Rel E )
6 1 subrgbas 
 |-  ( A e. ( SubRing ` R ) -> A = ( Base ` S ) )
7 eqid 
 |-  ( Base ` R ) = ( Base ` R )
8 7 subrgss 
 |-  ( A e. ( SubRing ` R ) -> A C_ ( Base ` R ) )
9 6 8 eqsstrrd 
 |-  ( A e. ( SubRing ` R ) -> ( Base ` S ) C_ ( Base ` R ) )
10 9 sseld 
 |-  ( A e. ( SubRing ` R ) -> ( x e. ( Base ` S ) -> x e. ( Base ` R ) ) )
11 eqid 
 |-  ( .r ` R ) = ( .r ` R )
12 1 11 ressmulr 
 |-  ( A e. ( SubRing ` R ) -> ( .r ` R ) = ( .r ` S ) )
13 12 oveqd 
 |-  ( A e. ( SubRing ` R ) -> ( z ( .r ` R ) x ) = ( z ( .r ` S ) x ) )
14 13 eqeq1d 
 |-  ( A e. ( SubRing ` R ) -> ( ( z ( .r ` R ) x ) = y <-> ( z ( .r ` S ) x ) = y ) )
15 14 rexbidv 
 |-  ( A e. ( SubRing ` R ) -> ( E. z e. ( Base ` S ) ( z ( .r ` R ) x ) = y <-> E. z e. ( Base ` S ) ( z ( .r ` S ) x ) = y ) )
16 ssrexv 
 |-  ( ( Base ` S ) C_ ( Base ` R ) -> ( E. z e. ( Base ` S ) ( z ( .r ` R ) x ) = y -> E. z e. ( Base ` R ) ( z ( .r ` R ) x ) = y ) )
17 9 16 syl 
 |-  ( A e. ( SubRing ` R ) -> ( E. z e. ( Base ` S ) ( z ( .r ` R ) x ) = y -> E. z e. ( Base ` R ) ( z ( .r ` R ) x ) = y ) )
18 15 17 sylbird 
 |-  ( A e. ( SubRing ` R ) -> ( E. z e. ( Base ` S ) ( z ( .r ` S ) x ) = y -> E. z e. ( Base ` R ) ( z ( .r ` R ) x ) = y ) )
19 10 18 anim12d 
 |-  ( A e. ( SubRing ` R ) -> ( ( x e. ( Base ` S ) /\ E. z e. ( Base ` S ) ( z ( .r ` S ) x ) = y ) -> ( x e. ( Base ` R ) /\ E. z e. ( Base ` R ) ( z ( .r ` R ) x ) = y ) ) )
20 eqid 
 |-  ( Base ` S ) = ( Base ` S )
21 eqid 
 |-  ( .r ` S ) = ( .r ` S )
22 20 3 21 dvdsr 
 |-  ( x E y <-> ( x e. ( Base ` S ) /\ E. z e. ( Base ` S ) ( z ( .r ` S ) x ) = y ) )
23 7 2 11 dvdsr 
 |-  ( x .|| y <-> ( x e. ( Base ` R ) /\ E. z e. ( Base ` R ) ( z ( .r ` R ) x ) = y ) )
24 19 22 23 3imtr4g 
 |-  ( A e. ( SubRing ` R ) -> ( x E y -> x .|| y ) )
25 df-br 
 |-  ( x E y <-> <. x , y >. e. E )
26 df-br 
 |-  ( x .|| y <-> <. x , y >. e. .|| )
27 24 25 26 3imtr3g 
 |-  ( A e. ( SubRing ` R ) -> ( <. x , y >. e. E -> <. x , y >. e. .|| ) )
28 5 27 relssdv 
 |-  ( A e. ( SubRing ` R ) -> E C_ .|| )