# 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 |`s A )`
subrg1.2
`|- .1. = ( 1r ` R )`
Assertion subrg1
`|- ( A e. ( SubRing ` R ) -> .1. = ( 1r ` S ) )`

### Proof

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