Metamath Proof Explorer

Theorem ringinvval

Description: The ring inverse expressed in terms of multiplication. (Contributed by Thierry Arnoux, 23-Oct-2017)

Ref Expression
Hypotheses ringinvval.b 
|- B = ( Base ` R )
ringinvval.p 
|- .* = ( .r ` R )
ringinvval.o 
|- .1. = ( 1r ` R )
ringinvval.n 
|- N = ( invr ` R )
ringinvval.u 
|- U = ( Unit ` R )
Assertion ringinvval 
|- ( ( R e. Ring /\ X e. U ) -> ( N ` X ) = ( iota_ y e. U ( y .* X ) = .1. ) )

Proof

Step Hyp Ref Expression
1 ringinvval.b 
 |-  B = ( Base ` R )
2 ringinvval.p 
 |-  .* = ( .r ` R )
3 ringinvval.o 
 |-  .1. = ( 1r ` R )
4 ringinvval.n 
 |-  N = ( invr ` R )
5 ringinvval.u 
 |-  U = ( Unit ` R )
6 eqid 
 |-  ( ( mulGrp ` R ) |`s U ) = ( ( mulGrp ` R ) |`s U )
7 5 6 unitgrpbas 
 |-  U = ( Base ` ( ( mulGrp ` R ) |`s U ) )
8 5 fvexi 
 |-  U e. _V
9 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
10 9 2 mgpplusg 
 |-  .* = ( +g ` ( mulGrp ` R ) )
11 6 10 ressplusg 
 |-  ( U e. _V -> .* = ( +g ` ( ( mulGrp ` R ) |`s U ) ) )
12 8 11 ax-mp 
 |-  .* = ( +g ` ( ( mulGrp ` R ) |`s U ) )
13 eqid 
 |-  ( 0g ` ( ( mulGrp ` R ) |`s U ) ) = ( 0g ` ( ( mulGrp ` R ) |`s U ) )
14 5 6 4 invrfval 
 |-  N = ( invg ` ( ( mulGrp ` R ) |`s U ) )
15 7 12 13 14 grpinvval 
 |-  ( X e. U -> ( N ` X ) = ( iota_ y e. U ( y .* X ) = ( 0g ` ( ( mulGrp ` R ) |`s U ) ) ) )
16 15 adantl 
 |-  ( ( R e. Ring /\ X e. U ) -> ( N ` X ) = ( iota_ y e. U ( y .* X ) = ( 0g ` ( ( mulGrp ` R ) |`s U ) ) ) )
17 5 6 3 unitgrpid 
 |-  ( R e. Ring -> .1. = ( 0g ` ( ( mulGrp ` R ) |`s U ) ) )
18 17 adantr 
 |-  ( ( R e. Ring /\ y e. U ) -> .1. = ( 0g ` ( ( mulGrp ` R ) |`s U ) ) )
19 18 eqeq2d 
 |-  ( ( R e. Ring /\ y e. U ) -> ( ( y .* X ) = .1. <-> ( y .* X ) = ( 0g ` ( ( mulGrp ` R ) |`s U ) ) ) )
20 19 riotabidva 
 |-  ( R e. Ring -> ( iota_ y e. U ( y .* X ) = .1. ) = ( iota_ y e. U ( y .* X ) = ( 0g ` ( ( mulGrp ` R ) |`s U ) ) ) )
21 20 adantr 
 |-  ( ( R e. Ring /\ X e. U ) -> ( iota_ y e. U ( y .* X ) = .1. ) = ( iota_ y e. U ( y .* X ) = ( 0g ` ( ( mulGrp ` R ) |`s U ) ) ) )
22 16 21 eqtr4d 
 |-  ( ( R e. Ring /\ X e. U ) -> ( N ` X ) = ( iota_ y e. U ( y .* X ) = .1. ) )