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. )