This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC ALGEBRAIC STRUCTURES Rings Semirings srgidcl
Description: The unity element of a semiring belongs to the base set of the semiring.
(Contributed by NM , 27-Aug-2011) (Revised by Mario Carneiro , 27-Dec-2014) (Revised by Thierry Arnoux , 1-Apr-2018)
Ref
Expression
Hypotheses
srgidcl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
srgidcl.u ⊢ 1 = ( 1r ‘ 𝑅 )
Assertion
srgidcl ⊢ ( 𝑅 ∈ SRing → 1 ∈ 𝐵 )
Proof
Step
Hyp
Ref
Expression
1
srgidcl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2
srgidcl.u ⊢ 1 = ( 1r ‘ 𝑅 )
3
eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
4
3
srgmgp ⊢ ( 𝑅 ∈ SRing → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
5
3 1
mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
6
3 2
ringidval ⊢ 1 = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
7
5 6
mndidcl ⊢ ( ( mulGrp ‘ 𝑅 ) ∈ Mnd → 1 ∈ 𝐵 )
8
4 7
syl ⊢ ( 𝑅 ∈ SRing → 1 ∈ 𝐵 )