This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem subrg1cl

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

		Ref	Expression
	Hypothesis	subrg1cl.a	$⊢ \underset{˙}{1} = 1_{R}$
	Assertion	subrg1cl	$⊢ A \in SubRing (R) \to \underset{˙}{1} \in A$

Step	Hyp	Ref	Expression
1		subrg1cl.a	$⊢ \underset{˙}{1} = 1_{R}$
2		eqid	$⊢ {Base}_{R} = {Base}_{R}$
3	2 1	issubrg	$⊢ A \in SubRing (R) \leftrightarrow ((R \in Ring \land R ↾_{𝑠} A \in Ring) \land (A \subseteq {Base}_{R} \land \underset{˙}{1} \in A))$
4	3	simprbi	$⊢ A \in SubRing (R) \to (A \subseteq {Base}_{R} \land \underset{˙}{1} \in A)$
5	4	simprd	$⊢ A \in SubRing (R) \to \underset{˙}{1} \in A$