Theorem opprsubrng

Description: Being a subring is a symmetric property. (Contributed by AV, 15-Feb-2025)

	Ref	Expression
Hypothesis	opprsubrng.o	$$⊢O={opp}_r\left(R\right)$$
Assertion	opprsubrng	Could not format assertion : No typesetting found for |- ( SubRng ` R ) = ( SubRng ` O ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		opprsubrng.o	$$⊢O={opp}_r\left(R\right)$$
2		subrngrcl	Could not format ( x e. ( SubRng ` R ) -> R e. Rng ) : No typesetting found for |- ( x e. ( SubRng ` R ) -> R e. Rng ) with typecode |-
3		subrngrcl	Could not format ( x e. ( SubRng ` O ) -> O e. Rng ) : No typesetting found for |- ( x e. ( SubRng ` O ) -> O e. Rng ) with typecode |-
4	1	opprrngb	$$⊢R\in \mathrm{Rng}\leftrightarrow O\in \mathrm{Rng}$$
5	3 4	sylibr	Could not format ( x e. ( SubRng ` O ) -> R e. Rng ) : No typesetting found for |- ( x e. ( SubRng ` O ) -> R e. Rng ) with typecode |-
6	1	opprsubg	$$⊢\mathrm{SubGrp}\left(R\right)=\mathrm{SubGrp}\left(O\right)$$
7	6	a1i	$$⊢R\in \mathrm{Rng}\to \mathrm{SubGrp}\left(R\right)=\mathrm{SubGrp}\left(O\right)$$
8	7	eleq2d	$$⊢R\in \mathrm{Rng}\to \left(x\in \mathrm{SubGrp}\left(R\right)\leftrightarrow x\in \mathrm{SubGrp}\left(O\right)\right)$$
9		ralcom	$$⊢\forall z\in x\forall y\in xz{\cdot }_{R}y\in x\leftrightarrow \forall y\in x\forall z\in xz{\cdot }_{R}y\in x$$
10		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
11		eqid	$$⊢{\cdot }_R={\cdot }_R$$
12		eqid	$$⊢{\cdot }_O={\cdot }_O$$
13	10 11 1 12	opprmul	$$⊢y{\cdot }_{O}z=z{\cdot }_{R}y$$
14	13	eleq1i	$$⊢y{\cdot }_{O}z\in x\leftrightarrow z{\cdot }_{R}y\in x$$
15	14	2ralbii	$$⊢\forall y\in x\forall z\in xy{\cdot }_{O}z\in x\leftrightarrow \forall y\in x\forall z\in xz{\cdot }_{R}y\in x$$
16	9 15	bitr4i	$$⊢\forall z\in x\forall y\in xz{\cdot }_{R}y\in x\leftrightarrow \forall y\in x\forall z\in xy{\cdot }_{O}z\in x$$
17	16	a1i	$$⊢R\in \mathrm{Rng}\to \left(\forall z\in x\forall y\in xz{\cdot }_{R}y\in x\leftrightarrow \forall y\in x\forall z\in xy{\cdot }_{O}z\in x\right)$$
18	8 17	anbi12d	$$⊢R\in \mathrm{Rng}\to \left(\left(x\in \mathrm{SubGrp}\left(R\right)\wedge \forall z\in x\forall y\in xz{\cdot }_{R}y\in x\right)\leftrightarrow \left(x\in \mathrm{SubGrp}\left(O\right)\wedge \forall y\in x\forall z\in xy{\cdot }_{O}z\in x\right)\right)$$
19	10 11	issubrng2	Could not format ( R e. Rng -> ( x e. ( SubRng ` R ) <-> ( x e. ( SubGrp ` R ) /\ A. z e. x A. y e. x ( z ( .r ` R ) y ) e. x ) ) ) : No typesetting found for |- ( R e. Rng -> ( x e. ( SubRng ` R ) <-> ( x e. ( SubGrp ` R ) /\ A. z e. x A. y e. x ( z ( .r ` R ) y ) e. x ) ) ) with typecode |-
20	1 10	opprbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_O$$
21	20 12	issubrng2	Could not format ( O e. Rng -> ( x e. ( SubRng ` O ) <-> ( x e. ( SubGrp ` O ) /\ A. y e. x A. z e. x ( y ( .r ` O ) z ) e. x ) ) ) : No typesetting found for |- ( O e. Rng -> ( x e. ( SubRng ` O ) <-> ( x e. ( SubGrp ` O ) /\ A. y e. x A. z e. x ( y ( .r ` O ) z ) e. x ) ) ) with typecode |-
22	4 21	sylbi	Could not format ( R e. Rng -> ( x e. ( SubRng ` O ) <-> ( x e. ( SubGrp ` O ) /\ A. y e. x A. z e. x ( y ( .r ` O ) z ) e. x ) ) ) : No typesetting found for |- ( R e. Rng -> ( x e. ( SubRng ` O ) <-> ( x e. ( SubGrp ` O ) /\ A. y e. x A. z e. x ( y ( .r ` O ) z ) e. x ) ) ) with typecode |-
23	18 19 22	3bitr4d	Could not format ( R e. Rng -> ( x e. ( SubRng ` R ) <-> x e. ( SubRng ` O ) ) ) : No typesetting found for |- ( R e. Rng -> ( x e. ( SubRng ` R ) <-> x e. ( SubRng ` O ) ) ) with typecode |-
24	2 5 23	pm5.21nii	Could not format ( x e. ( SubRng ` R ) <-> x e. ( SubRng ` O ) ) : No typesetting found for |- ( x e. ( SubRng ` R ) <-> x e. ( SubRng ` O ) ) with typecode |-
25	24	eqriv	Could not format ( SubRng ` R ) = ( SubRng ` O ) : No typesetting found for |- ( SubRng ` R ) = ( SubRng ` O ) with typecode |-