Database
BASIC ALGEBRAIC STRUCTURES
Ideals
Nonzero rings and zero rings
subrgnzr
Next ⟩
0ringnnzr
Metamath Proof Explorer
Ascii
Unicode
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