Theorem unitinvcl

Description: The inverse of a unit exists and is a unit. (Contributed by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Hypotheses	unitinvcl.1	⊢ 𝑈 = ( Unit ‘ 𝑅 )
	unitinvcl.2	⊢ 𝐼 = ( invr ‘ 𝑅 )
Assertion	unitinvcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		unitinvcl.1	⊢ 𝑈 = ( Unit ‘ 𝑅 )
2		unitinvcl.2	⊢ 𝐼 = ( invr ‘ 𝑅 )
3		eqid	⊢ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) = ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 )
4	1 3	unitgrp	⊢ ( 𝑅 ∈ Ring → ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) ∈ Grp )
5	1 3	unitgrpbas	⊢ 𝑈 = ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) )
6	1 3 2	invrfval	⊢ 𝐼 = ( invg ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) )
7	5 6	grpinvcl	⊢ ( ( ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) ∈ Grp ∧ 𝑋 ∈ 𝑈 ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝑈 )
8	4 7	sylan	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝑈 )