# Metamath Proof Explorer

## Theorem subrg1

Description: A subring always has the same multiplicative identity. (Contributed by Stefan O'Rear, 27-Nov-2014)

Ref Expression
Hypotheses subrg1.1 ${⊢}{S}={R}{↾}_{𝑠}{A}$
subrg1.2
Assertion subrg1

### Proof

Step Hyp Ref Expression
1 subrg1.1 ${⊢}{S}={R}{↾}_{𝑠}{A}$
2 subrg1.2
3 eqid ${⊢}{1}_{{R}}={1}_{{R}}$
4 3 subrg1cl ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {1}_{{R}}\in {A}$
5 1 subrgbas ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {A}={\mathrm{Base}}_{{S}}$
6 4 5 eleqtrd ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {1}_{{R}}\in {\mathrm{Base}}_{{S}}$
7 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
8 7 subrgss ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {A}\subseteq {\mathrm{Base}}_{{R}}$
9 5 8 eqsstrrd ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {\mathrm{Base}}_{{S}}\subseteq {\mathrm{Base}}_{{R}}$
10 9 sselda ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {\mathrm{Base}}_{{S}}\right)\to {x}\in {\mathrm{Base}}_{{R}}$
11 subrgrcl ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {R}\in \mathrm{Ring}$
12 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
13 7 12 3 ringidmlem ${⊢}\left({R}\in \mathrm{Ring}\wedge {x}\in {\mathrm{Base}}_{{R}}\right)\to \left({1}_{{R}}{\cdot }_{{R}}{x}={x}\wedge {x}{\cdot }_{{R}}{1}_{{R}}={x}\right)$
14 11 13 sylan ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {\mathrm{Base}}_{{R}}\right)\to \left({1}_{{R}}{\cdot }_{{R}}{x}={x}\wedge {x}{\cdot }_{{R}}{1}_{{R}}={x}\right)$
15 1 12 ressmulr ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {\cdot }_{{R}}={\cdot }_{{S}}$
16 15 oveqd ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {1}_{{R}}{\cdot }_{{R}}{x}={1}_{{R}}{\cdot }_{{S}}{x}$
17 16 eqeq1d ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to \left({1}_{{R}}{\cdot }_{{R}}{x}={x}↔{1}_{{R}}{\cdot }_{{S}}{x}={x}\right)$
18 15 oveqd ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {x}{\cdot }_{{R}}{1}_{{R}}={x}{\cdot }_{{S}}{1}_{{R}}$
19 18 eqeq1d ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to \left({x}{\cdot }_{{R}}{1}_{{R}}={x}↔{x}{\cdot }_{{S}}{1}_{{R}}={x}\right)$
20 17 19 anbi12d ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to \left(\left({1}_{{R}}{\cdot }_{{R}}{x}={x}\wedge {x}{\cdot }_{{R}}{1}_{{R}}={x}\right)↔\left({1}_{{R}}{\cdot }_{{S}}{x}={x}\wedge {x}{\cdot }_{{S}}{1}_{{R}}={x}\right)\right)$
21 20 biimpa ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge \left({1}_{{R}}{\cdot }_{{R}}{x}={x}\wedge {x}{\cdot }_{{R}}{1}_{{R}}={x}\right)\right)\to \left({1}_{{R}}{\cdot }_{{S}}{x}={x}\wedge {x}{\cdot }_{{S}}{1}_{{R}}={x}\right)$
22 14 21 syldan ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {\mathrm{Base}}_{{R}}\right)\to \left({1}_{{R}}{\cdot }_{{S}}{x}={x}\wedge {x}{\cdot }_{{S}}{1}_{{R}}={x}\right)$
23 10 22 syldan ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {\mathrm{Base}}_{{S}}\right)\to \left({1}_{{R}}{\cdot }_{{S}}{x}={x}\wedge {x}{\cdot }_{{S}}{1}_{{R}}={x}\right)$
24 23 ralrimiva ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to \forall {x}\in {\mathrm{Base}}_{{S}}\phantom{\rule{.4em}{0ex}}\left({1}_{{R}}{\cdot }_{{S}}{x}={x}\wedge {x}{\cdot }_{{S}}{1}_{{R}}={x}\right)$
25 1 subrgring ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {S}\in \mathrm{Ring}$
26 eqid ${⊢}{\mathrm{Base}}_{{S}}={\mathrm{Base}}_{{S}}$
27 eqid ${⊢}{\cdot }_{{S}}={\cdot }_{{S}}$
28 eqid ${⊢}{1}_{{S}}={1}_{{S}}$
29 26 27 28 isringid ${⊢}{S}\in \mathrm{Ring}\to \left(\left({1}_{{R}}\in {\mathrm{Base}}_{{S}}\wedge \forall {x}\in {\mathrm{Base}}_{{S}}\phantom{\rule{.4em}{0ex}}\left({1}_{{R}}{\cdot }_{{S}}{x}={x}\wedge {x}{\cdot }_{{S}}{1}_{{R}}={x}\right)\right)↔{1}_{{S}}={1}_{{R}}\right)$
30 25 29 syl ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to \left(\left({1}_{{R}}\in {\mathrm{Base}}_{{S}}\wedge \forall {x}\in {\mathrm{Base}}_{{S}}\phantom{\rule{.4em}{0ex}}\left({1}_{{R}}{\cdot }_{{S}}{x}={x}\wedge {x}{\cdot }_{{S}}{1}_{{R}}={x}\right)\right)↔{1}_{{S}}={1}_{{R}}\right)$
31 6 24 30 mpbi2and ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {1}_{{S}}={1}_{{R}}$
32 31 2 syl6reqr