Metamath Proof Explorer

Theorem opprsubrng

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

Ref Expression
Hypothesis opprsubrng.o ⊢ O = opp r ⁡ R
Assertion opprsubrng ⊢ SubRng ⁡ R = SubRng ⁡ O

Proof

Step Hyp Ref Expression
1 opprsubrng.o ⊢ O = opp r ⁡ R
2 subrngrcl ⊢ x ∈ SubRng ⁡ R → R ∈ Rng
3 subrngrcl ⊢ x ∈ SubRng ⁡ O → O ∈ Rng
4 1 opprrngb ⊢ R ∈ Rng ↔ O ∈ Rng
5 3 4 sylibr ⊢ x ∈ SubRng ⁡ O → R ∈ Rng
6 1 opprsubg ⊢ SubGrp ⁡ R = SubGrp ⁡ O
7 6 a1i ⊢ R ∈ Rng → SubGrp ⁡ R = SubGrp ⁡ O
8 7 eleq2d ⊢ R ∈ Rng → x ∈ SubGrp ⁡ R ↔ x ∈ SubGrp ⁡ O
9 ralcom ⊢ ∀ z ∈ x ∀ y ∈ x z ⋅ R y ∈ x ↔ ∀ y ∈ x ∀ z ∈ x z ⋅ R y ∈ x
10 eqid ⊢ Base R = Base R
11 eqid ⊢ ⋅ R = ⋅ R
12 eqid ⊢ ⋅ O = ⋅ O
13 10 11 1 12 opprmul ⊢ y ⋅ O z = z ⋅ R y
14 13 eleq1i ⊢ y ⋅ O z ∈ x ↔ z ⋅ R y ∈ x
15 14 2ralbii ⊢ ∀ y ∈ x ∀ z ∈ x y ⋅ O z ∈ x ↔ ∀ y ∈ x ∀ z ∈ x z ⋅ R y ∈ x
16 9 15 bitr4i ⊢ ∀ z ∈ x ∀ y ∈ x z ⋅ R y ∈ x ↔ ∀ y ∈ x ∀ z ∈ x y ⋅ O z ∈ x
17 16 a1i ⊢ R ∈ Rng → ∀ z ∈ x ∀ y ∈ x z ⋅ R y ∈ x ↔ ∀ y ∈ x ∀ z ∈ x y ⋅ O z ∈ x
18 8 17 anbi12d ⊢ R ∈ Rng → x ∈ SubGrp ⁡ R ∧ ∀ z ∈ x ∀ y ∈ x z ⋅ R y ∈ x ↔ x ∈ SubGrp ⁡ O ∧ ∀ y ∈ x ∀ z ∈ x y ⋅ O z ∈ x
19 10 11 issubrng2 ⊢ R ∈ Rng → x ∈ SubRng ⁡ R ↔ x ∈ SubGrp ⁡ R ∧ ∀ z ∈ x ∀ y ∈ x z ⋅ R y ∈ x
20 1 10 opprbas ⊢ Base R = Base O
21 20 12 issubrng2 ⊢ O ∈ Rng → x ∈ SubRng ⁡ O ↔ x ∈ SubGrp ⁡ O ∧ ∀ y ∈ x ∀ z ∈ x y ⋅ O z ∈ x
22 4 21 sylbi ⊢ R ∈ Rng → x ∈ SubRng ⁡ O ↔ x ∈ SubGrp ⁡ O ∧ ∀ y ∈ x ∀ z ∈ x y ⋅ O z ∈ x
23 18 19 22 3bitr4d ⊢ R ∈ Rng → x ∈ SubRng ⁡ R ↔ x ∈ SubRng ⁡ O
24 2 5 23 pm5.21nii ⊢ x ∈ SubRng ⁡ R ↔ x ∈ SubRng ⁡ O
25 24 eqriv ⊢ SubRng ⁡ R = SubRng ⁡ O