Theorem srgidcl

Description: The unit 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 ∈ 𝐵 )