Theorem unitlinv

Description: A unit times its inverse is the identity. (Contributed by Mario Carneiro, 2-Dec-2014)

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

Proof

Step	Hyp	Ref	Expression
1		unitinvcl.1	⊢ 𝑈 = ( Unit ‘ 𝑅 )
2		unitinvcl.2	⊢ 𝐼 = ( invr ‘ 𝑅 )
3		unitinvcl.3	⊢ · = ( .r ‘ 𝑅 )
4		unitinvcl.4	⊢ 1 = ( 1r ‘ 𝑅 )
5		eqid	⊢ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) = ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 )
6	1 5	unitgrp	⊢ ( 𝑅 ∈ Ring → ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) ∈ Grp )
7	1 5	unitgrpbas	⊢ 𝑈 = ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) )
8	1	fvexi	⊢ 𝑈 ∈ V
9		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
10	9 3	mgpplusg	⊢ · = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
11	5 10	ressplusg	⊢ ( 𝑈 ∈ V → · = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) ) )
12	8 11	ax-mp	⊢ · = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) )
13		eqid	⊢ ( 0g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) ) = ( 0g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) )
14	1 5 2	invrfval	⊢ 𝐼 = ( invg ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) )
15	7 12 13 14	grplinv	⊢ ( ( ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) ∈ Grp ∧ 𝑋 ∈ 𝑈 ) → ( ( 𝐼 ‘ 𝑋 ) · 𝑋 ) = ( 0g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) ) )
16	6 15	sylan	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( ( 𝐼 ‘ 𝑋 ) · 𝑋 ) = ( 0g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) ) )
17	1 5 4	unitgrpid	⊢ ( 𝑅 ∈ Ring → 1 = ( 0g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) ) )
18	17	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → 1 = ( 0g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) ) )
19	16 18	eqtr4d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( ( 𝐼 ‘ 𝑋 ) · 𝑋 ) = 1 )