Database
BASIC ALGEBRAIC STRUCTURES
Rings
Subrings
Subrings of non-unital rings
subrngsubg
Next ⟩
subrngringnsg
Metamath Proof Explorer
Ascii
Unicode
Theorem
subrngsubg
Description:
A subring is a subgroup.
(Contributed by
AV
, 14-Feb-2025)
Ref
Expression
Assertion
subrngsubg
⊢
A
∈
SubRng
⁡
R
→
A
∈
SubGrp
⁡
R
Proof
Step
Hyp
Ref
Expression
1
subrngrcl
⊢
A
∈
SubRng
⁡
R
→
R
∈
Rng
2
rnggrp
⊢
R
∈
Rng
→
R
∈
Grp
3
1
2
syl
⊢
A
∈
SubRng
⁡
R
→
R
∈
Grp
4
eqid
⊢
Base
R
=
Base
R
5
4
subrngss
⊢
A
∈
SubRng
⁡
R
→
A
⊆
Base
R
6
eqid
⊢
R
↾
𝑠
A
=
R
↾
𝑠
A
7
6
subrngrng
⊢
A
∈
SubRng
⁡
R
→
R
↾
𝑠
A
∈
Rng
8
rnggrp
⊢
R
↾
𝑠
A
∈
Rng
→
R
↾
𝑠
A
∈
Grp
9
7
8
syl
⊢
A
∈
SubRng
⁡
R
→
R
↾
𝑠
A
∈
Grp
10
4
issubg
⊢
A
∈
SubGrp
⁡
R
↔
R
∈
Grp
∧
A
⊆
Base
R
∧
R
↾
𝑠
A
∈
Grp
11
3
5
9
10
syl3anbrc
⊢
A
∈
SubRng
⁡
R
→
A
∈
SubGrp
⁡
R