Metamath Proof Explorer

Theorem subrginv

Description: A subring always has the same inversion function, for elements that are invertible. (Contributed by Mario Carneiro, 4-Dec-2014)

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

Proof

Step Hyp Ref Expression
1 subrginv.1 
 |-  S = ( R |`s A )
2 subrginv.2 
 |-  I = ( invr ` R )
3 subrginv.3 
 |-  U = ( Unit ` S )
4 subrginv.4 
 |-  J = ( invr ` S )
5 subrgrcl 
 |-  ( A e. ( SubRing ` R ) -> R e. Ring )
6 5 adantr 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. U ) -> R e. Ring )
7 1 subrgbas 
 |-  ( A e. ( SubRing ` R ) -> A = ( Base ` S ) )
8 eqid 
 |-  ( Base ` R ) = ( Base ` R )
9 8 subrgss 
 |-  ( A e. ( SubRing ` R ) -> A C_ ( Base ` R ) )
10 7 9 eqsstrrd 
 |-  ( A e. ( SubRing ` R ) -> ( Base ` S ) C_ ( Base ` R ) )
11 10 adantr 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. U ) -> ( Base ` S ) C_ ( Base ` R ) )
12 1 subrgring 
 |-  ( A e. ( SubRing ` R ) -> S e. Ring )
13 eqid 
 |-  ( Base ` S ) = ( Base ` S )
14 3 4 13 ringinvcl 
 |-  ( ( S e. Ring /\ X e. U ) -> ( J ` X ) e. ( Base ` S ) )
15 12 14 sylan 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. U ) -> ( J ` X ) e. ( Base ` S ) )
16 11 15 sseldd 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. U ) -> ( J ` X ) e. ( Base ` R ) )
17 13 3 unitcl 
 |-  ( X e. U -> X e. ( Base ` S ) )
18 17 adantl 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. U ) -> X e. ( Base ` S ) )
19 11 18 sseldd 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. U ) -> X e. ( Base ` R ) )
20 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
21 1 20 3 subrguss 
 |-  ( A e. ( SubRing ` R ) -> U C_ ( Unit ` R ) )
22 21 sselda 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. U ) -> X e. ( Unit ` R ) )
23 20 2 8 ringinvcl 
 |-  ( ( R e. Ring /\ X e. ( Unit ` R ) ) -> ( I ` X ) e. ( Base ` R ) )
24 5 22 23 syl2an2r 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. U ) -> ( I ` X ) e. ( Base ` R ) )
25 eqid 
 |-  ( .r ` R ) = ( .r ` R )
26 8 25 ringass 
 |-  ( ( R e. Ring /\ ( ( J ` X ) e. ( Base ` R ) /\ X e. ( Base ` R ) /\ ( I ` X ) e. ( Base ` R ) ) ) -> ( ( ( J ` X ) ( .r ` R ) X ) ( .r ` R ) ( I ` X ) ) = ( ( J ` X ) ( .r ` R ) ( X ( .r ` R ) ( I ` X ) ) ) )
27 6 16 19 24 26 syl13anc 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. U ) -> ( ( ( J ` X ) ( .r ` R ) X ) ( .r ` R ) ( I ` X ) ) = ( ( J ` X ) ( .r ` R ) ( X ( .r ` R ) ( I ` X ) ) ) )
28 eqid 
 |-  ( .r ` S ) = ( .r ` S )
29 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
30 3 4 28 29 unitlinv 
 |-  ( ( S e. Ring /\ X e. U ) -> ( ( J ` X ) ( .r ` S ) X ) = ( 1r ` S ) )
31 12 30 sylan 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. U ) -> ( ( J ` X ) ( .r ` S ) X ) = ( 1r ` S ) )
32 1 25 ressmulr 
 |-  ( A e. ( SubRing ` R ) -> ( .r ` R ) = ( .r ` S ) )
33 32 adantr 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. U ) -> ( .r ` R ) = ( .r ` S ) )
34 33 oveqd 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. U ) -> ( ( J ` X ) ( .r ` R ) X ) = ( ( J ` X ) ( .r ` S ) X ) )
35 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
36 1 35 subrg1 
 |-  ( A e. ( SubRing ` R ) -> ( 1r ` R ) = ( 1r ` S ) )
37 36 adantr 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. U ) -> ( 1r ` R ) = ( 1r ` S ) )
38 31 34 37 3eqtr4d 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. U ) -> ( ( J ` X ) ( .r ` R ) X ) = ( 1r ` R ) )
39 38 oveq1d 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. U ) -> ( ( ( J ` X ) ( .r ` R ) X ) ( .r ` R ) ( I ` X ) ) = ( ( 1r ` R ) ( .r ` R ) ( I ` X ) ) )
40 20 2 25 35 unitrinv 
 |-  ( ( R e. Ring /\ X e. ( Unit ` R ) ) -> ( X ( .r ` R ) ( I ` X ) ) = ( 1r ` R ) )
41 5 22 40 syl2an2r 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. U ) -> ( X ( .r ` R ) ( I ` X ) ) = ( 1r ` R ) )
42 41 oveq2d 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. U ) -> ( ( J ` X ) ( .r ` R ) ( X ( .r ` R ) ( I ` X ) ) ) = ( ( J ` X ) ( .r ` R ) ( 1r ` R ) ) )
43 27 39 42 3eqtr3d 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. U ) -> ( ( 1r ` R ) ( .r ` R ) ( I ` X ) ) = ( ( J ` X ) ( .r ` R ) ( 1r ` R ) ) )
44 8 25 35 ringlidm 
 |-  ( ( R e. Ring /\ ( I ` X ) e. ( Base ` R ) ) -> ( ( 1r ` R ) ( .r ` R ) ( I ` X ) ) = ( I ` X ) )
45 5 24 44 syl2an2r 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. U ) -> ( ( 1r ` R ) ( .r ` R ) ( I ` X ) ) = ( I ` X ) )
46 8 25 35 ringridm 
 |-  ( ( R e. Ring /\ ( J ` X ) e. ( Base ` R ) ) -> ( ( J ` X ) ( .r ` R ) ( 1r ` R ) ) = ( J ` X ) )
47 5 16 46 syl2an2r 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. U ) -> ( ( J ` X ) ( .r ` R ) ( 1r ` R ) ) = ( J ` X ) )
48 43 45 47 3eqtr3d 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. U ) -> ( I ` X ) = ( J ` X ) )