# Metamath Proof Explorer

## Theorem subrginv

Description: A subring always has the same inversion function, for elements that are invertible. (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Hypotheses subrginv.1 ${⊢}{S}={R}{↾}_{𝑠}{A}$
subrginv.2 ${⊢}{I}={inv}_{r}\left({R}\right)$
subrginv.3 ${⊢}{U}=\mathrm{Unit}\left({S}\right)$
subrginv.4 ${⊢}{J}={inv}_{r}\left({S}\right)$
Assertion subrginv ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {X}\in {U}\right)\to {I}\left({X}\right)={J}\left({X}\right)$

### Proof

Step Hyp Ref Expression
1 subrginv.1 ${⊢}{S}={R}{↾}_{𝑠}{A}$
2 subrginv.2 ${⊢}{I}={inv}_{r}\left({R}\right)$
3 subrginv.3 ${⊢}{U}=\mathrm{Unit}\left({S}\right)$
4 subrginv.4 ${⊢}{J}={inv}_{r}\left({S}\right)$
5 subrgrcl ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {R}\in \mathrm{Ring}$
6 5 adantr ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {X}\in {U}\right)\to {R}\in \mathrm{Ring}$
7 1 subrgbas ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {A}={\mathrm{Base}}_{{S}}$
8 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
9 8 subrgss ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {A}\subseteq {\mathrm{Base}}_{{R}}$
10 7 9 eqsstrrd ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {\mathrm{Base}}_{{S}}\subseteq {\mathrm{Base}}_{{R}}$
11 10 adantr ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {X}\in {U}\right)\to {\mathrm{Base}}_{{S}}\subseteq {\mathrm{Base}}_{{R}}$
12 1 subrgring ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {S}\in \mathrm{Ring}$
13 eqid ${⊢}{\mathrm{Base}}_{{S}}={\mathrm{Base}}_{{S}}$
14 3 4 13 ringinvcl ${⊢}\left({S}\in \mathrm{Ring}\wedge {X}\in {U}\right)\to {J}\left({X}\right)\in {\mathrm{Base}}_{{S}}$
15 12 14 sylan ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {X}\in {U}\right)\to {J}\left({X}\right)\in {\mathrm{Base}}_{{S}}$
16 11 15 sseldd ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {X}\in {U}\right)\to {J}\left({X}\right)\in {\mathrm{Base}}_{{R}}$
17 13 3 unitcl ${⊢}{X}\in {U}\to {X}\in {\mathrm{Base}}_{{S}}$
18 17 adantl ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {X}\in {U}\right)\to {X}\in {\mathrm{Base}}_{{S}}$
19 11 18 sseldd ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {X}\in {U}\right)\to {X}\in {\mathrm{Base}}_{{R}}$
20 eqid ${⊢}\mathrm{Unit}\left({R}\right)=\mathrm{Unit}\left({R}\right)$
21 1 20 3 subrguss ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {U}\subseteq \mathrm{Unit}\left({R}\right)$
22 21 sselda ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {X}\in {U}\right)\to {X}\in \mathrm{Unit}\left({R}\right)$
23 20 2 8 ringinvcl ${⊢}\left({R}\in \mathrm{Ring}\wedge {X}\in \mathrm{Unit}\left({R}\right)\right)\to {I}\left({X}\right)\in {\mathrm{Base}}_{{R}}$
24 5 22 23 syl2an2r ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {X}\in {U}\right)\to {I}\left({X}\right)\in {\mathrm{Base}}_{{R}}$
25 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
26 8 25 ringass ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({J}\left({X}\right)\in {\mathrm{Base}}_{{R}}\wedge {X}\in {\mathrm{Base}}_{{R}}\wedge {I}\left({X}\right)\in {\mathrm{Base}}_{{R}}\right)\right)\to \left({J}\left({X}\right){\cdot }_{{R}}{X}\right){\cdot }_{{R}}{I}\left({X}\right)={J}\left({X}\right){\cdot }_{{R}}\left({X}{\cdot }_{{R}}{I}\left({X}\right)\right)$
27 6 16 19 24 26 syl13anc ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {X}\in {U}\right)\to \left({J}\left({X}\right){\cdot }_{{R}}{X}\right){\cdot }_{{R}}{I}\left({X}\right)={J}\left({X}\right){\cdot }_{{R}}\left({X}{\cdot }_{{R}}{I}\left({X}\right)\right)$
28 eqid ${⊢}{\cdot }_{{S}}={\cdot }_{{S}}$
29 eqid ${⊢}{1}_{{S}}={1}_{{S}}$
30 3 4 28 29 unitlinv ${⊢}\left({S}\in \mathrm{Ring}\wedge {X}\in {U}\right)\to {J}\left({X}\right){\cdot }_{{S}}{X}={1}_{{S}}$
31 12 30 sylan ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {X}\in {U}\right)\to {J}\left({X}\right){\cdot }_{{S}}{X}={1}_{{S}}$
32 1 25 ressmulr ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {\cdot }_{{R}}={\cdot }_{{S}}$
33 32 adantr ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {X}\in {U}\right)\to {\cdot }_{{R}}={\cdot }_{{S}}$
34 33 oveqd ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {X}\in {U}\right)\to {J}\left({X}\right){\cdot }_{{R}}{X}={J}\left({X}\right){\cdot }_{{S}}{X}$
35 eqid ${⊢}{1}_{{R}}={1}_{{R}}$
36 1 35 subrg1 ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {1}_{{R}}={1}_{{S}}$
37 36 adantr ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {X}\in {U}\right)\to {1}_{{R}}={1}_{{S}}$
38 31 34 37 3eqtr4d ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {X}\in {U}\right)\to {J}\left({X}\right){\cdot }_{{R}}{X}={1}_{{R}}$
39 38 oveq1d ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {X}\in {U}\right)\to \left({J}\left({X}\right){\cdot }_{{R}}{X}\right){\cdot }_{{R}}{I}\left({X}\right)={1}_{{R}}{\cdot }_{{R}}{I}\left({X}\right)$
40 20 2 25 35 unitrinv ${⊢}\left({R}\in \mathrm{Ring}\wedge {X}\in \mathrm{Unit}\left({R}\right)\right)\to {X}{\cdot }_{{R}}{I}\left({X}\right)={1}_{{R}}$
41 5 22 40 syl2an2r ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {X}\in {U}\right)\to {X}{\cdot }_{{R}}{I}\left({X}\right)={1}_{{R}}$
42 41 oveq2d ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {X}\in {U}\right)\to {J}\left({X}\right){\cdot }_{{R}}\left({X}{\cdot }_{{R}}{I}\left({X}\right)\right)={J}\left({X}\right){\cdot }_{{R}}{1}_{{R}}$
43 27 39 42 3eqtr3d ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {X}\in {U}\right)\to {1}_{{R}}{\cdot }_{{R}}{I}\left({X}\right)={J}\left({X}\right){\cdot }_{{R}}{1}_{{R}}$
44 8 25 35 ringlidm ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\left({X}\right)\in {\mathrm{Base}}_{{R}}\right)\to {1}_{{R}}{\cdot }_{{R}}{I}\left({X}\right)={I}\left({X}\right)$
45 5 24 44 syl2an2r ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {X}\in {U}\right)\to {1}_{{R}}{\cdot }_{{R}}{I}\left({X}\right)={I}\left({X}\right)$
46 8 25 35 ringridm ${⊢}\left({R}\in \mathrm{Ring}\wedge {J}\left({X}\right)\in {\mathrm{Base}}_{{R}}\right)\to {J}\left({X}\right){\cdot }_{{R}}{1}_{{R}}={J}\left({X}\right)$
47 5 16 46 syl2an2r ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {X}\in {U}\right)\to {J}\left({X}\right){\cdot }_{{R}}{1}_{{R}}={J}\left({X}\right)$
48 43 45 47 3eqtr3d ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {X}\in {U}\right)\to {I}\left({X}\right)={J}\left({X}\right)$