Theorem ringidcl

Description: The unity element of a ring belongs to the base set of the ring. (Contributed by FL, 12-Feb-2010) (Revised by NM, 27-Aug-2011) (Revised by Mario Carneiro, 27-Dec-2014)

	Ref	Expression
Hypotheses	ringidcl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	ringidcl.u	⊢ 1 = ( 1r ‘ 𝑅 )
Assertion	ringidcl	⊢ ( 𝑅 ∈ Ring → 1 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ringidcl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		ringidcl.u	⊢ 1 = ( 1r ‘ 𝑅 )
3		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
4	3	ringmgp	⊢ ( 𝑅 ∈ Ring → ( 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	⊢ ( 𝑅 ∈ Ring → 1 ∈ 𝐵 )