Theorem subrgnzr

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

	Ref	Expression
Hypothesis	subrgnzr.1	⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
Assertion	subrgnzr	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) → 𝑆 ∈ NzRing )

Proof

Step	Hyp	Ref	Expression
1		subrgnzr.1	⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
2	1	subrgring	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 ∈ Ring )
3	2	adantl	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) → 𝑆 ∈ Ring )
4		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
5		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
6	4 5	nzrnz	⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
7	6	adantr	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
8	1 4	subrg1	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑆 ) )
9	8	adantl	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) → ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑆 ) )
10	1 5	subrg0	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑆 ) )
11	10	adantl	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑆 ) )
12	7 9 11	3netr3d	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) → ( 1r ‘ 𝑆 ) ≠ ( 0g ‘ 𝑆 ) )
13		eqid	⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
14		eqid	⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
15	13 14	isnzr	⊢ ( 𝑆 ∈ NzRing ↔ ( 𝑆 ∈ Ring ∧ ( 1r ‘ 𝑆 ) ≠ ( 0g ‘ 𝑆 ) ) )
16	3 12 15	sylanbrc	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) → 𝑆 ∈ NzRing )