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