# 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 𝐴 )
subrgugrp.2 𝑈 = ( Unit ‘ 𝑅 )
subrgugrp.3 𝑉 = ( Unit ‘ 𝑆 )
subrgugrp.4 𝐺 = ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 )
Assertion subrgugrp ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝑉 ∈ ( SubGrp ‘ 𝐺 ) )

### Proof

Step Hyp Ref Expression
1 subrgugrp.1 𝑆 = ( 𝑅s 𝐴 )
2 subrgugrp.2 𝑈 = ( Unit ‘ 𝑅 )
3 subrgugrp.3 𝑉 = ( Unit ‘ 𝑆 )
4 subrgugrp.4 𝐺 = ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 )
5 1 2 3 subrguss ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝑉𝑈 )
6 1 subrgring ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 ∈ Ring )
7 eqid ( 1r𝑆 ) = ( 1r𝑆 )
8 3 7 1unit ( 𝑆 ∈ Ring → ( 1r𝑆 ) ∈ 𝑉 )
9 ne0i ( ( 1r𝑆 ) ∈ 𝑉𝑉 ≠ ∅ )
10 6 8 9 3syl ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝑉 ≠ ∅ )
11 eqid ( .r𝑅 ) = ( .r𝑅 )
12 1 11 ressmulr ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( .r𝑅 ) = ( .r𝑆 ) )
13 12 3ad2ant1 ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥𝑉𝑦𝑉 ) → ( .r𝑅 ) = ( .r𝑆 ) )
14 13 oveqd ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥𝑉𝑦𝑉 ) → ( 𝑥 ( .r𝑅 ) 𝑦 ) = ( 𝑥 ( .r𝑆 ) 𝑦 ) )
15 eqid ( .r𝑆 ) = ( .r𝑆 )
16 3 15 unitmulcl ( ( 𝑆 ∈ Ring ∧ 𝑥𝑉𝑦𝑉 ) → ( 𝑥 ( .r𝑆 ) 𝑦 ) ∈ 𝑉 )
17 6 16 syl3an1 ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥𝑉𝑦𝑉 ) → ( 𝑥 ( .r𝑆 ) 𝑦 ) ∈ 𝑉 )
18 14 17 eqeltrd ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥𝑉𝑦𝑉 ) → ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑉 )
19 18 3expa ( ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥𝑉 ) ∧ 𝑦𝑉 ) → ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑉 )
20 19 ralrimiva ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥𝑉 ) → ∀ 𝑦𝑉 ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑉 )
21 eqid ( invr𝑅 ) = ( invr𝑅 )
22 eqid ( invr𝑆 ) = ( invr𝑆 )
23 1 21 3 22 subrginv ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥𝑉 ) → ( ( invr𝑅 ) ‘ 𝑥 ) = ( ( invr𝑆 ) ‘ 𝑥 ) )
24 3 22 unitinvcl ( ( 𝑆 ∈ Ring ∧ 𝑥𝑉 ) → ( ( invr𝑆 ) ‘ 𝑥 ) ∈ 𝑉 )
25 6 24 sylan ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥𝑉 ) → ( ( invr𝑆 ) ‘ 𝑥 ) ∈ 𝑉 )
26 23 25 eqeltrd ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥𝑉 ) → ( ( invr𝑅 ) ‘ 𝑥 ) ∈ 𝑉 )
27 20 26 jca ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥𝑉 ) → ( ∀ 𝑦𝑉 ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑉 ∧ ( ( invr𝑅 ) ‘ 𝑥 ) ∈ 𝑉 ) )
28 27 ralrimiva ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ∀ 𝑥𝑉 ( ∀ 𝑦𝑉 ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑉 ∧ ( ( invr𝑅 ) ‘ 𝑥 ) ∈ 𝑉 ) )
29 subrgrcl ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝑅 ∈ Ring )
30 2 4 unitgrp ( 𝑅 ∈ Ring → 𝐺 ∈ Grp )
31 2 4 unitgrpbas 𝑈 = ( Base ‘ 𝐺 )
32 2 fvexi 𝑈 ∈ V
33 eqid ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
34 33 11 mgpplusg ( .r𝑅 ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
35 4 34 ressplusg ( 𝑈 ∈ V → ( .r𝑅 ) = ( +g𝐺 ) )
36 32 35 ax-mp ( .r𝑅 ) = ( +g𝐺 )
37 2 4 21 invrfval ( invr𝑅 ) = ( invg𝐺 )
38 31 36 37 issubg2 ( 𝐺 ∈ Grp → ( 𝑉 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑉𝑈𝑉 ≠ ∅ ∧ ∀ 𝑥𝑉 ( ∀ 𝑦𝑉 ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑉 ∧ ( ( invr𝑅 ) ‘ 𝑥 ) ∈ 𝑉 ) ) ) )
39 29 30 38 3syl ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 𝑉 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑉𝑈𝑉 ≠ ∅ ∧ ∀ 𝑥𝑉 ( ∀ 𝑦𝑉 ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑉 ∧ ( ( invr𝑅 ) ‘ 𝑥 ) ∈ 𝑉 ) ) ) )
40 5 10 28 39 mpbir3and ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝑉 ∈ ( SubGrp ‘ 𝐺 ) )