Metamath Proof Explorer

Theorem unitgrp

Description: The group of units is a group under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014)

Ref Expression
Hypotheses unitmulcl.1 
|- U = ( Unit ` R )
unitgrp.2 
|- G = ( ( mulGrp ` R ) |`s U )
Assertion unitgrp 
|- ( R e. Ring -> G e. Grp )

Proof

Step Hyp Ref Expression
1 unitmulcl.1 
 |-  U = ( Unit ` R )
2 unitgrp.2 
 |-  G = ( ( mulGrp ` R ) |`s U )
3 1 2 unitgrpbas 
 |-  U = ( Base ` G )
4 3 a1i 
 |-  ( R e. Ring -> U = ( Base ` G ) )
5 1 fvexi 
 |-  U e. _V
6 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
7 eqid 
 |-  ( .r ` R ) = ( .r ` R )
8 6 7 mgpplusg 
 |-  ( .r ` R ) = ( +g ` ( mulGrp ` R ) )
9 2 8 ressplusg 
 |-  ( U e. _V -> ( .r ` R ) = ( +g ` G ) )
10 5 9 mp1i 
 |-  ( R e. Ring -> ( .r ` R ) = ( +g ` G ) )
11 1 7 unitmulcl 
 |-  ( ( R e. Ring /\ x e. U /\ y e. U ) -> ( x ( .r ` R ) y ) e. U )
12 eqid 
 |-  ( Base ` R ) = ( Base ` R )
13 12 1 unitcl 
 |-  ( x e. U -> x e. ( Base ` R ) )
14 12 1 unitcl 
 |-  ( y e. U -> y e. ( Base ` R ) )
15 12 1 unitcl 
 |-  ( z e. U -> z e. ( Base ` R ) )
16 13 14 15 3anim123i 
 |-  ( ( x e. U /\ y e. U /\ z e. U ) -> ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) )
17 12 7 ringass 
 |-  ( ( R e. Ring /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> ( ( x ( .r ` R ) y ) ( .r ` R ) z ) = ( x ( .r ` R ) ( y ( .r ` R ) z ) ) )
18 16 17 sylan2 
 |-  ( ( R e. Ring /\ ( x e. U /\ y e. U /\ z e. U ) ) -> ( ( x ( .r ` R ) y ) ( .r ` R ) z ) = ( x ( .r ` R ) ( y ( .r ` R ) z ) ) )
19 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
20 1 19 1unit 
 |-  ( R e. Ring -> ( 1r ` R ) e. U )
