Metamath Proof Explorer


Theorem unitrinv

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 unitrinv ( ( 𝑅 ∈ 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 grprinv ( ( ( ( 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 )