| Step |
Hyp |
Ref |
Expression |
| 1 |
|
0ringsubrg.1 |
|- B = ( Base ` R ) |
| 2 |
|
0ringsubrg.2 |
|- ( ph -> R e. Ring ) |
| 3 |
|
0ringsubrg.3 |
|- ( ph -> ( # ` B ) = 1 ) |
| 4 |
|
0ringsubrg.4 |
|- ( ph -> S e. ( SubRing ` R ) ) |
| 5 |
1
|
subrgss |
|- ( S e. ( SubRing ` R ) -> S C_ B ) |
| 6 |
4 5
|
syl |
|- ( ph -> S C_ B ) |
| 7 |
|
eqid |
|- ( 0g ` R ) = ( 0g ` R ) |
| 8 |
1 7
|
0ring |
|- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> B = { ( 0g ` R ) } ) |
| 9 |
2 3 8
|
syl2anc |
|- ( ph -> B = { ( 0g ` R ) } ) |
| 10 |
6 9
|
sseqtrd |
|- ( ph -> S C_ { ( 0g ` R ) } ) |
| 11 |
|
sssn |
|- ( S C_ { ( 0g ` R ) } <-> ( S = (/) \/ S = { ( 0g ` R ) } ) ) |
| 12 |
10 11
|
sylib |
|- ( ph -> ( S = (/) \/ S = { ( 0g ` R ) } ) ) |
| 13 |
|
eqid |
|- ( 1r ` R ) = ( 1r ` R ) |
| 14 |
13
|
subrg1cl |
|- ( S e. ( SubRing ` R ) -> ( 1r ` R ) e. S ) |
| 15 |
4 14
|
syl |
|- ( ph -> ( 1r ` R ) e. S ) |
| 16 |
|
n0i |
|- ( ( 1r ` R ) e. S -> -. S = (/) ) |
| 17 |
15 16
|
syl |
|- ( ph -> -. S = (/) ) |
| 18 |
12 17
|
orcnd |
|- ( ph -> S = { ( 0g ` R ) } ) |
| 19 |
18
|
fveq2d |
|- ( ph -> ( # ` S ) = ( # ` { ( 0g ` R ) } ) ) |
| 20 |
|
fvex |
|- ( 0g ` R ) e. _V |
| 21 |
|
hashsng |
|- ( ( 0g ` R ) e. _V -> ( # ` { ( 0g ` R ) } ) = 1 ) |
| 22 |
20 21
|
ax-mp |
|- ( # ` { ( 0g ` R ) } ) = 1 |
| 23 |
19 22
|
eqtrdi |
|- ( ph -> ( # ` S ) = 1 ) |