Metamath Proof Explorer


Theorem unitlinv

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

Ref Expression
Hypotheses unitinvcl.1
|- U = ( Unit ` R )
unitinvcl.2
|- I = ( invr ` R )
unitinvcl.3
|- .x. = ( .r ` R )
unitinvcl.4
|- .1. = ( 1r ` R )
Assertion unitlinv
|- ( ( R e. Ring /\ X e. U ) -> ( ( I ` X ) .x. X ) = .1. )

Proof

Step Hyp Ref Expression
1 unitinvcl.1
 |-  U = ( Unit ` R )
2 unitinvcl.2
 |-  I = ( invr ` R )
3 unitinvcl.3
 |-  .x. = ( .r ` R )
4 unitinvcl.4
 |-  .1. = ( 1r ` R )
5 eqid
 |-  ( ( mulGrp ` R ) |`s U ) = ( ( mulGrp ` R ) |`s U )
6 1 5 unitgrp
 |-  ( R e. Ring -> ( ( mulGrp ` R ) |`s U ) e. Grp )
7 1 5 unitgrpbas
 |-  U = ( Base ` ( ( mulGrp ` R ) |`s U ) )
8 1 fvexi
 |-  U e. _V
9 eqid
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
10 9 3 mgpplusg
 |-  .x. = ( +g ` ( mulGrp ` R ) )
11 5 10 ressplusg
 |-  ( U e. _V -> .x. = ( +g ` ( ( mulGrp ` R ) |`s U ) ) )
12 8 11 ax-mp
 |-  .x. = ( +g ` ( ( mulGrp ` R ) |`s U ) )
13 eqid
 |-  ( 0g ` ( ( mulGrp ` R ) |`s U ) ) = ( 0g ` ( ( mulGrp ` R ) |`s U ) )
14 1 5 2 invrfval
 |-  I = ( invg ` ( ( mulGrp ` R ) |`s U ) )
15 7 12 13 14 grplinv
 |-  ( ( ( ( mulGrp ` R ) |`s U ) e. Grp /\ X e. U ) -> ( ( I ` X ) .x. X ) = ( 0g ` ( ( mulGrp ` R ) |`s U ) ) )
16 6 15 sylan
 |-  ( ( R e. Ring /\ X e. U ) -> ( ( I ` X ) .x. X ) = ( 0g ` ( ( mulGrp ` R ) |`s U ) ) )
17 1 5 4 unitgrpid
 |-  ( R e. Ring -> .1. = ( 0g ` ( ( mulGrp ` R ) |`s U ) ) )
18 17 adantr
 |-  ( ( R e. Ring /\ X e. U ) -> .1. = ( 0g ` ( ( mulGrp ` R ) |`s U ) ) )
19 16 18 eqtr4d
 |-  ( ( R e. Ring /\ X e. U ) -> ( ( I ` X ) .x. X ) = .1. )