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 ) |`s U )
Assertion	unitabl	|- ( R e. CRing -> G e. Abel )

Proof

Step	Hyp	Ref	Expression
1		unitmulcl.1	|- U = ( Unit ` R )
2		unitgrp.2	|- G = ( ( mulGrp ` R ) |`s U )
3		crngring	|- ( R e. CRing -> R e. Ring )
4	1 2	unitgrp	|- ( R e. Ring -> G e. Grp )
5	3 4	syl	|- ( R e. CRing -> G e. Grp )
6		eqid	|- ( mulGrp ` R ) = ( mulGrp ` R )
7	6	crngmgp	|- ( R e. CRing -> ( mulGrp ` R ) e. CMnd )
8	5	grpmndd	|- ( R e. CRing -> G e. Mnd )
9	2	subcmn	|- ( ( ( mulGrp ` R ) e. CMnd /\ G e. Mnd ) -> G e. CMnd )
10	7 8 9	syl2anc	|- ( R e. CRing -> G e. CMnd )
11		isabl	|- ( G e. Abel <-> ( G e. Grp /\ G e. CMnd ) )
12	5 10 11	sylanbrc	|- ( R e. CRing -> G e. Abel )