Step |
Hyp |
Ref |
Expression |
1 |
|
subrgss.1 |
|- B = ( Base ` R ) |
2 |
|
id |
|- ( R e. Ring -> R e. Ring ) |
3 |
1
|
ressid |
|- ( R e. Ring -> ( R |`s B ) = R ) |
4 |
3 2
|
eqeltrd |
|- ( R e. Ring -> ( R |`s B ) e. Ring ) |
5 |
|
eqid |
|- ( 1r ` R ) = ( 1r ` R ) |
6 |
1 5
|
ringidcl |
|- ( R e. Ring -> ( 1r ` R ) e. B ) |
7 |
|
ssid |
|- B C_ B |
8 |
6 7
|
jctil |
|- ( R e. Ring -> ( B C_ B /\ ( 1r ` R ) e. B ) ) |
9 |
1 5
|
issubrg |
|- ( B e. ( SubRing ` R ) <-> ( ( R e. Ring /\ ( R |`s B ) e. Ring ) /\ ( B C_ B /\ ( 1r ` R ) e. B ) ) ) |
10 |
2 4 8 9
|
syl21anbrc |
|- ( R e. Ring -> B e. ( SubRing ` R ) ) |