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 simpr 
 |-  ( ( R e. Ring /\ x e. U ) -> x e. U )
24 eqid 
 |-  ( ||r ` R ) = ( ||r ` R )
25 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
26 eqid 
 |-  ( ||r ` ( oppR ` R ) ) = ( ||r ` ( oppR ` R ) )
27 1 19 24 25 26 isunit 
 |-  ( x e. U <-> ( x ( ||r ` R ) ( 1r ` R ) /\ x ( ||r ` ( oppR ` R ) ) ( 1r ` R ) ) )
28 23 27 sylib 
 |-  ( ( R e. Ring /\ x e. U ) -> ( x ( ||r ` R ) ( 1r ` R ) /\ x ( ||r ` ( oppR ` R ) ) ( 1r ` R ) ) )
29 13 adantl 
 |-  ( ( R e. Ring /\ x e. U ) -> x e. ( Base ` R ) )
30 12 24 7 dvdsr2 
 |-  ( x e. ( Base ` R ) -> ( x ( ||r ` R ) ( 1r ` R ) <-> E. y e. ( Base ` R ) ( y ( .r ` R ) x ) = ( 1r ` R ) ) )
31 29 30 syl 
 |-  ( ( R e. Ring /\ x e. U ) -> ( x ( ||r ` R ) ( 1r ` R ) <-> E. y e. ( Base ` R ) ( y ( .r ` R ) x ) = ( 1r ` R ) ) )
32 25 12 opprbas 
 |-  ( Base ` R ) = ( Base ` ( oppR ` R ) )
33 eqid 
 |-  ( .r ` ( oppR ` R ) ) = ( .r ` ( oppR ` R ) )
34 32 26 33 dvdsr2 
 |-  ( x e. ( Base ` R ) -> ( x ( ||r ` ( oppR ` R ) ) ( 1r ` R ) <-> E. m e. ( Base ` R ) ( m ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) ) )
35 29 34 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 ) ) )
36 31 35 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 ) ) ) )
37 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 ) ) )
38 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 ) )
39 29 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 ) )
40 12 24 7 dvdsrmul 
 |-  ( ( m e. ( Base ` R ) /\ x e. ( Base ` R ) ) -> m ( ||r ` R ) ( x ( .r ` R ) m ) )
41 38 39 40 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 ) )
42 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 )
43 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 ) )
44 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 ) ) )
45 42 43 39 38 44 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 ) ) )
46 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 ) )
47 46 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 ) )
48 12 7 25 33 opprmul 
 |-  ( m ( .r ` ( oppR ` R ) ) x ) = ( x ( .r ` R ) m )
49 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 ) )
50 48 49 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 ) )
51 50 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 ) ) )
52 45 47 51 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 ) ) )
53 12 7 19 ringlidm 
 |-  ( ( R e. Ring /\ m e. ( Base ` R ) ) -> ( ( 1r ` R ) ( .r ` R ) m ) = m )
54 42 38 53 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 )
55 12 7 19 ringridm 
 |-  ( ( R e. Ring /\ y e. ( Base ` R ) ) -> ( y ( .r ` R ) ( 1r ` R ) ) = y )
56 42 43 55 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 )
57 52 54 56 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 )
58 41 57 50 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 ) )
59 32 26 33 dvdsrmul 
 |-  ( ( y e. ( Base ` R ) /\ x e. ( Base ` R ) ) -> y ( ||r ` ( oppR ` R ) ) ( x ( .r ` ( oppR ` R ) ) y ) )
60 43 39 59 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 ) )
61 12 7 25 33 opprmul 
 |-  ( x ( .r ` ( oppR ` R ) ) y ) = ( y ( .r ` R ) x )
62 61 46 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 ) )
63 60 62 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 ) )
64 1 19 24 25 26 isunit 
 |-  ( y e. U <-> ( y ( ||r ` R ) ( 1r ` R ) /\ y ( ||r ` ( oppR ` R ) ) ( 1r ` R ) ) )
65 58 63 64 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 )
66 65 46 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 ) ) )
67 66 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 ) ) ) )
68 67 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 ) ) ) )
69 68 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 ) ) )
70 37 69 syl5bir 
 |-  ( ( 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 ) ) )
71 36 70 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 ) ) )
72 28 71 mpd 
 |-  ( ( R e. Ring /\ x e. U ) -> E. y e. U ( y ( .r ` R ) x ) = ( 1r ` R ) )
73 4 10 11 18 20 22 72 isgrpde 
 |-  ( R e. Ring -> G e. Grp )