Metamath Proof Explorer

Theorem subrgunit

Description: An element of a ring is a unit of a subring iff it is a unit of the parent ring and both it and its inverse are in the subring. (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Hypotheses subrgugrp.1 
|- S = ( R |`s A )
subrgugrp.2 
|- U = ( Unit ` R )
subrgugrp.3 
|- V = ( Unit ` S )
subrgunit.4 
|- I = ( invr ` R )
Assertion subrgunit 
|- ( A e. ( SubRing ` R ) -> ( X e. V <-> ( X e. U /\ X e. A /\ ( I ` X ) e. A ) ) )

Proof

Step Hyp Ref Expression
1 subrgugrp.1 
 |-  S = ( R |`s A )
2 subrgugrp.2 
 |-  U = ( Unit ` R )
3 subrgugrp.3 
 |-  V = ( Unit ` S )
4 subrgunit.4 
 |-  I = ( invr ` R )
5 1 2 3 subrguss 
 |-  ( A e. ( SubRing ` R ) -> V C_ U )
6 5 sselda 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. V ) -> X e. U )
7 eqid 
 |-  ( Base ` S ) = ( Base ` S )
8 7 3 unitcl 
 |-  ( X e. V -> X e. ( Base ` S ) )
9 8 adantl 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. V ) -> X e. ( Base ` S ) )
10 1 subrgbas 
 |-  ( A e. ( SubRing ` R ) -> A = ( Base ` S ) )
11 10 adantr 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. V ) -> A = ( Base ` S ) )
12 9 11 eleqtrrd 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. V ) -> X e. A )
13 1 subrgring 
 |-  ( A e. ( SubRing ` R ) -> S e. Ring )
14 eqid 
 |-  ( invr ` S ) = ( invr ` S )
15 3 14 7 ringinvcl 
 |-  ( ( S e. Ring /\ X e. V ) -> ( ( invr ` S ) ` X ) e. ( Base ` S ) )
16 13 15 sylan 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. V ) -> ( ( invr ` S ) ` X ) e. ( Base ` S ) )
17 1 4 3 14 subrginv 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. V ) -> ( I ` X ) = ( ( invr ` S ) ` X ) )
18 16 17 11 3eltr4d 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. V ) -> ( I ` X ) e. A )
19 6 12 18 3jca 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. V ) -> ( X e. U /\ X e. A /\ ( I ` X ) e. A ) )
20 simpr2 
 |-  ( ( A e. ( SubRing ` R ) /\ ( X e. U /\ X e. A /\ ( I ` X ) e. A ) ) -> X e. A )
21 10 adantr 
 |-  ( ( A e. ( SubRing ` R ) /\ ( X e. U /\ X e. A /\ ( I ` X ) e. A ) ) -> A = ( Base ` S ) )
22 20 21 eleqtrd 
 |-  ( ( A e. ( SubRing ` R ) /\ ( X e. U /\ X e. A /\ ( I ` X ) e. A ) ) -> X e. ( Base ` S ) )
23 simpr3 
 |-  ( ( A e. ( SubRing ` R ) /\ ( X e. U /\ X e. A /\ ( I ` X ) e. A ) ) -> ( I ` X ) e. A )
24 23 21 eleqtrd 
 |-  ( ( A e. ( SubRing ` R ) /\ ( X e. U /\ X e. A /\ ( I ` X ) e. A ) ) -> ( I ` X ) e. ( Base ` S ) )
25 eqid 
 |-  ( ||r ` S ) = ( ||r ` S )
26 eqid 
 |-  ( .r ` S ) = ( .r ` S )
27 7 25 26 dvdsrmul 
 |-  ( ( X e. ( Base ` S ) /\ ( I ` X ) e. ( Base ` S ) ) -> X ( ||r ` S ) ( ( I ` X ) ( .r ` S ) X ) )
28 22 24 27 syl2anc 
 |-  ( ( A e. ( SubRing ` R ) /\ ( X e. U /\ X e. A /\ ( I ` X ) e. A ) ) -> X ( ||r ` S ) ( ( I ` X ) ( .r ` S ) X ) )
29 subrgrcl 
 |-  ( A e. ( SubRing ` R ) -> R e. Ring )
30 29 adantr 
 |-  ( ( A e. ( SubRing ` R ) /\ ( X e. U /\ X e. A /\ ( I ` X ) e. A ) ) -> R e. Ring )
31 simpr1 
 |-  ( ( A e. ( SubRing ` R ) /\ ( X e. U /\ X e. A /\ ( I ` X ) e. A ) ) -> X e. U )
32 eqid 
 |-  ( .r ` R ) = ( .r ` R )
33 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
34 2 4 32 33 unitlinv 
 |-  ( ( R e. Ring /\ X e. U ) -> ( ( I ` X ) ( .r ` R ) X ) = ( 1r ` R ) )
35 30 31 34 syl2anc 
 |-  ( ( A e. ( SubRing ` R ) /\ ( X e. U /\ X e. A /\ ( I ` X ) e. A ) ) -> ( ( I ` X ) ( .r ` R ) X ) = ( 1r ` R ) )
36 1 32 ressmulr 
 |-  ( A e. ( SubRing ` R ) -> ( .r ` R ) = ( .r ` S ) )
37 36 adantr 
 |-  ( ( A e. ( SubRing ` R ) /\ ( X e. U /\ X e. A /\ ( I ` X ) e. A ) ) -> ( .r ` R ) = ( .r ` S ) )