21 12 7 19 ringlidm 
 |-  ( ( R e. Ring /\ x e. ( Base ` R ) ) -> ( ( 1r ` R ) ( .r ` R ) x ) = x )
22 13 21 sylan2 
 |-  ( ( R e. Ring /\ x e. U ) -> ( ( 1r ` R ) ( .r ` R ) x ) = x )
23 eqid 
 |-  ( ||r ` R ) = ( ||r ` R )
24 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
25 eqid 
 |-  ( ||r ` ( oppR ` R ) ) = ( ||r ` ( oppR ` R ) )
26 1 19 23 24 25 isunit 
 |-  ( x e. U <-> ( x ( ||r ` R ) ( 1r ` R ) /\ x ( ||r ` ( oppR ` R ) ) ( 1r ` R ) ) )
27 26 bilani 
 |-  ( ( R e. Ring /\ x e. U ) -> ( x ( ||r ` R ) ( 1r ` R ) /\ x ( ||r ` ( oppR ` R ) ) ( 1r ` R ) ) )
28 13 adantl 
 |-  ( ( R e. Ring /\ x e. U ) -> x e. ( Base ` R ) )
29 12 23 7 dvdsr2 
 |-  ( x e. ( Base ` R ) -> ( x ( ||r ` R ) ( 1r ` R ) <-> E. y e. ( Base ` R ) ( y ( .r ` R ) x ) = ( 1r ` R ) ) )
30 28 29 syl 
 |-  ( ( R e. Ring /\ x e. U ) -> ( x ( ||r ` R ) ( 1r ` R ) <-> E. y e. ( Base ` R ) ( y ( .r ` R ) x ) = ( 1r ` R ) ) )
31 24 12 opprbas 
 |-  ( Base ` R ) = ( Base ` ( oppR ` R ) )
32 eqid 
 |-  ( .r ` ( oppR ` R ) ) = ( .r ` ( oppR ` R ) )
33 31 25 32 dvdsr2 
 |-  ( x e. ( Base ` R ) -> ( x ( ||r ` ( oppR ` R ) ) ( 1r ` R ) <-> E. m e. ( Base ` R ) ( m ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) ) )
34 28 33 syl 
 |-  ( ( R e. Ring /\ x e. U ) -> ( x ( ||r ` ( oppR ` R ) ) ( 1r ` R ) <-> E. m e. ( Base ` R ) ( m ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) ) )
35 30 34 anbi12d 
 |-  ( ( R e. Ring /\ x e. U ) -> ( ( x ( ||r ` R ) ( 1r ` R ) /\ x ( ||r ` ( oppR ` R ) ) ( 1r ` R ) ) <-> ( E. y e. ( Base ` R ) ( y ( .r ` R ) x ) = ( 1r ` R ) /\ E. m e. ( Base ` R ) ( m ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) ) ) )
36 reeanv 
 |-  ( E. y e. ( Base ` R ) E. m e. ( Base ` R ) ( ( y ( .r ` R ) x ) = ( 1r ` R ) /\ ( m ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) ) <-> ( E. y e. ( Base ` R ) ( y ( .r ` R ) x ) = ( 1r ` R ) /\ E. m e. ( Base ` R ) ( m ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) ) )
37 simprl 
 |-  ( ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) /\ ( m e. ( Base ` R ) /\ ( ( y ( .r ` R ) x ) = ( 1r ` R ) /\ ( m ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) ) ) ) -> m e. ( Base ` R ) )
38 28 ad2antrr 
 |-  ( ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) /\ ( m e. ( Base ` R ) /\ ( ( y ( .r ` R ) x ) = ( 1r ` R ) /\ ( m ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) ) ) ) -> x e. ( Base ` R ) )
39 12 23 7 dvdsrmul 
 |-  ( ( m e. ( Base ` R ) /\ x e. ( Base ` R ) ) -> m ( ||r ` R ) ( x ( .r ` R ) m ) )
40 37 38 39 syl2anc 
 |-  ( ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) /\ ( m e. ( Base ` R ) /\ ( ( y ( .r ` R ) x ) = ( 1r ` R ) /\ ( m ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) ) ) ) -> m ( ||r ` R ) ( x ( .r ` R ) m ) )
41 simplll 
 |-  ( ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) /\ ( m e. ( Base ` R ) /\ ( ( y ( .r ` R ) x ) = ( 1r ` R ) /\ ( m ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) ) ) ) -> R e. Ring )
42 simplr 
 |-  ( ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) /\ ( m e. ( Base ` R ) /\ ( ( y ( .r ` R ) x ) = ( 1r ` R ) /\ ( m ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) ) ) ) -> y e. ( Base ` R ) )
43 12 7 ringass 
 |-  ( ( R e. Ring /\ ( y e. ( Base ` R ) /\ x e. ( Base ` R ) /\ m e. ( Base ` R ) ) ) -> ( ( y ( .r ` R ) x ) ( .r ` R ) m ) = ( y ( .r ` R ) ( x ( .r ` R ) m ) ) )
44 41 42 38 37 43 syl13anc 
 |-  ( ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) /\ ( m e. ( Base ` R ) /\ ( ( y ( .r ` R ) x ) = ( 1r ` R ) /\ ( m ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) ) ) ) -> ( ( y ( .r ` R ) x ) ( .r ` R ) m ) = ( y ( .r ` R ) ( x ( .r ` R ) m ) ) )
45 simprrl 
 |-  ( ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) /\ ( m e. ( Base ` R ) /\ ( ( y ( .r ` R ) x ) = ( 1r ` R ) /\ ( m ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) ) ) ) -> ( y ( .r ` R ) x ) = ( 1r ` R ) )
46 45 oveq1d 
 |-  ( ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) /\ ( m e. ( Base ` R ) /\ ( ( y ( .r ` R ) x ) = ( 1r ` R ) /\ ( m ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) ) ) ) -> ( ( y ( .r ` R ) x ) ( .r ` R ) m ) = ( ( 1r ` R ) ( .r ` R ) m ) )
47 12 7 24 32 opprmul 
 |-  ( m ( .r ` ( oppR ` R ) ) x ) = ( x ( .r ` R ) m )
48 simprrr 
 |-  ( ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) /\ ( m e. ( Base ` R ) /\ ( ( y ( .r ` R ) x ) = ( 1r ` R ) /\ ( m ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) ) ) ) -> ( m ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) )
49 47 48 eqtr3id 
 |-  ( ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) /\ ( m e. ( Base ` R ) /\ ( ( y ( .r ` R ) x ) = ( 1r ` R ) /\ ( m ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) ) ) ) -> ( x ( .r ` R ) m ) = ( 1r ` R ) )
50 49 oveq2d 
 |-  ( ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) /\ ( m e. ( Base ` R ) /\ ( ( y ( .r ` R ) x ) = ( 1r ` R ) /\ ( m ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) ) ) ) -> ( y ( .r ` R ) ( x ( .r ` R ) m ) ) = ( y ( .r ` R ) ( 1r ` R ) ) )
51 44 46 50 3eqtr3d 
 |-  ( ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) /\ ( m e. ( Base ` R ) /\ ( ( y ( .r ` R ) x ) = ( 1r ` R ) /\ ( m ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) ) ) ) -> ( ( 1r ` R ) ( .r ` R ) m ) = ( y ( .r ` R ) ( 1r ` R ) ) )
52 12 7 19 ringlidm 
 |-  ( ( R e. Ring /\ m e. ( Base ` R ) ) -> ( ( 1r ` R ) ( .r ` R ) m ) = m )
53 41 37 52 syl2anc 
 |-  ( ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) /\ ( m e. ( Base ` R ) /\ ( ( y ( .r ` R ) x ) = ( 1r ` R ) /\ ( m ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) ) ) ) -> ( ( 1r ` R ) ( .r ` R ) m ) = m )
54 12 7 19 ringridm 
 |-  ( ( R e. Ring /\ y e. ( Base ` R ) ) -> ( y ( .r ` R ) ( 1r ` R ) ) = y )
55 41 42 54 syl2anc 
 |-  ( ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) /\ ( m e. ( Base ` R ) /\ ( ( y ( .r ` R ) x ) = ( 1r ` R ) /\ ( m ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) ) ) ) -> ( y ( .r ` R ) ( 1r ` R ) ) = y )
56 51 53 55 3eqtr3d 
 |-  ( ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) /\ ( m e. ( Base ` R ) /\ ( ( y ( .r ` R ) x ) = ( 1r ` R ) /\ ( m ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) ) ) ) -> m = y )
57 40 56 49 3brtr3d 
 |-  ( ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) /\ ( m e. ( Base ` R ) /\ ( ( y ( .r ` R ) x ) = ( 1r ` R ) /\ ( m ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) ) ) ) -> y ( ||r ` R ) ( 1r ` R ) )
58 31 25 32 dvdsrmul 
 |-  ( ( y e. ( Base ` R ) /\ x e. ( Base ` R ) ) -> y ( ||r ` ( oppR ` R ) ) ( x ( .r ` ( oppR ` R ) ) y ) )
59 42 38 58 syl2anc 
 |-  ( ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) /\ ( m e. ( Base ` R ) /\ ( ( y ( .r ` R ) x ) = ( 1r ` R ) /\ ( m ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) ) ) ) -> y ( ||r ` ( oppR ` R ) ) ( x ( .r ` ( oppR ` R ) ) y ) )
