Theorem unitinvinv

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

	Ref	Expression
Hypotheses	unitinvcl.1	⊢ 𝑈 = ( Unit ‘ 𝑅 )
	unitinvcl.2	⊢ 𝐼 = ( invr ‘ 𝑅 )
Assertion	unitinvinv	⊢ ( ( 𝑅 ∈ 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	grpinvinv	⊢ ( ( ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) ∈ Grp ∧ 𝑋 ∈ 𝑈 ) → ( 𝐼 ‘ ( 𝐼 ‘ 𝑋 ) ) = 𝑋 )
8	4 7	sylan	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝐼 ‘ ( 𝐼 ‘ 𝑋 ) ) = 𝑋 )