38 37 oveqd 
 |-  ( ( A e. ( SubRing ` R ) /\ ( X e. U /\ X e. A /\ ( I ` X ) e. A ) ) -> ( ( I ` X ) ( .r ` R ) X ) = ( ( I ` X ) ( .r ` S ) X ) )
39 1 33 subrg1 
 |-  ( A e. ( SubRing ` R ) -> ( 1r ` R ) = ( 1r ` S ) )
40 39 adantr 
 |-  ( ( A e. ( SubRing ` R ) /\ ( X e. U /\ X e. A /\ ( I ` X ) e. A ) ) -> ( 1r ` R ) = ( 1r ` S ) )
41 35 38 40 3eqtr3d 
 |-  ( ( A e. ( SubRing ` R ) /\ ( X e. U /\ X e. A /\ ( I ` X ) e. A ) ) -> ( ( I ` X ) ( .r ` S ) X ) = ( 1r ` S ) )
42 28 41 breqtrd 
 |-  ( ( A e. ( SubRing ` R ) /\ ( X e. U /\ X e. A /\ ( I ` X ) e. A ) ) -> X ( ||r ` S ) ( 1r ` S ) )
43 eqid 
 |-  ( oppR ` S ) = ( oppR ` S )
44 43 7 opprbas 
 |-  ( Base ` S ) = ( Base ` ( oppR ` S ) )
45 eqid 
 |-  ( ||r ` ( oppR ` S ) ) = ( ||r ` ( oppR ` S ) )
46 eqid 
 |-  ( .r ` ( oppR ` S ) ) = ( .r ` ( oppR ` S ) )
47 44 45 46 dvdsrmul 
 |-  ( ( X e. ( Base ` S ) /\ ( I ` X ) e. ( Base ` S ) ) -> X ( ||r ` ( oppR ` S ) ) ( ( I ` X ) ( .r ` ( oppR ` S ) ) X ) )
48 22 24 47 syl2anc 
 |-  ( ( A e. ( SubRing ` R ) /\ ( X e. U /\ X e. A /\ ( I ` X ) e. A ) ) -> X ( ||r ` ( oppR ` S ) ) ( ( I ` X ) ( .r ` ( oppR ` S ) ) X ) )
49 7 26 43 46 opprmul 
 |-  ( ( I ` X ) ( .r ` ( oppR ` S ) ) X ) = ( X ( .r ` S ) ( I ` X ) )
50 2 4 32 33 unitrinv 
 |-  ( ( R e. Ring /\ X e. U ) -> ( X ( .r ` R ) ( I ` X ) ) = ( 1r ` R ) )
51 30 31 50 syl2anc 
 |-  ( ( A e. ( SubRing ` R ) /\ ( X e. U /\ X e. A /\ ( I ` X ) e. A ) ) -> ( X ( .r ` R ) ( I ` X ) ) = ( 1r ` R ) )
52 37 oveqd 
 |-  ( ( A e. ( SubRing ` R ) /\ ( X e. U /\ X e. A /\ ( I ` X ) e. A ) ) -> ( X ( .r ` R ) ( I ` X ) ) = ( X ( .r ` S ) ( I ` X ) ) )
53 51 52 40 3eqtr3d 
 |-  ( ( A e. ( SubRing ` R ) /\ ( X e. U /\ X e. A /\ ( I ` X ) e. A ) ) -> ( X ( .r ` S ) ( I ` X ) ) = ( 1r ` S ) )
54 49 53 syl5eq 
 |-  ( ( A e. ( SubRing ` R ) /\ ( X e. U /\ X e. A /\ ( I ` X ) e. A ) ) -> ( ( I ` X ) ( .r ` ( oppR ` S ) ) X ) = ( 1r ` S ) )
55 48 54 breqtrd 
 |-  ( ( A e. ( SubRing ` R ) /\ ( X e. U /\ X e. A /\ ( I ` X ) e. A ) ) -> X ( ||r ` ( oppR ` S ) ) ( 1r ` S ) )
56 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
57 3 56 25 43 45 isunit 
 |-  ( X e. V <-> ( X ( ||r ` S ) ( 1r ` S ) /\ X ( ||r ` ( oppR ` S ) ) ( 1r ` S ) ) )
58 42 55 57 sylanbrc 
 |-  ( ( A e. ( SubRing ` R ) /\ ( X e. U /\ X e. A /\ ( I ` X ) e. A ) ) -> X e. V )
59 19 58 impbida 
 |-  ( A e. ( SubRing ` R ) -> ( X e. V <-> ( X e. U /\ X e. A /\ ( I ` X ) e. A ) ) )