Metamath Proof Explorer

Theorem invrpropd

Description: The ring inverse function depends only on the ring's base set and multiplication operation. (Contributed by Mario Carneiro, 26-Dec-2014) (Revised by Mario Carneiro, 5-Oct-2015)

Ref Expression
Hypotheses rngidpropd.1 
|- ( ph -> B = ( Base ` K ) )
rngidpropd.2 
|- ( ph -> B = ( Base ` L ) )
rngidpropd.3 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
Assertion invrpropd 
|- ( ph -> ( invr ` K ) = ( invr ` L ) )

Proof

Step Hyp Ref Expression
1 rngidpropd.1 
 |-  ( ph -> B = ( Base ` K ) )
2 rngidpropd.2 
 |-  ( ph -> B = ( Base ` L ) )
3 rngidpropd.3 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
4 eqid 
 |-  ( Unit ` K ) = ( Unit ` K )
5 eqid 
 |-  ( ( mulGrp ` K ) |`s ( Unit ` K ) ) = ( ( mulGrp ` K ) |`s ( Unit ` K ) )
6 4 5 unitgrpbas 
 |-  ( Unit ` K ) = ( Base ` ( ( mulGrp ` K ) |`s ( Unit ` K ) ) )
7 6 a1i 
 |-  ( ph -> ( Unit ` K ) = ( Base ` ( ( mulGrp ` K ) |`s ( Unit ` K ) ) ) )
8 1 2 3 unitpropd 
 |-  ( ph -> ( Unit ` K ) = ( Unit ` L ) )
9 eqid 
 |-  ( Unit ` L ) = ( Unit ` L )
10 eqid 
 |-  ( ( mulGrp ` L ) |`s ( Unit ` L ) ) = ( ( mulGrp ` L ) |`s ( Unit ` L ) )
11 9 10 unitgrpbas 
 |-  ( Unit ` L ) = ( Base ` ( ( mulGrp ` L ) |`s ( Unit ` L ) ) )
12 8 11 eqtrdi 
 |-  ( ph -> ( Unit ` K ) = ( Base ` ( ( mulGrp ` L ) |`s ( Unit ` L ) ) ) )
13 eqid 
 |-  ( Base ` K ) = ( Base ` K )
14 13 4 unitss 
 |-  ( Unit ` K ) C_ ( Base ` K )
15 14 1 sseqtrrid 
 |-  ( ph -> ( Unit ` K ) C_ B )
16 15 sselda 
 |-  ( ( ph /\ x e. ( Unit ` K ) ) -> x e. B )
17 15 sselda 
 |-  ( ( ph /\ y e. ( Unit ` K ) ) -> y e. B )
18 16 17 anim12dan 
 |-  ( ( ph /\ ( x e. ( Unit ` K ) /\ y e. ( Unit ` K ) ) ) -> ( x e. B /\ y e. B ) )
19 18 3 syldan 
 |-  ( ( ph /\ ( x e. ( Unit ` K ) /\ y e. ( Unit ` K ) ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
20 fvex 
 |-  ( Unit ` K ) e. _V
21 eqid 
 |-  ( mulGrp ` K ) = ( mulGrp ` K )
22 eqid 
 |-  ( .r ` K ) = ( .r ` K )
23 21 22 mgpplusg 
 |-  ( .r ` K ) = ( +g ` ( mulGrp ` K ) )
24 5 23 ressplusg 
 |-  ( ( Unit ` K ) e. _V -> ( .r ` K ) = ( +g ` ( ( mulGrp ` K ) |`s ( Unit ` K ) ) ) )
25 20 24 ax-mp 
 |-  ( .r ` K ) = ( +g ` ( ( mulGrp ` K ) |`s ( Unit ` K ) ) )
26 25 oveqi 
 |-  ( x ( .r ` K ) y ) = ( x ( +g ` ( ( mulGrp ` K ) |`s ( Unit ` K ) ) ) y )
27 fvex 
 |-  ( Unit ` L ) e. _V
28 eqid 
 |-  ( mulGrp ` L ) = ( mulGrp ` L )
29 eqid 
 |-  ( .r ` L ) = ( .r ` L )
30 28 29 mgpplusg 
 |-  ( .r ` L ) = ( +g ` ( mulGrp ` L ) )
31 10 30 ressplusg 
 |-  ( ( Unit ` L ) e. _V -> ( .r ` L ) = ( +g ` ( ( mulGrp ` L ) |`s ( Unit ` L ) ) ) )
32 27 31 ax-mp 
 |-  ( .r ` L ) = ( +g ` ( ( mulGrp ` L ) |`s ( Unit ` L ) ) )
33 32 oveqi 
 |-  ( x ( .r ` L ) y ) = ( x ( +g ` ( ( mulGrp ` L ) |`s ( Unit ` L ) ) ) y )
34 19 26 33 3eqtr3g 
 |-  ( ( ph /\ ( x e. ( Unit ` K ) /\ y e. ( Unit ` K ) ) ) -> ( x ( +g ` ( ( mulGrp ` K ) |`s ( Unit ` K ) ) ) y ) = ( x ( +g ` ( ( mulGrp ` L ) |`s ( Unit ` L ) ) ) y ) )
35 7 12 34 grpinvpropd 
 |-  ( ph -> ( invg ` ( ( mulGrp ` K ) |`s ( Unit ` K ) ) ) = ( invg ` ( ( mulGrp ` L ) |`s ( Unit ` L ) ) ) )
36 eqid 
 |-  ( invr ` K ) = ( invr ` K )
37 4 5 36 invrfval 
 |-  ( invr ` K ) = ( invg ` ( ( mulGrp ` K ) |`s ( Unit ` K ) ) )
38 eqid 
 |-  ( invr ` L ) = ( invr ` L )
39 9 10 38 invrfval 
 |-  ( invr ` L ) = ( invg ` ( ( mulGrp ` L ) |`s ( Unit ` L ) ) )
40 35 37 39 3eqtr4g 
 |-  ( ph -> ( invr ` K ) = ( invr ` L ) )