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 ) )