Metamath Proof Explorer

Theorem unitabl

Description: The group of units of a commutative ring is abelian. (Contributed by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses unitmulcl.1 ⊢ U = Unit ⁡ R
unitgrp.2 ⊢ G = mulGrp R ↾ 𝑠 U
Assertion unitabl ⊢ R ∈ CRing → G ∈ Abel

Proof

Step Hyp Ref Expression
1 unitmulcl.1 ⊢ U = Unit ⁡ R
2 unitgrp.2 ⊢ G = mulGrp R ↾ 𝑠 U
3 crngring ⊢ R ∈ CRing → R ∈ Ring
4 1 2 unitgrp ⊢ R ∈ Ring → G ∈ Grp
5 3 4 syl ⊢ R ∈ CRing → G ∈ Grp
6 eqid ⊢ mulGrp R = mulGrp R
7 6 crngmgp ⊢ R ∈ CRing → mulGrp R ∈ CMnd
8 5 grpmndd ⊢ R ∈ CRing → G ∈ Mnd
9 2 subcmn ⊢ mulGrp R ∈ CMnd ∧ G ∈ Mnd → G ∈ CMnd
10 7 8 9 syl2anc ⊢ R ∈ CRing → G ∈ CMnd
11 isabl ⊢ G ∈ Abel ↔ G ∈ Grp ∧ G ∈ CMnd
12 5 10 11 sylanbrc ⊢ R ∈ CRing → G ∈ Abel