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