60 12 7 24 32 opprmul 
 |-  ( x ( .r ` ( oppR ` R ) ) y ) = ( y ( .r ` R ) x )
61 60 45 eqtrid 
 |-  ( ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) /\ ( m e. ( Base ` R ) /\ ( ( y ( .r ` R ) x ) = ( 1r ` R ) /\ ( m ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) ) ) ) -> ( x ( .r ` ( oppR ` R ) ) y ) = ( 1r ` R ) )
62 59 61 breqtrd 
 |-  ( ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) /\ ( m e. ( Base ` R ) /\ ( ( y ( .r ` R ) x ) = ( 1r ` R ) /\ ( m ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) ) ) ) -> y ( ||r ` ( oppR ` R ) ) ( 1r ` R ) )
63 1 19 23 24 25 isunit 
 |-  ( y e. U <-> ( y ( ||r ` R ) ( 1r ` R ) /\ y ( ||r ` ( oppR ` R ) ) ( 1r ` R ) ) )
64 57 62 63 sylanbrc 
 |-  ( ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) /\ ( m e. ( Base ` R ) /\ ( ( y ( .r ` R ) x ) = ( 1r ` R ) /\ ( m ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) ) ) ) -> y e. U )
65 64 45 jca 
 |-  ( ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) /\ ( m e. ( Base ` R ) /\ ( ( y ( .r ` R ) x ) = ( 1r ` R ) /\ ( m ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) ) ) ) -> ( y e. U /\ ( y ( .r ` R ) x ) = ( 1r ` R ) ) )
66 65 rexlimdvaa 
 |-  ( ( ( R e. Ring /\ x e. U ) /\ y e. ( Base ` R ) ) -> ( E. m e. ( Base ` R ) ( ( y ( .r ` R ) x ) = ( 1r ` R ) /\ ( m ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) ) -> ( y e. U /\ ( y ( .r ` R ) x ) = ( 1r ` R ) ) ) )
67 66 expimpd 
 |-  ( ( R e. Ring /\ x e. U ) -> ( ( y e. ( Base ` R ) /\ E. m e. ( Base ` R ) ( ( y ( .r ` R ) x ) = ( 1r ` R ) /\ ( m ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) ) ) -> ( y e. U /\ ( y ( .r ` R ) x ) = ( 1r ` R ) ) ) )
68 67 reximdv2 
 |-  ( ( R e. Ring /\ x e. U ) -> ( E. y e. ( Base ` R ) E. m e. ( Base ` R ) ( ( y ( .r ` R ) x ) = ( 1r ` R ) /\ ( m ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) ) -> E. y e. U ( y ( .r ` R ) x ) = ( 1r ` R ) ) )
69 36 68 biimtrrid 
 |-  ( ( R e. Ring /\ x e. U ) -> ( ( E. y e. ( Base ` R ) ( y ( .r ` R ) x ) = ( 1r ` R ) /\ E. m e. ( Base ` R ) ( m ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) ) -> E. y e. U ( y ( .r ` R ) x ) = ( 1r ` R ) ) )
70 35 69 sylbid 
 |-  ( ( R e. Ring /\ x e. U ) -> ( ( x ( ||r ` R ) ( 1r ` R ) /\ x ( ||r ` ( oppR ` R ) ) ( 1r ` R ) ) -> E. y e. U ( y ( .r ` R ) x ) = ( 1r ` R ) ) )
71 27 70 mpd 
 |-  ( ( R e. Ring /\ x e. U ) -> E. y e. U ( y ( .r ` R ) x ) = ( 1r ` R ) )
72 4 10 11 18 20 22 71 isgrpde 
 |-  ( R e. Ring -> G e. Grp )