Database
BASIC ALGEBRAIC STRUCTURES
Rings
Subrings
Subrings of non-unital rings
subrngbas
Next ⟩
subrng0
Metamath Proof Explorer
Ascii
Unicode
Theorem
subrngbas
Description:
Base set of a subring structure.
(Contributed by
AV
, 14-Feb-2025)
Ref
Expression
Hypothesis
subrng0.1
⊢
S
=
R
↾
𝑠
A
Assertion
subrngbas
⊢
A
∈
SubRng
⁡
R
→
A
=
Base
S
Proof
Step
Hyp
Ref
Expression
1
subrng0.1
⊢
S
=
R
↾
𝑠
A
2
subrngsubg
⊢
A
∈
SubRng
⁡
R
→
A
∈
SubGrp
⁡
R
3
1
subgbas
⊢
A
∈
SubGrp
⁡
R
→
A
=
Base
S
4
2
3
syl
⊢
A
∈
SubRng
⁡
R
→
A
=
Base
S