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		grpmnd	⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
9	5 8	syl	⊢ ( 𝑅 ∈ CRing → 𝐺 ∈ Mnd )
10	2	subcmn	⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ CMnd ∧ 𝐺 ∈ Mnd ) → 𝐺 ∈ CMnd )
11	7 9 10	syl2anc	⊢ ( 𝑅 ∈ CRing → 𝐺 ∈ CMnd )
12		isabl	⊢ ( 𝐺 ∈ Abel ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd ) )
13	5 11 12	sylanbrc	⊢ ( 𝑅 ∈ CRing → 𝐺 ∈ Abel )