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 ⊢ 𝑈 = ( Unit ‘ 𝑅 )
unitgrp.2 ⊢ 𝐺 = ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 )
Assertion unitabl ( 𝑅 ∈ CRing → 𝐺 ∈ Abel )

Proof

Step Hyp Ref Expression
1 unitmulcl.1 ⊢ 𝑈 = ( Unit ‘ 𝑅 )
2 unitgrp.2 ⊢ 𝐺 = ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 )
3 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
4 1 2 unitgrp ⊢ ( 𝑅 ∈ Ring → 𝐺 ∈ Grp )
5 3 4 syl ⊢ ( 𝑅 ∈ CRing → 𝐺 ∈ Grp )
6 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
7 6 crngmgp ⊢ ( 𝑅 ∈ CRing → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
8 5 grpmndd ⊢ ( 𝑅 ∈ CRing → 𝐺 ∈ Mnd )
9 2 subcmn ⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ CMnd ∧ 𝐺 ∈ Mnd ) → 𝐺 ∈ CMnd )
10 7 8 9 syl2anc ⊢ ( 𝑅 ∈ CRing → 𝐺 ∈ CMnd )
11 isabl ⊢ ( 𝐺 ∈ Abel ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd ) )
12 5 10 11 sylanbrc ⊢ ( 𝑅 ∈ CRing → 𝐺 ∈ Abel )