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 𝑠 A
Assertion subrgnzr R NzRing A SubRing R S NzRing

Proof

Step Hyp Ref Expression
1 subrgnzr.1 S = R 𝑠 A
2 1 subrgring A SubRing R S Ring
3 2 adantl R NzRing A SubRing R S Ring
4 eqid 1 R = 1 R
5 eqid 0 R = 0 R
6 4 5 nzrnz R NzRing 1 R 0 R
7 6 adantr R NzRing A SubRing R 1 R 0 R
8 1 4 subrg1 A SubRing R 1 R = 1 S
9 8 adantl R NzRing A SubRing R 1 R = 1 S
10 1 5 subrg0 A SubRing R 0 R = 0 S
11 10 adantl R NzRing A SubRing R 0 R = 0 S
12 7 9 11 3netr3d R NzRing A SubRing R 1 S 0 S
13 eqid 1 S = 1 S
14 eqid 0 S = 0 S
15 13 14 isnzr S NzRing S Ring 1 S 0 S
16 3 12 15 sylanbrc R NzRing A SubRing R S NzRing