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

Metamath Proof Explorer

Theorem subrgugrp

Description: The units of a subring form a subgroup of the unit group of the original ring. (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 )
subrgugrp.4 
|- G = ( ( mulGrp ` R ) |`s U )
Assertion subrgugrp 
|- ( A e. ( SubRing ` R ) -> V e. ( SubGrp ` G ) )

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 subrgugrp.4 
 |-  G = ( ( mulGrp ` R ) |`s U )
5 1 2 3 subrguss 
 |-  ( A e. ( SubRing ` R ) -> V C_ U )
6 1 subrgring 
 |-  ( A e. ( SubRing ` R ) -> S e. Ring )
7 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
8 3 7 1unit 
 |-  ( S e. Ring -> ( 1r ` S ) e. V )
9 ne0i 
 |-  ( ( 1r ` S ) e. V -> V =/= (/) )
10 6 8 9 3syl 
 |-  ( A e. ( SubRing ` R ) -> V =/= (/) )
11 eqid 
 |-  ( .r ` R ) = ( .r ` R )
12 1 11 ressmulr 
 |-  ( A e. ( SubRing ` R ) -> ( .r ` R ) = ( .r ` S ) )
13 12 3ad2ant1 
 |-  ( ( A e. ( SubRing ` R ) /\ x e. V /\ y e. V ) -> ( .r ` R ) = ( .r ` S ) )
14 13 oveqd 
 |-  ( ( A e. ( SubRing ` R ) /\ x e. V /\ y e. V ) -> ( x ( .r ` R ) y ) = ( x ( .r ` S ) y ) )
15 eqid 
 |-  ( .r ` S ) = ( .r ` S )
16 3 15 unitmulcl 
 |-  ( ( S e. Ring /\ x e. V /\ y e. V ) -> ( x ( .r ` S ) y ) e. V )
17 6 16 syl3an1 
 |-  ( ( A e. ( SubRing ` R ) /\ x e. V /\ y e. V ) -> ( x ( .r ` S ) y ) e. V )
18 14 17 eqeltrd 
 |-  ( ( A e. ( SubRing ` R ) /\ x e. V /\ y e. V ) -> ( x ( .r ` R ) y ) e. V )
19 18 3expa 
 |-  ( ( ( A e. ( SubRing ` R ) /\ x e. V ) /\ y e. V ) -> ( x ( .r ` R ) y ) e. V )
20 19 ralrimiva 
 |-  ( ( A e. ( SubRing ` R ) /\ x e. V ) -> A. y e. V ( x ( .r ` R ) y ) e. V )
21 eqid 
 |-  ( invr ` R ) = ( invr ` R )
22 eqid 
 |-  ( invr ` S ) = ( invr ` S )
23 1 21 3 22 subrginv 
 |-  ( ( A e. ( SubRing ` R ) /\ x e. V ) -> ( ( invr ` R ) ` x ) = ( ( invr ` S ) ` x ) )
24 3 22 unitinvcl 
 |-  ( ( S e. Ring /\ x e. V ) -> ( ( invr ` S ) ` x ) e. V )
25 6 24 sylan 
 |-  ( ( A e. ( SubRing ` R ) /\ x e. V ) -> ( ( invr ` S ) ` x ) e. V )
26 23 25 eqeltrd 
 |-  ( ( A e. ( SubRing ` R ) /\ x e. V ) -> ( ( invr ` R ) ` x ) e. V )
27 20 26 jca 
 |-  ( ( A e. ( SubRing ` R ) /\ x e. V ) -> ( A. y e. V ( x ( .r ` R ) y ) e. V /\ ( ( invr ` R ) ` x ) e. V ) )
28 27 ralrimiva 
 |-  ( A e. ( SubRing ` R ) -> A. x e. V ( A. y e. V ( x ( .r ` R ) y ) e. V /\ ( ( invr ` R ) ` x ) e. V ) )
29 subrgrcl 
 |-  ( A e. ( SubRing ` R ) -> R e. Ring )
30 2 4 unitgrp 
 |-  ( R e. Ring -> G e. Grp )
31 2 4 unitgrpbas 
 |-  U = ( Base ` G )
32 2 fvexi 
 |-  U e. _V
33 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
34 33 11 mgpplusg 
 |-  ( .r ` R ) = ( +g ` ( mulGrp ` R ) )
35 4 34 ressplusg 
 |-  ( U e. _V -> ( .r ` R ) = ( +g ` G ) )
36 32 35 ax-mp 
 |-  ( .r ` R ) = ( +g ` G )
37 2 4 21 invrfval 
 |-  ( invr ` R ) = ( invg ` G )
38 31 36 37 issubg2 
 |-  ( G e. Grp -> ( V e. ( SubGrp ` G ) <-> ( V C_ U /\ V =/= (/) /\ A. x e. V ( A. y e. V ( x ( .r ` R ) y ) e. V /\ ( ( invr ` R ) ` x ) e. V ) ) ) )
39 29 30 38 3syl 
 |-  ( A e. ( SubRing ` R ) -> ( V e. ( SubGrp ` G ) <-> ( V C_ U /\ V =/= (/) /\ A. x e. V ( A. y e. V ( x ( .r ` R ) y ) e. V /\ ( ( invr ` R ) ` x ) e. V ) ) ) )
40 5 10 28 39 mpbir3and 
 |-  ( A e. ( SubRing ` R ) -> V e. ( SubGrp ` G ) )