Theorem subrg1cl

Description: A subring contains the multiplicative identity. (Contributed by Stefan O'Rear, 27-Nov-2014)

	Ref	Expression
Hypothesis	subrg1cl.a	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	subrg1cl	$$⊢A\in \mathrm{SubRing}\left(R\right)\to \underset{\dot{}}{1}\in A$$

Proof

Step	Hyp	Ref	Expression
1		subrg1cl.a	$$⊢\underset{\dot{}}{1}=1_R$$
2		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
3	2 1	issubrg	$$⊢A\in \mathrm{SubRing}\left(R\right)\leftrightarrow \left(\left(R\in \mathrm{Ring}\wedge R{\upharpoonright }_{𝑠}A\in \mathrm{Ring}\right)\wedge \left(A\subseteq {\mathrm{Base}}_R\wedge \underset{\dot{}}{1}\in A\right)\right)$$
4	3	simprbi	$$⊢A\in \mathrm{SubRing}\left(R\right)\to \left(A\subseteq {\mathrm{Base}}_R\wedge \underset{\dot{}}{1}\in A\right)$$
5	4	simprd	$$⊢A\in \mathrm{SubRing}\left(R\right)\to \underset{\dot{}}{1}\in A$$