This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) |`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 )