Metamath Proof Explorer

Theorem subrgnzr

Description: A subring of a nonzero ring is nonzero. (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Hypothesis subrgnzr.1 
|- S = ( R |`s A )
Assertion subrgnzr 
|- ( ( R e. NzRing /\ A e. ( SubRing ` R ) ) -> S e. NzRing )

Proof

Step Hyp Ref Expression
1 subrgnzr.1 
 |-  S = ( R |`s A )
2 1 subrgring 
 |-  ( A e. ( SubRing ` R ) -> S e. Ring )
3 2 adantl 
 |-  ( ( R e. NzRing /\ A e. ( SubRing ` R ) ) -> S e. Ring )
4 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
5 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
6 4 5 nzrnz 
 |-  ( R e. NzRing -> ( 1r ` R ) =/= ( 0g ` R ) )
7 6 adantr 
 |-  ( ( R e. NzRing /\ A e. ( SubRing ` R ) ) -> ( 1r ` R ) =/= ( 0g ` R ) )
8 1 4 subrg1 
 |-  ( A e. ( SubRing ` R ) -> ( 1r ` R ) = ( 1r ` S ) )
9 8 adantl 
 |-  ( ( R e. NzRing /\ A e. ( SubRing ` R ) ) -> ( 1r ` R ) = ( 1r ` S ) )
10 1 5 subrg0 
 |-  ( A e. ( SubRing ` R ) -> ( 0g ` R ) = ( 0g ` S ) )
11 10 adantl 
 |-  ( ( R e. NzRing /\ A e. ( SubRing ` R ) ) -> ( 0g ` R ) = ( 0g ` S ) )
12 7 9 11 3netr3d 
 |-  ( ( R e. NzRing /\ A e. ( SubRing ` R ) ) -> ( 1r ` S ) =/= ( 0g ` S ) )
13 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
14 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
15 13 14 isnzr 
 |-  ( S e. NzRing <-> ( S e. Ring /\ ( 1r ` S ) =/= ( 0g ` S ) ) )
16 3 12 15 sylanbrc 
 |-  ( ( R e. NzRing /\ A e. ( SubRing ` R ) ) -> S e. NzRing )