# 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}{↾}_{𝑠}{A}$
subrgugrp.2 ${⊢}{U}=\mathrm{Unit}\left({R}\right)$
subrgugrp.3 ${⊢}{V}=\mathrm{Unit}\left({S}\right)$
subrgugrp.4 ${⊢}{G}={\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}{U}$
Assertion subrgugrp ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {V}\in \mathrm{SubGrp}\left({G}\right)$

### Proof

Step Hyp Ref Expression
1 subrgugrp.1 ${⊢}{S}={R}{↾}_{𝑠}{A}$
2 subrgugrp.2 ${⊢}{U}=\mathrm{Unit}\left({R}\right)$
3 subrgugrp.3 ${⊢}{V}=\mathrm{Unit}\left({S}\right)$
4 subrgugrp.4 ${⊢}{G}={\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}{U}$
5 1 2 3 subrguss ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {V}\subseteq {U}$
6 1 subrgring ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {S}\in \mathrm{Ring}$
7 eqid ${⊢}{1}_{{S}}={1}_{{S}}$
8 3 7 1unit ${⊢}{S}\in \mathrm{Ring}\to {1}_{{S}}\in {V}$
9 ne0i ${⊢}{1}_{{S}}\in {V}\to {V}\ne \varnothing$
10 6 8 9 3syl ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {V}\ne \varnothing$
11 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
12 1 11 ressmulr ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {\cdot }_{{R}}={\cdot }_{{S}}$
13 12 3ad2ant1 ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {V}\wedge {y}\in {V}\right)\to {\cdot }_{{R}}={\cdot }_{{S}}$
14 13 oveqd ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {V}\wedge {y}\in {V}\right)\to {x}{\cdot }_{{R}}{y}={x}{\cdot }_{{S}}{y}$
15 eqid ${⊢}{\cdot }_{{S}}={\cdot }_{{S}}$
16 3 15 unitmulcl ${⊢}\left({S}\in \mathrm{Ring}\wedge {x}\in {V}\wedge {y}\in {V}\right)\to {x}{\cdot }_{{S}}{y}\in {V}$
17 6 16 syl3an1 ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {V}\wedge {y}\in {V}\right)\to {x}{\cdot }_{{S}}{y}\in {V}$
18 14 17 eqeltrd ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {V}\wedge {y}\in {V}\right)\to {x}{\cdot }_{{R}}{y}\in {V}$
19 18 3expa ${⊢}\left(\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {V}\right)\wedge {y}\in {V}\right)\to {x}{\cdot }_{{R}}{y}\in {V}$
20 19 ralrimiva ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {V}\right)\to \forall {y}\in {V}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{{R}}{y}\in {V}$
21 eqid ${⊢}{inv}_{r}\left({R}\right)={inv}_{r}\left({R}\right)$
22 eqid ${⊢}{inv}_{r}\left({S}\right)={inv}_{r}\left({S}\right)$
23 1 21 3 22 subrginv ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {V}\right)\to {inv}_{r}\left({R}\right)\left({x}\right)={inv}_{r}\left({S}\right)\left({x}\right)$
24 3 22 unitinvcl ${⊢}\left({S}\in \mathrm{Ring}\wedge {x}\in {V}\right)\to {inv}_{r}\left({S}\right)\left({x}\right)\in {V}$
25 6 24 sylan ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {V}\right)\to {inv}_{r}\left({S}\right)\left({x}\right)\in {V}$
26 23 25 eqeltrd ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {V}\right)\to {inv}_{r}\left({R}\right)\left({x}\right)\in {V}$
27 20 26 jca ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {V}\right)\to \left(\forall {y}\in {V}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{{R}}{y}\in {V}\wedge {inv}_{r}\left({R}\right)\left({x}\right)\in {V}\right)$
28 27 ralrimiva ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {V}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{{R}}{y}\in {V}\wedge {inv}_{r}\left({R}\right)\left({x}\right)\in {V}\right)$
29 subrgrcl ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {R}\in \mathrm{Ring}$
30 2 4 unitgrp ${⊢}{R}\in \mathrm{Ring}\to {G}\in \mathrm{Grp}$
31 2 4 unitgrpbas ${⊢}{U}={\mathrm{Base}}_{{G}}$
32 2 fvexi ${⊢}{U}\in \mathrm{V}$
33 eqid ${⊢}{\mathrm{mulGrp}}_{{R}}={\mathrm{mulGrp}}_{{R}}$
34 33 11 mgpplusg ${⊢}{\cdot }_{{R}}={+}_{{\mathrm{mulGrp}}_{{R}}}$
35 4 34 ressplusg ${⊢}{U}\in \mathrm{V}\to {\cdot }_{{R}}={+}_{{G}}$
36 32 35 ax-mp ${⊢}{\cdot }_{{R}}={+}_{{G}}$
37 2 4 21 invrfval ${⊢}{inv}_{r}\left({R}\right)={inv}_{g}\left({G}\right)$
38 31 36 37 issubg2 ${⊢}{G}\in \mathrm{Grp}\to \left({V}\in \mathrm{SubGrp}\left({G}\right)↔\left({V}\subseteq {U}\wedge {V}\ne \varnothing \wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {V}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{{R}}{y}\in {V}\wedge {inv}_{r}\left({R}\right)\left({x}\right)\in {V}\right)\right)\right)$
39 29 30 38 3syl ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to \left({V}\in \mathrm{SubGrp}\left({G}\right)↔\left({V}\subseteq {U}\wedge {V}\ne \varnothing \wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {V}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{{R}}{y}\in {V}\wedge {inv}_{r}\left({R}\right)\left({x}\right)\in {V}\right)\right)\right)$
40 5 10 28 39 mpbir3and ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {V}\in \mathrm{SubGrp}\left({G}\right)$