Theorem ringinvcl

Description: The inverse of a unit is an element of the ring. (Contributed by Mario Carneiro, 2-Dec-2014)

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

Proof

Step	Hyp	Ref	Expression
1		unitinvcl.1	⊢ 𝑈 = ( Unit ‘ 𝑅 )
2		unitinvcl.2	⊢ 𝐼 = ( invr ‘ 𝑅 )
3		ringinvcl.3	⊢ 𝐵 = ( Base ‘ 𝑅 )
4	1 2	unitinvcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝑈 )
5	3 1	unitcl	⊢ ( ( 𝐼 ‘ 𝑋 ) ∈ 𝑈 → ( 𝐼 ‘ 𝑋 ) ∈ 𝐵 )
6	4 5	syl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝐵 )