subrgsubrng

Description: A subring of a unital ring is a subring of a non-unital ring. (Contributed by AV, 30-Mar-2025)

		Ref	Expression
	Assertion	subrgsubrng	Could not format assertion : No typesetting found for \|- ( A e. ( SubRing ` R ) -> A e. ( SubRng ` R ) ) with typecode \|-

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{R} = {Base}_{R}$
2		eqid	$⊢ 1_{R} = 1_{R}$
3	1 2	issubrg	$⊢ A \in SubRing (R) \leftrightarrow ((R \in Ring \land R ↾_{𝑠} A \in Ring) \land (A \subseteq {Base}_{R} \land 1_{R} \in A))$
4		ringrng	$⊢ R \in Ring \to R \in Rng$
5	4	ad2antrr	$⊢ ((R \in Ring \land R ↾_{𝑠} A \in Ring) \land (A \subseteq {Base}_{R} \land 1_{R} \in A)) \to R \in Rng$
6		ringrng	$⊢ R ↾_{𝑠} A \in Ring \to R ↾_{𝑠} A \in Rng$
7	6	ad2antlr	$⊢ ((R \in Ring \land R ↾_{𝑠} A \in Ring) \land (A \subseteq {Base}_{R} \land 1_{R} \in A)) \to R ↾_{𝑠} A \in Rng$
8		simprl	$⊢ ((R \in Ring \land R ↾_{𝑠} A \in Ring) \land (A \subseteq {Base}_{R} \land 1_{R} \in A)) \to A \subseteq {Base}_{R}$
9	1	issubrng	Could not format ( A e. ( SubRng ` R ) <-> ( R e. Rng /\ ( R \|`s A ) e. Rng /\ A C_ ( Base ` R ) ) ) : No typesetting found for \|- ( A e. ( SubRng ` R ) <-> ( R e. Rng /\ ( R \|`s A ) e. Rng /\ A C_ ( Base ` R ) ) ) with typecode \|-
10	5 7 8 9	syl3anbrc	Could not format ( ( ( R e. Ring /\ ( R \|`s A ) e. Ring ) /\ ( A C_ ( Base ` R ) /\ ( 1r ` R ) e. A ) ) -> A e. ( SubRng ` R ) ) : No typesetting found for \|- ( ( ( R e. Ring /\ ( R \|`s A ) e. Ring ) /\ ( A C_ ( Base ` R ) /\ ( 1r ` R ) e. A ) ) -> A e. ( SubRng ` R ) ) with typecode \|-
11	3 10	sylbi	Could not format ( A e. ( SubRing ` R ) -> A e. ( SubRng ` R ) ) : No typesetting found for \|- ( A e. ( SubRing ` R ) -> A e. ( SubRng ` R ) ) with typecode \|-

Metamath Proof Explorer