# 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}=\mathrm{Unit}\left({R}\right)$
unitgrp.2 ${⊢}{G}={\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}{U}$
Assertion unitgrp ${⊢}{R}\in \mathrm{Ring}\to {G}\in \mathrm{Grp}$

### Proof

Step Hyp Ref Expression
1 unitmulcl.1 ${⊢}{U}=\mathrm{Unit}\left({R}\right)$
2 unitgrp.2 ${⊢}{G}={\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}{U}$
3 1 2 unitgrpbas ${⊢}{U}={\mathrm{Base}}_{{G}}$
4 3 a1i ${⊢}{R}\in \mathrm{Ring}\to {U}={\mathrm{Base}}_{{G}}$
5 1 fvexi ${⊢}{U}\in \mathrm{V}$
6 eqid ${⊢}{\mathrm{mulGrp}}_{{R}}={\mathrm{mulGrp}}_{{R}}$
7 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
8 6 7 mgpplusg ${⊢}{\cdot }_{{R}}={+}_{{\mathrm{mulGrp}}_{{R}}}$
9 2 8 ressplusg ${⊢}{U}\in \mathrm{V}\to {\cdot }_{{R}}={+}_{{G}}$
10 5 9 mp1i ${⊢}{R}\in \mathrm{Ring}\to {\cdot }_{{R}}={+}_{{G}}$
11 1 7 unitmulcl ${⊢}\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\wedge {y}\in {U}\right)\to {x}{\cdot }_{{R}}{y}\in {U}$
12 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
13 12 1 unitcl ${⊢}{x}\in {U}\to {x}\in {\mathrm{Base}}_{{R}}$
14 12 1 unitcl ${⊢}{y}\in {U}\to {y}\in {\mathrm{Base}}_{{R}}$
15 12 1 unitcl ${⊢}{z}\in {U}\to {z}\in {\mathrm{Base}}_{{R}}$
16 13 14 15 3anim123i ${⊢}\left({x}\in {U}\wedge {y}\in {U}\wedge {z}\in {U}\right)\to \left({x}\in {\mathrm{Base}}_{{R}}\wedge {y}\in {\mathrm{Base}}_{{R}}\wedge {z}\in {\mathrm{Base}}_{{R}}\right)$
17 12 7 ringass ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({x}\in {\mathrm{Base}}_{{R}}\wedge {y}\in {\mathrm{Base}}_{{R}}\wedge {z}\in {\mathrm{Base}}_{{R}}\right)\right)\to \left({x}{\cdot }_{{R}}{y}\right){\cdot }_{{R}}{z}={x}{\cdot }_{{R}}\left({y}{\cdot }_{{R}}{z}\right)$
18 16 17 sylan2 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({x}\in {U}\wedge {y}\in {U}\wedge {z}\in {U}\right)\right)\to \left({x}{\cdot }_{{R}}{y}\right){\cdot }_{{R}}{z}={x}{\cdot }_{{R}}\left({y}{\cdot }_{{R}}{z}\right)$
19 eqid ${⊢}{1}_{{R}}={1}_{{R}}$
20 1 19 1unit ${⊢}{R}\in \mathrm{Ring}\to {1}_{{R}}\in {U}$
21 12 7 19 ringlidm ${⊢}\left({R}\in \mathrm{Ring}\wedge {x}\in {\mathrm{Base}}_{{R}}\right)\to {1}_{{R}}{\cdot }_{{R}}{x}={x}$
22 13 21 sylan2 ${⊢}\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\to {1}_{{R}}{\cdot }_{{R}}{x}={x}$
23 simpr ${⊢}\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\to {x}\in {U}$
24 eqid ${⊢}{\parallel }_{r}\left({R}\right)={\parallel }_{r}\left({R}\right)$
25 eqid ${⊢}{opp}_{r}\left({R}\right)={opp}_{r}\left({R}\right)$
26 eqid ${⊢}{\parallel }_{r}\left({opp}_{r}\left({R}\right)\right)={\parallel }_{r}\left({opp}_{r}\left({R}\right)\right)$
27 1 19 24 25 26 isunit ${⊢}{x}\in {U}↔\left({x}{\parallel }_{r}\left({R}\right){1}_{{R}}\wedge {x}{\parallel }_{r}\left({opp}_{r}\left({R}\right)\right){1}_{{R}}\right)$
28 23 27 sylib ${⊢}\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\to \left({x}{\parallel }_{r}\left({R}\right){1}_{{R}}\wedge {x}{\parallel }_{r}\left({opp}_{r}\left({R}\right)\right){1}_{{R}}\right)$
29 13 adantl ${⊢}\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\to {x}\in {\mathrm{Base}}_{{R}}$
30 12 24 7 dvdsr2 ${⊢}{x}\in {\mathrm{Base}}_{{R}}\to \left({x}{\parallel }_{r}\left({R}\right){1}_{{R}}↔\exists {y}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{{R}}{x}={1}_{{R}}\right)$
31 29 30 syl ${⊢}\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\to \left({x}{\parallel }_{r}\left({R}\right){1}_{{R}}↔\exists {y}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{{R}}{x}={1}_{{R}}\right)$
32 25 12 opprbas ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{opp}_{r}\left({R}\right)}$
33 eqid ${⊢}{\cdot }_{{opp}_{r}\left({R}\right)}={\cdot }_{{opp}_{r}\left({R}\right)}$
34 32 26 33 dvdsr2 ${⊢}{x}\in {\mathrm{Base}}_{{R}}\to \left({x}{\parallel }_{r}\left({opp}_{r}\left({R}\right)\right){1}_{{R}}↔\exists {m}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}{m}{\cdot }_{{opp}_{r}\left({R}\right)}{x}={1}_{{R}}\right)$
35 29 34 syl ${⊢}\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\to \left({x}{\parallel }_{r}\left({opp}_{r}\left({R}\right)\right){1}_{{R}}↔\exists {m}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}{m}{\cdot }_{{opp}_{r}\left({R}\right)}{x}={1}_{{R}}\right)$
36 31 35 anbi12d ${⊢}\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\to \left(\left({x}{\parallel }_{r}\left({R}\right){1}_{{R}}\wedge {x}{\parallel }_{r}\left({opp}_{r}\left({R}\right)\right){1}_{{R}}\right)↔\left(\exists {y}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{{R}}{x}={1}_{{R}}\wedge \exists {m}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}{m}{\cdot }_{{opp}_{r}\left({R}\right)}{x}={1}_{{R}}\right)\right)$
37 reeanv ${⊢}\exists {y}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\exists {m}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\left({y}{\cdot }_{{R}}{x}={1}_{{R}}\wedge {m}{\cdot }_{{opp}_{r}\left({R}\right)}{x}={1}_{{R}}\right)↔\left(\exists {y}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{{R}}{x}={1}_{{R}}\wedge \exists {m}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}{m}{\cdot }_{{opp}_{r}\left({R}\right)}{x}={1}_{{R}}\right)$
38 simprl ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\wedge {y}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({m}\in {\mathrm{Base}}_{{R}}\wedge \left({y}{\cdot }_{{R}}{x}={1}_{{R}}\wedge {m}{\cdot }_{{opp}_{r}\left({R}\right)}{x}={1}_{{R}}\right)\right)\right)\to {m}\in {\mathrm{Base}}_{{R}}$
39 29 ad2antrr ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\wedge {y}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({m}\in {\mathrm{Base}}_{{R}}\wedge \left({y}{\cdot }_{{R}}{x}={1}_{{R}}\wedge {m}{\cdot }_{{opp}_{r}\left({R}\right)}{x}={1}_{{R}}\right)\right)\right)\to {x}\in {\mathrm{Base}}_{{R}}$
40 12 24 7 dvdsrmul ${⊢}\left({m}\in {\mathrm{Base}}_{{R}}\wedge {x}\in {\mathrm{Base}}_{{R}}\right)\to {m}{\parallel }_{r}\left({R}\right)\left({x}{\cdot }_{{R}}{m}\right)$
41 38 39 40 syl2anc ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\wedge {y}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({m}\in {\mathrm{Base}}_{{R}}\wedge \left({y}{\cdot }_{{R}}{x}={1}_{{R}}\wedge {m}{\cdot }_{{opp}_{r}\left({R}\right)}{x}={1}_{{R}}\right)\right)\right)\to {m}{\parallel }_{r}\left({R}\right)\left({x}{\cdot }_{{R}}{m}\right)$
42 simplll ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\wedge {y}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({m}\in {\mathrm{Base}}_{{R}}\wedge \left({y}{\cdot }_{{R}}{x}={1}_{{R}}\wedge {m}{\cdot }_{{opp}_{r}\left({R}\right)}{x}={1}_{{R}}\right)\right)\right)\to {R}\in \mathrm{Ring}$
43 simplr ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\wedge {y}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({m}\in {\mathrm{Base}}_{{R}}\wedge \left({y}{\cdot }_{{R}}{x}={1}_{{R}}\wedge {m}{\cdot }_{{opp}_{r}\left({R}\right)}{x}={1}_{{R}}\right)\right)\right)\to {y}\in {\mathrm{Base}}_{{R}}$
44 12 7 ringass ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({y}\in {\mathrm{Base}}_{{R}}\wedge {x}\in {\mathrm{Base}}_{{R}}\wedge {m}\in {\mathrm{Base}}_{{R}}\right)\right)\to \left({y}{\cdot }_{{R}}{x}\right){\cdot }_{{R}}{m}={y}{\cdot }_{{R}}\left({x}{\cdot }_{{R}}{m}\right)$
45 42 43 39 38 44 syl13anc ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\wedge {y}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({m}\in {\mathrm{Base}}_{{R}}\wedge \left({y}{\cdot }_{{R}}{x}={1}_{{R}}\wedge {m}{\cdot }_{{opp}_{r}\left({R}\right)}{x}={1}_{{R}}\right)\right)\right)\to \left({y}{\cdot }_{{R}}{x}\right){\cdot }_{{R}}{m}={y}{\cdot }_{{R}}\left({x}{\cdot }_{{R}}{m}\right)$
46 simprrl ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\wedge {y}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({m}\in {\mathrm{Base}}_{{R}}\wedge \left({y}{\cdot }_{{R}}{x}={1}_{{R}}\wedge {m}{\cdot }_{{opp}_{r}\left({R}\right)}{x}={1}_{{R}}\right)\right)\right)\to {y}{\cdot }_{{R}}{x}={1}_{{R}}$
47 46 oveq1d ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\wedge {y}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({m}\in {\mathrm{Base}}_{{R}}\wedge \left({y}{\cdot }_{{R}}{x}={1}_{{R}}\wedge {m}{\cdot }_{{opp}_{r}\left({R}\right)}{x}={1}_{{R}}\right)\right)\right)\to \left({y}{\cdot }_{{R}}{x}\right){\cdot }_{{R}}{m}={1}_{{R}}{\cdot }_{{R}}{m}$
48 12 7 25 33 opprmul ${⊢}{m}{\cdot }_{{opp}_{r}\left({R}\right)}{x}={x}{\cdot }_{{R}}{m}$
49 simprrr ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\wedge {y}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({m}\in {\mathrm{Base}}_{{R}}\wedge \left({y}{\cdot }_{{R}}{x}={1}_{{R}}\wedge {m}{\cdot }_{{opp}_{r}\left({R}\right)}{x}={1}_{{R}}\right)\right)\right)\to {m}{\cdot }_{{opp}_{r}\left({R}\right)}{x}={1}_{{R}}$
50 48 49 syl5eqr ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\wedge {y}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({m}\in {\mathrm{Base}}_{{R}}\wedge \left({y}{\cdot }_{{R}}{x}={1}_{{R}}\wedge {m}{\cdot }_{{opp}_{r}\left({R}\right)}{x}={1}_{{R}}\right)\right)\right)\to {x}{\cdot }_{{R}}{m}={1}_{{R}}$
51 50 oveq2d ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\wedge {y}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({m}\in {\mathrm{Base}}_{{R}}\wedge \left({y}{\cdot }_{{R}}{x}={1}_{{R}}\wedge {m}{\cdot }_{{opp}_{r}\left({R}\right)}{x}={1}_{{R}}\right)\right)\right)\to {y}{\cdot }_{{R}}\left({x}{\cdot }_{{R}}{m}\right)={y}{\cdot }_{{R}}{1}_{{R}}$
52 45 47 51 3eqtr3d ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\wedge {y}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({m}\in {\mathrm{Base}}_{{R}}\wedge \left({y}{\cdot }_{{R}}{x}={1}_{{R}}\wedge {m}{\cdot }_{{opp}_{r}\left({R}\right)}{x}={1}_{{R}}\right)\right)\right)\to {1}_{{R}}{\cdot }_{{R}}{m}={y}{\cdot }_{{R}}{1}_{{R}}$
53 12 7 19 ringlidm ${⊢}\left({R}\in \mathrm{Ring}\wedge {m}\in {\mathrm{Base}}_{{R}}\right)\to {1}_{{R}}{\cdot }_{{R}}{m}={m}$
54 42 38 53 syl2anc ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\wedge {y}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({m}\in {\mathrm{Base}}_{{R}}\wedge \left({y}{\cdot }_{{R}}{x}={1}_{{R}}\wedge {m}{\cdot }_{{opp}_{r}\left({R}\right)}{x}={1}_{{R}}\right)\right)\right)\to {1}_{{R}}{\cdot }_{{R}}{m}={m}$
55 12 7 19 ringridm ${⊢}\left({R}\in \mathrm{Ring}\wedge {y}\in {\mathrm{Base}}_{{R}}\right)\to {y}{\cdot }_{{R}}{1}_{{R}}={y}$
56 42 43 55 syl2anc ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\wedge {y}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({m}\in {\mathrm{Base}}_{{R}}\wedge \left({y}{\cdot }_{{R}}{x}={1}_{{R}}\wedge {m}{\cdot }_{{opp}_{r}\left({R}\right)}{x}={1}_{{R}}\right)\right)\right)\to {y}{\cdot }_{{R}}{1}_{{R}}={y}$
57 52 54 56 3eqtr3d ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\wedge {y}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({m}\in {\mathrm{Base}}_{{R}}\wedge \left({y}{\cdot }_{{R}}{x}={1}_{{R}}\wedge {m}{\cdot }_{{opp}_{r}\left({R}\right)}{x}={1}_{{R}}\right)\right)\right)\to {m}={y}$
58 41 57 50 3brtr3d ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\wedge {y}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({m}\in {\mathrm{Base}}_{{R}}\wedge \left({y}{\cdot }_{{R}}{x}={1}_{{R}}\wedge {m}{\cdot }_{{opp}_{r}\left({R}\right)}{x}={1}_{{R}}\right)\right)\right)\to {y}{\parallel }_{r}\left({R}\right){1}_{{R}}$
59 32 26 33 dvdsrmul ${⊢}\left({y}\in {\mathrm{Base}}_{{R}}\wedge {x}\in {\mathrm{Base}}_{{R}}\right)\to {y}{\parallel }_{r}\left({opp}_{r}\left({R}\right)\right)\left({x}{\cdot }_{{opp}_{r}\left({R}\right)}{y}\right)$
60 43 39 59 syl2anc ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\wedge {y}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({m}\in {\mathrm{Base}}_{{R}}\wedge \left({y}{\cdot }_{{R}}{x}={1}_{{R}}\wedge {m}{\cdot }_{{opp}_{r}\left({R}\right)}{x}={1}_{{R}}\right)\right)\right)\to {y}{\parallel }_{r}\left({opp}_{r}\left({R}\right)\right)\left({x}{\cdot }_{{opp}_{r}\left({R}\right)}{y}\right)$
61 12 7 25 33 opprmul ${⊢}{x}{\cdot }_{{opp}_{r}\left({R}\right)}{y}={y}{\cdot }_{{R}}{x}$
62 61 46 syl5eq ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\wedge {y}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({m}\in {\mathrm{Base}}_{{R}}\wedge \left({y}{\cdot }_{{R}}{x}={1}_{{R}}\wedge {m}{\cdot }_{{opp}_{r}\left({R}\right)}{x}={1}_{{R}}\right)\right)\right)\to {x}{\cdot }_{{opp}_{r}\left({R}\right)}{y}={1}_{{R}}$
63 60 62 breqtrd ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\wedge {y}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({m}\in {\mathrm{Base}}_{{R}}\wedge \left({y}{\cdot }_{{R}}{x}={1}_{{R}}\wedge {m}{\cdot }_{{opp}_{r}\left({R}\right)}{x}={1}_{{R}}\right)\right)\right)\to {y}{\parallel }_{r}\left({opp}_{r}\left({R}\right)\right){1}_{{R}}$
64 1 19 24 25 26 isunit ${⊢}{y}\in {U}↔\left({y}{\parallel }_{r}\left({R}\right){1}_{{R}}\wedge {y}{\parallel }_{r}\left({opp}_{r}\left({R}\right)\right){1}_{{R}}\right)$
65 58 63 64 sylanbrc ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\wedge {y}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({m}\in {\mathrm{Base}}_{{R}}\wedge \left({y}{\cdot }_{{R}}{x}={1}_{{R}}\wedge {m}{\cdot }_{{opp}_{r}\left({R}\right)}{x}={1}_{{R}}\right)\right)\right)\to {y}\in {U}$
66 65 46 jca ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\wedge {y}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({m}\in {\mathrm{Base}}_{{R}}\wedge \left({y}{\cdot }_{{R}}{x}={1}_{{R}}\wedge {m}{\cdot }_{{opp}_{r}\left({R}\right)}{x}={1}_{{R}}\right)\right)\right)\to \left({y}\in {U}\wedge {y}{\cdot }_{{R}}{x}={1}_{{R}}\right)$
67 66 rexlimdvaa ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\wedge {y}\in {\mathrm{Base}}_{{R}}\right)\to \left(\exists {m}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\left({y}{\cdot }_{{R}}{x}={1}_{{R}}\wedge {m}{\cdot }_{{opp}_{r}\left({R}\right)}{x}={1}_{{R}}\right)\to \left({y}\in {U}\wedge {y}{\cdot }_{{R}}{x}={1}_{{R}}\right)\right)$
68 67 expimpd ${⊢}\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\to \left(\left({y}\in {\mathrm{Base}}_{{R}}\wedge \exists {m}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\left({y}{\cdot }_{{R}}{x}={1}_{{R}}\wedge {m}{\cdot }_{{opp}_{r}\left({R}\right)}{x}={1}_{{R}}\right)\right)\to \left({y}\in {U}\wedge {y}{\cdot }_{{R}}{x}={1}_{{R}}\right)\right)$
69 68 reximdv2 ${⊢}\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\to \left(\exists {y}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\exists {m}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\left({y}{\cdot }_{{R}}{x}={1}_{{R}}\wedge {m}{\cdot }_{{opp}_{r}\left({R}\right)}{x}={1}_{{R}}\right)\to \exists {y}\in {U}\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{{R}}{x}={1}_{{R}}\right)$
70 37 69 syl5bir ${⊢}\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\to \left(\left(\exists {y}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{{R}}{x}={1}_{{R}}\wedge \exists {m}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}{m}{\cdot }_{{opp}_{r}\left({R}\right)}{x}={1}_{{R}}\right)\to \exists {y}\in {U}\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{{R}}{x}={1}_{{R}}\right)$
71 36 70 sylbid ${⊢}\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\to \left(\left({x}{\parallel }_{r}\left({R}\right){1}_{{R}}\wedge {x}{\parallel }_{r}\left({opp}_{r}\left({R}\right)\right){1}_{{R}}\right)\to \exists {y}\in {U}\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{{R}}{x}={1}_{{R}}\right)$
72 28 71 mpd ${⊢}\left({R}\in \mathrm{Ring}\wedge {x}\in {U}\right)\to \exists {y}\in {U}\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{{R}}{x}={1}_{{R}}$
73 4 10 11 18 20 22 72 isgrpde ${⊢}{R}\in \mathrm{Ring}\to {G}\in \mathrm{Grp}$