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=UnitR
unitgrp.2 G=mulGrpR𝑠U
Assertion unitgrp RRingGGrp

Proof

Step Hyp Ref Expression
1 unitmulcl.1 U=UnitR
2 unitgrp.2 G=mulGrpR𝑠U
3 1 2 unitgrpbas U=BaseG
4 3 a1i RRingU=BaseG
5 1 fvexi UV
6 eqid mulGrpR=mulGrpR
7 eqid R=R
8 6 7 mgpplusg R=+mulGrpR
9 2 8 ressplusg UVR=+G
10 5 9 mp1i RRingR=+G
11 1 7 unitmulcl RRingxUyUxRyU
12 eqid BaseR=BaseR
13 12 1 unitcl xUxBaseR
14 12 1 unitcl yUyBaseR
15 12 1 unitcl zUzBaseR
16 13 14 15 3anim123i xUyUzUxBaseRyBaseRzBaseR
17 12 7 ringass RRingxBaseRyBaseRzBaseRxRyRz=xRyRz
18 16 17 sylan2 RRingxUyUzUxRyRz=xRyRz
19 eqid 1R=1R
20 1 19 1unit RRing1RU
21 12 7 19 ringlidm RRingxBaseR1RRx=x
22 13 21 sylan2 RRingxU1RRx=x
23 simpr RRingxUxU
24 eqid rR=rR
25 eqid opprR=opprR
26 eqid ropprR=ropprR
27 1 19 24 25 26 isunit xUxrR1RxropprR1R
28 23 27 sylib RRingxUxrR1RxropprR1R
29 13 adantl RRingxUxBaseR
30 12 24 7 dvdsr2 xBaseRxrR1RyBaseRyRx=1R
31 29 30 syl RRingxUxrR1RyBaseRyRx=1R
32 25 12 opprbas BaseR=BaseopprR
33 eqid opprR=opprR
34 32 26 33 dvdsr2 xBaseRxropprR1RmBaseRmopprRx=1R
35 29 34 syl RRingxUxropprR1RmBaseRmopprRx=1R
36 31 35 anbi12d RRingxUxrR1RxropprR1RyBaseRyRx=1RmBaseRmopprRx=1R
37 reeanv yBaseRmBaseRyRx=1RmopprRx=1RyBaseRyRx=1RmBaseRmopprRx=1R
38 simprl RRingxUyBaseRmBaseRyRx=1RmopprRx=1RmBaseR
39 29 ad2antrr RRingxUyBaseRmBaseRyRx=1RmopprRx=1RxBaseR
40 12 24 7 dvdsrmul mBaseRxBaseRmrRxRm
41 38 39 40 syl2anc RRingxUyBaseRmBaseRyRx=1RmopprRx=1RmrRxRm
42 simplll RRingxUyBaseRmBaseRyRx=1RmopprRx=1RRRing
43 simplr RRingxUyBaseRmBaseRyRx=1RmopprRx=1RyBaseR
44 12 7 ringass RRingyBaseRxBaseRmBaseRyRxRm=yRxRm
45 42 43 39 38 44 syl13anc RRingxUyBaseRmBaseRyRx=1RmopprRx=1RyRxRm=yRxRm
46 simprrl RRingxUyBaseRmBaseRyRx=1RmopprRx=1RyRx=1R
47 46 oveq1d RRingxUyBaseRmBaseRyRx=1RmopprRx=1RyRxRm=1RRm
48 12 7 25 33 opprmul mopprRx=xRm
49 simprrr RRingxUyBaseRmBaseRyRx=1RmopprRx=1RmopprRx=1R
50 48 49 eqtr3id RRingxUyBaseRmBaseRyRx=1RmopprRx=1RxRm=1R
51 50 oveq2d RRingxUyBaseRmBaseRyRx=1RmopprRx=1RyRxRm=yR1R
52 45 47 51 3eqtr3d RRingxUyBaseRmBaseRyRx=1RmopprRx=1R1RRm=yR1R
53 12 7 19 ringlidm RRingmBaseR1RRm=m
54 42 38 53 syl2anc RRingxUyBaseRmBaseRyRx=1RmopprRx=1R1RRm=m
55 12 7 19 ringridm RRingyBaseRyR1R=y
56 42 43 55 syl2anc RRingxUyBaseRmBaseRyRx=1RmopprRx=1RyR1R=y
57 52 54 56 3eqtr3d RRingxUyBaseRmBaseRyRx=1RmopprRx=1Rm=y
58 41 57 50 3brtr3d RRingxUyBaseRmBaseRyRx=1RmopprRx=1RyrR1R
59 32 26 33 dvdsrmul yBaseRxBaseRyropprRxopprRy
60 43 39 59 syl2anc RRingxUyBaseRmBaseRyRx=1RmopprRx=1RyropprRxopprRy
61 12 7 25 33 opprmul xopprRy=yRx
62 61 46 eqtrid RRingxUyBaseRmBaseRyRx=1RmopprRx=1RxopprRy=1R
63 60 62 breqtrd RRingxUyBaseRmBaseRyRx=1RmopprRx=1RyropprR1R
64 1 19 24 25 26 isunit yUyrR1RyropprR1R
65 58 63 64 sylanbrc RRingxUyBaseRmBaseRyRx=1RmopprRx=1RyU
66 65 46 jca RRingxUyBaseRmBaseRyRx=1RmopprRx=1RyUyRx=1R
67 66 rexlimdvaa RRingxUyBaseRmBaseRyRx=1RmopprRx=1RyUyRx=1R
68 67 expimpd RRingxUyBaseRmBaseRyRx=1RmopprRx=1RyUyRx=1R
69 68 reximdv2 RRingxUyBaseRmBaseRyRx=1RmopprRx=1RyUyRx=1R
70 37 69 biimtrrid RRingxUyBaseRyRx=1RmBaseRmopprRx=1RyUyRx=1R
71 36 70 sylbid RRingxUxrR1RxropprR1RyUyRx=1R
72 28 71 mpd RRingxUyUyRx=1R
73 4 10 11 18 20 22 72 isgrpde RRingGGrp