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

Metamath Proof Explorer

Theorem subrngrng

Description: A subring is a non-unital ring. (Contributed by AV, 14-Feb-2025)

		Ref	Expression
	Hypothesis	subrngrng.1	$⊢ S = R ↾_{𝑠} A$
	Assertion	subrngrng	$⊢ A \in SubRng (R) \to S \in Rng$

Step	Hyp	Ref	Expression
1		subrngrng.1	$⊢ S = R ↾_{𝑠} A$
2		simp2	$⊢ (R \in Rng \land R ↾_{𝑠} A \in Rng \land A \subseteq {Base}_{R}) \to R ↾_{𝑠} A \in Rng$
3		eqid	$⊢ {Base}_{R} = {Base}_{R}$
4	3	issubrng	$⊢ A \in SubRng (R) \leftrightarrow (R \in Rng \land R ↾_{𝑠} A \in Rng \land A \subseteq {Base}_{R})$
5	1	eleq1i	$⊢ S \in Rng \leftrightarrow R ↾_{𝑠} A \in Rng$
6	2 4 5	3imtr4i	$⊢ A \in SubRng (R) \to S \in Rng$