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 φ B = Base K
rngidpropd.2 φ B = Base L
rngidpropd.3 φ x B y B x K y = x L y
Assertion invrpropd φ inv r K = inv r L

Proof

Step Hyp Ref Expression
1 rngidpropd.1 φ B = Base K
2 rngidpropd.2 φ B = Base L
3 rngidpropd.3 φ x B y B x K y = x L y
4 eqid Unit K = Unit K
5 eqid mulGrp K 𝑠 Unit K = mulGrp K 𝑠 Unit K
6 4 5 unitgrpbas Unit K = Base mulGrp K 𝑠 Unit K
7 6 a1i φ Unit K = Base mulGrp K 𝑠 Unit K
8 1 2 3 unitpropd φ Unit K = Unit L
9 eqid Unit L = Unit L
10 eqid mulGrp L 𝑠 Unit L = mulGrp L 𝑠 Unit L
11 9 10 unitgrpbas Unit L = Base mulGrp L 𝑠 Unit L
12 8 11 syl6eq φ Unit K = Base mulGrp L 𝑠 Unit L
13 eqid Base K = Base K
14 13 4 unitss Unit K Base K
15 14 1 sseqtrrid φ Unit K B
16 15 sselda φ x Unit K x B
17 15 sselda φ y Unit K y B
18 16 17 anim12dan φ x Unit K y Unit K x B y B
19 18 3 syldan φ x Unit K y Unit K x K y = x L y
20 fvex Unit K V
21 eqid mulGrp K = mulGrp K
22 eqid K = K
23 21 22 mgpplusg K = + mulGrp K
24 5 23 ressplusg Unit K V K = + mulGrp K 𝑠 Unit K
25 20 24 ax-mp K = + mulGrp K 𝑠 Unit K
26 25 oveqi x K y = x + mulGrp K 𝑠 Unit K y
27 fvex Unit L V
28 eqid mulGrp L = mulGrp L
29 eqid L = L
30 28 29 mgpplusg L = + mulGrp L
31 10 30 ressplusg Unit L V L = + mulGrp L 𝑠 Unit L
32 27 31 ax-mp L = + mulGrp L 𝑠 Unit L
33 32 oveqi x L y = x + mulGrp L 𝑠 Unit L y
34 19 26 33 3eqtr3g φ x Unit K y Unit K x + mulGrp K 𝑠 Unit K y = x + mulGrp L 𝑠 Unit L y
35 7 12 34 grpinvpropd φ inv g mulGrp K 𝑠 Unit K = inv g mulGrp L 𝑠 Unit L
36 eqid inv r K = inv r K
37 4 5 36 invrfval inv r K = inv g mulGrp K 𝑠 Unit K
38 eqid inv r L = inv r L
39 9 10 38 invrfval inv r L = inv g mulGrp L 𝑠 Unit L
40 35 37 39 3eqtr4g φ inv r K = inv r L