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 1 ˙ = 1 R
Assertion subrg1 A SubRing R 1 ˙ = 1 S

Proof

Step Hyp Ref Expression
1 subrg1.1 S = R 𝑠 A
2 subrg1.2 1 ˙ = 1 R
3 eqid 1 R = 1 R
4 3 subrg1cl A SubRing R 1 R A
5 1 subrgbas A SubRing R A = Base S
6 4 5 eleqtrd A SubRing R 1 R Base S
7 eqid Base R = Base R
8 7 subrgss A SubRing R A Base R
9 5 8 eqsstrrd A SubRing R Base S Base R
10 9 sselda A SubRing R x Base S x Base R
11 subrgrcl A SubRing R R Ring
12 eqid R = R
13 7 12 3 ringidmlem R Ring x Base R 1 R R x = x x R 1 R = x
14 11 13 sylan A SubRing R x Base R 1 R R x = x x R 1 R = x
15 1 12 ressmulr A SubRing R R = S
16 15 oveqd A SubRing R 1 R R x = 1 R S x
17 16 eqeq1d A SubRing R 1 R R x = x 1 R S x = x
18 15 oveqd A SubRing R x R 1 R = x S 1 R
19 18 eqeq1d A SubRing R x R 1 R = x x S 1 R = x
20 17 19 anbi12d A SubRing R 1 R R x = x x R 1 R = x 1 R S x = x x S 1 R = x
21 20 biimpa A SubRing R 1 R R x = x x R 1 R = x 1 R S x = x x S 1 R = x
22 14 21 syldan A SubRing R x Base R 1 R S x = x x S 1 R = x
23 10 22 syldan A SubRing R x Base S 1 R S x = x x S 1 R = x
24 23 ralrimiva A SubRing R x Base S 1 R S x = x x S 1 R = x
25 1 subrgring A SubRing R S Ring
26 eqid Base S = Base S
27 eqid S = S
28 eqid 1 S = 1 S
29 26 27 28 isringid S Ring 1 R Base S x Base S 1 R S x = x x S 1 R = x 1 S = 1 R
30 25 29 syl A SubRing R 1 R Base S x Base S 1 R S x = x x S 1 R = x 1 S = 1 R
31 6 24 30 mpbi2and A SubRing R 1 S = 1 R
32 2 31 eqtr4id A SubRing R 1 ˙ = 1 S