Theorem unitgrpid

Description: The identity of the group of units of a ring is the ring unity. (Contributed by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Hypotheses	unitmulcl.1	⊢ 𝑈 = ( Unit ‘ 𝑅 )
	unitgrp.2	⊢ 𝐺 = ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 )
	unitgrp.3	⊢ 1 = ( 1r ‘ 𝑅 )
Assertion	unitgrpid	⊢ ( 𝑅 ∈ Ring → 1 = ( 0g ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		unitmulcl.1	⊢ 𝑈 = ( Unit ‘ 𝑅 )
2		unitgrp.2	⊢ 𝐺 = ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 )
3		unitgrp.3	⊢ 1 = ( 1r ‘ 𝑅 )
4	1 3	1unit	⊢ ( 𝑅 ∈ Ring → 1 ∈ 𝑈 )
5		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6	5 1	unitss	⊢ 𝑈 ⊆ ( Base ‘ 𝑅 )
7	2 5 3	ringidss	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ⊆ ( Base ‘ 𝑅 ) ∧ 1 ∈ 𝑈 ) → 1 = ( 0g ‘ 𝐺 ) )
8	6 7	mp3an2	⊢ ( ( 𝑅 ∈ Ring ∧ 1 ∈ 𝑈 ) → 1 = ( 0g ‘ 𝐺 ) )
9	4 8	mpdan	⊢ ( 𝑅 ∈ Ring → 1 = ( 0g ‘ 𝐺 ) )