Description: A subring always has the same additive identity. (Contributed by Stefan O'Rear, 27-Nov-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | subrg0.1 | |- S = ( R |`s A ) |
|
subrg0.2 | |- .0. = ( 0g ` R ) |
||
Assertion | subrg0 | |- ( A e. ( SubRing ` R ) -> .0. = ( 0g ` S ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | subrg0.1 | |- S = ( R |`s A ) |
|
2 | subrg0.2 | |- .0. = ( 0g ` R ) |
|
3 | subrgsubg | |- ( A e. ( SubRing ` R ) -> A e. ( SubGrp ` R ) ) |
|
4 | 1 2 | subg0 | |- ( A e. ( SubGrp ` R ) -> .0. = ( 0g ` S ) ) |
5 | 3 4 | syl | |- ( A e. ( SubRing ` R ) -> .0. = ( 0g ` S ) ) |