unitabl

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

Step	Hyp	Ref	Expression
1		unitmulcl.1	$⊢ U = Unit (R)$
2		unitgrp.2	$⊢ G = {mulGrp}_{R} ↾_{𝑠} U$
3		crngring	$⊢ R \in CRing \to R \in Ring$
4	1 2	unitgrp	$⊢ R \in Ring \to G \in Grp$
5	3 4	syl	$⊢ R \in CRing \to G \in Grp$
6		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
7	6	crngmgp	$⊢ R \in CRing \to {mulGrp}_{R} \in CMnd$
8	5	grpmndd	$⊢ R \in CRing \to G \in Mnd$
9	2	subcmn	$⊢ ({mulGrp}_{R} \in CMnd \land G \in Mnd) \to G \in CMnd$
10	7 8 9	syl2anc	$⊢ R \in CRing \to G \in CMnd$
11		isabl	$⊢ G \in Abel \leftrightarrow (G \in Grp \land G \in CMnd)$
12	5 10 11	sylanbrc	$⊢ R \in CRing \to G \in Abel$

Metamath Proof Explorer