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

Metamath Proof Explorer

Theorem subrguss

Description: A unit of a subring is a unit of the parent ring. (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Hypotheses subrguss.1 
|- S = ( R |`s A )
subrguss.2 
|- U = ( Unit ` R )
subrguss.3 
|- V = ( Unit ` S )
Assertion subrguss 
|- ( A e. ( SubRing ` R ) -> V C_ U )

Proof

Step Hyp Ref Expression
1 subrguss.1 
 |-  S = ( R |`s A )
2 subrguss.2 
 |-  U = ( Unit ` R )
3 subrguss.3 
 |-  V = ( Unit ` S )
4 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
5 eqid 
 |-  ( ||r ` S ) = ( ||r ` S )
6 eqid 
 |-  ( oppR ` S ) = ( oppR ` S )
7 eqid 
 |-  ( ||r ` ( oppR ` S ) ) = ( ||r ` ( oppR ` S ) )
8 3 4 5 6 7 isunit 
 |-  ( x e. V <-> ( x ( ||r ` S ) ( 1r ` S ) /\ x ( ||r ` ( oppR ` S ) ) ( 1r ` S ) ) )
9 8 bilani 
 |-  ( ( A e. ( SubRing ` R ) /\ x e. V ) -> ( x ( ||r ` S ) ( 1r ` S ) /\ x ( ||r ` ( oppR ` S ) ) ( 1r ` S ) ) )
10 9 simpld 
 |-  ( ( A e. ( SubRing ` R ) /\ x e. V ) -> x ( ||r ` S ) ( 1r ` S ) )
11 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
12 1 11 subrg1 
 |-  ( A e. ( SubRing ` R ) -> ( 1r ` R ) = ( 1r ` S ) )
13 12 adantr 
 |-  ( ( A e. ( SubRing ` R ) /\ x e. V ) -> ( 1r ` R ) = ( 1r ` S ) )
14 10 13 breqtrrd 
 |-  ( ( A e. ( SubRing ` R ) /\ x e. V ) -> x ( ||r ` S ) ( 1r ` R ) )
15 eqid 
 |-  ( ||r ` R ) = ( ||r ` R )
16 1 15 5 subrgdvds 
 |-  ( A e. ( SubRing ` R ) -> ( ||r ` S ) C_ ( ||r ` R ) )
17 16 adantr 
 |-  ( ( A e. ( SubRing ` R ) /\ x e. V ) -> ( ||r ` S ) C_ ( ||r ` R ) )
18 17 ssbrd 
 |-  ( ( A e. ( SubRing ` R ) /\ x e. V ) -> ( x ( ||r ` S ) ( 1r ` R ) -> x ( ||r ` R ) ( 1r ` R ) ) )
19 14 18 mpd 
 |-  ( ( A e. ( SubRing ` R ) /\ x e. V ) -> x ( ||r ` R ) ( 1r ` R ) )
20 1 subrgbas 
 |-  ( A e. ( SubRing ` R ) -> A = ( Base ` S ) )
21 20 adantr 
 |-  ( ( A e. ( SubRing ` R ) /\ x e. V ) -> A = ( Base ` S ) )
22 eqid 
 |-  ( Base ` R ) = ( Base ` R )
23 22 subrgss 
 |-  ( A e. ( SubRing ` R ) -> A C_ ( Base ` R ) )
24 23 adantr 
 |-  ( ( A e. ( SubRing ` R ) /\ x e. V ) -> A C_ ( Base ` R ) )
25 21 24 eqsstrrd 
 |-  ( ( A e. ( SubRing ` R ) /\ x e. V ) -> ( Base ` S ) C_ ( Base ` R ) )
26 eqid 
 |-  ( Base ` S ) = ( Base ` S )
27 26 3 unitcl 
 |-  ( x e. V -> x e. ( Base ` S ) )
28 27 adantl 
 |-  ( ( A e. ( SubRing ` R ) /\ x e. V ) -> x e. ( Base ` S ) )
29 25 28 sseldd 
 |-  ( ( A e. ( SubRing ` R ) /\ x e. V ) -> x e. ( Base ` R ) )
30 1 subrgring 
 |-  ( A e. ( SubRing ` R ) -> S e. Ring )
31 eqid 
 |-  ( invr ` S ) = ( invr ` S )
32 3 31 26 ringinvcl 
 |-  ( ( S e. Ring /\ x e. V ) -> ( ( invr ` S ) ` x ) e. ( Base ` S ) )
33 30 32 sylan 
 |-  ( ( A e. ( SubRing ` R ) /\ x e. V ) -> ( ( invr ` S ) ` x ) e. ( Base ` S ) )
34 25 33 sseldd 
 |-  ( ( A e. ( SubRing ` R ) /\ x e. V ) -> ( ( invr ` S ) ` x ) e. ( Base ` R ) )
35 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
36 35 22 opprbas 
 |-  ( Base ` R ) = ( Base ` ( oppR ` R ) )
37 eqid 
 |-  ( ||r ` ( oppR ` R ) ) = ( ||r ` ( oppR ` R ) )
38 eqid 
 |-  ( .r ` ( oppR ` R ) ) = ( .r ` ( oppR ` R ) )
39 36 37 38 dvdsrmul 
 |-  ( ( x e. ( Base ` R ) /\ ( ( invr ` S ) ` x ) e. ( Base ` R ) ) -> x ( ||r ` ( oppR ` R ) ) ( ( ( invr ` S ) ` x ) ( .r ` ( oppR ` R ) ) x ) )
40 29 34 39 syl2anc 
 |-  ( ( A e. ( SubRing ` R ) /\ x e. V ) -> x ( ||r ` ( oppR ` R ) ) ( ( ( invr ` S ) ` x ) ( .r ` ( oppR ` R ) ) x ) )
41 eqid 
 |-  ( .r ` R ) = ( .r ` R )
42 22 41 35 38 opprmul 
 |-  ( ( ( invr ` S ) ` x ) ( .r ` ( oppR ` R ) ) x ) = ( x ( .r ` R ) ( ( invr ` S ) ` x ) )
43 eqid 
 |-  ( .r ` S ) = ( .r ` S )
44 3 31 43 4 unitrinv 
 |-  ( ( S e. Ring /\ x e. V ) -> ( x ( .r ` S ) ( ( invr ` S ) ` x ) ) = ( 1r ` S ) )
45 30 44 sylan 
 |-  ( ( A e. ( SubRing ` R ) /\ x e. V ) -> ( x ( .r ` S ) ( ( invr ` S ) ` x ) ) = ( 1r ` S ) )
46 1 41 ressmulr 
 |-  ( A e. ( SubRing ` R ) -> ( .r ` R ) = ( .r ` S ) )
47 46 adantr 
 |-  ( ( A e. ( SubRing ` R ) /\ x e. V ) -> ( .r ` R ) = ( .r ` S ) )
48 47 oveqd 
 |-  ( ( A e. ( SubRing ` R ) /\ x e. V ) -> ( x ( .r ` R ) ( ( invr ` S ) ` x ) ) = ( x ( .r ` S ) ( ( invr ` S ) ` x ) ) )
49 45 48 13 3eqtr4d 
 |-  ( ( A e. ( SubRing ` R ) /\ x e. V ) -> ( x ( .r ` R ) ( ( invr ` S ) ` x ) ) = ( 1r ` R ) )
50 42 49 eqtrid 
 |-  ( ( A e. ( SubRing ` R ) /\ x e. V ) -> ( ( ( invr ` S ) ` x ) ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) )
51 40 50 breqtrd 
 |-  ( ( A e. ( SubRing ` R ) /\ x e. V ) -> x ( ||r ` ( oppR ` R ) ) ( 1r ` R ) )
52 2 11 15 35 37 isunit 
 |-  ( x e. U <-> ( x ( ||r ` R ) ( 1r ` R ) /\ x ( ||r ` ( oppR ` R ) ) ( 1r ` R ) ) )
53 19 51 52 sylanbrc 
 |-  ( ( A e. ( SubRing ` R ) /\ x e. V ) -> x e. U )
54 53 ex 
 |-  ( A e. ( SubRing ` R ) -> ( x e. V -> x e. U ) )
55 54 ssrdv 
 |-  ( A e. ( SubRing ` R ) -> V C_ U )