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 \in NzRing \land A \in SubRing (R)) \to S \in NzRing$

Step	Hyp	Ref	Expression
1		subrgnzr.1	$⊢ S = R ↾_{𝑠} A$
2	1	subrgring	$⊢ A \in SubRing (R) \to S \in Ring$
3	2	adantl	$⊢ (R \in NzRing \land A \in SubRing (R)) \to S \in Ring$
4		eqid	$⊢ 1_{R} = 1_{R}$
5		eqid	$⊢ 0_{R} = 0_{R}$
6	4 5	nzrnz	$⊢ R \in NzRing \to 1_{R} \neq 0_{R}$
7	6	adantr	$⊢ (R \in NzRing \land A \in SubRing (R)) \to 1_{R} \neq 0_{R}$
8	1 4	subrg1	$⊢ A \in SubRing (R) \to 1_{R} = 1_{S}$
9	8	adantl	$⊢ (R \in NzRing \land A \in SubRing (R)) \to 1_{R} = 1_{S}$
10	1 5	subrg0	$⊢ A \in SubRing (R) \to 0_{R} = 0_{S}$
11	10	adantl	$⊢ (R \in NzRing \land A \in SubRing (R)) \to 0_{R} = 0_{S}$
12	7 9 11	3netr3d	$⊢ (R \in NzRing \land A \in SubRing (R)) \to 1_{S} \neq 0_{S}$
13		eqid	$⊢ 1_{S} = 1_{S}$
14		eqid	$⊢ 0_{S} = 0_{S}$
15	13 14	isnzr	$⊢ S \in NzRing \leftrightarrow (S \in Ring \land 1_{S} \neq 0_{S})$
16	3 12 15	sylanbrc	$⊢ (R \in NzRing \land A \in SubRing (R)) \to S \in NzRing$

Metamath Proof Explorer