This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐴 )
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 )