Theorem subrngsubg

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

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

Proof

Step	Hyp	Ref	Expression
1		subrngrcl	Could not format ( A e. ( SubRng ` R ) -> R e. Rng ) : No typesetting found for |- ( A e. ( SubRng ` R ) -> R e. Rng ) with typecode |-
2		rnggrp	$$⊢R\in \mathrm{Rng}\to R\in \mathrm{Grp}$$
3	1 2	syl	Could not format ( A e. ( SubRng ` R ) -> R e. Grp ) : No typesetting found for |- ( A e. ( SubRng ` R ) -> R e. Grp ) with typecode |-
4		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
5	4	subrngss	Could not format ( A e. ( SubRng ` R ) -> A C_ ( Base ` R ) ) : No typesetting found for |- ( A e. ( SubRng ` R ) -> A C_ ( Base ` R ) ) with typecode |-
6		eqid	$$⊢R{\upharpoonright }_{𝑠}A=R{\upharpoonright }_{𝑠}A$$
7	6	subrngrng	Could not format ( A e. ( SubRng ` R ) -> ( R |`s A ) e. Rng ) : No typesetting found for |- ( A e. ( SubRng ` R ) -> ( R |`s A ) e. Rng ) with typecode |-
8		rnggrp	$$⊢R{\upharpoonright }_{𝑠}A\in \mathrm{Rng}\to R{\upharpoonright }_{𝑠}A\in \mathrm{Grp}$$
9	7 8	syl	Could not format ( A e. ( SubRng ` R ) -> ( R |`s A ) e. Grp ) : No typesetting found for |- ( A e. ( SubRng ` R ) -> ( R |`s A ) e. Grp ) with typecode |-
10	4	issubg	$$⊢A\in \mathrm{SubGrp}\left(R\right)\leftrightarrow \left(R\in \mathrm{Grp}\wedge A\subseteq {\mathrm{Base}}_R\wedge R{\upharpoonright }_{𝑠}A\in \mathrm{Grp}\right)$$
11	3 5 9 10	syl3anbrc	Could not format ( A e. ( SubRng ` R ) -> A e. ( SubGrp ` R ) ) : No typesetting found for |- ( A e. ( SubRng ` R ) -> A e. ( SubGrp ` R ) ) with typecode |-