# 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 ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{K}}$
rngidpropd.2 ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{L}}$
rngidpropd.3 ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {x}{\cdot }_{{K}}{y}={x}{\cdot }_{{L}}{y}$
Assertion invrpropd ${⊢}{\phi }\to {inv}_{r}\left({K}\right)={inv}_{r}\left({L}\right)$

### Proof

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