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 ‘ 𝐺 ) )