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		grpmnd	|- ( G e. Grp -> G e. Mnd )
9	5 8	syl	|- ( R e. CRing -> G e. Mnd )
10	2	subcmn	|- ( ( ( mulGrp ` R ) e. CMnd /\ G e. Mnd ) -> G e. CMnd )
11	7 9 10	syl2anc	|- ( R e. CRing -> G e. CMnd )
12		isabl	|- ( G e. Abel <-> ( G e. Grp /\ G e. CMnd ) )
13	5 11 12	sylanbrc	|- ( R e. CRing -> G e. Abel )