Metamath Proof Explorer

Theorem opprsubrg

Description: Being a subring is a symmetric property. (Contributed by Mario Carneiro, 6-Dec-2014)

Ref Expression
Hypothesis opprsubrg.o ⊢ O = opp r ⁡ R
Assertion opprsubrg ⊢ SubRing ⁡ R = SubRing ⁡ O

Proof

Step Hyp Ref Expression
1 opprsubrg.o ⊢ O = opp r ⁡ R
2 subrgrcl ⊢ x ∈ SubRing ⁡ R → R ∈ Ring
3 subrgrcl ⊢ x ∈ SubRing ⁡ O → O ∈ Ring
4 1 opprringb ⊢ R ∈ Ring ↔ O ∈ Ring
5 3 4 sylibr ⊢ x ∈ SubRing ⁡ O → R ∈ Ring
6 1 opprsubg ⊢ SubGrp ⁡ R = SubGrp ⁡ O
7 6 a1i ⊢ R ∈ Ring → SubGrp ⁡ R = SubGrp ⁡ O
8 7 eleq2d ⊢ R ∈ Ring → x ∈ SubGrp ⁡ R ↔ x ∈ SubGrp ⁡ O
9 ralcom ⊢ ∀ y ∈ x ∀ z ∈ x y ⋅ R z ∈ x ↔ ∀ z ∈ x ∀ y ∈ x y ⋅ R z ∈ x
10 eqid ⊢ Base R = Base R
11 eqid ⊢ ⋅ R = ⋅ R
12 eqid ⊢ ⋅ O = ⋅ O
13 10 11 1 12 opprmul ⊢ z ⋅ O y = y ⋅ R z
14 13 eleq1i ⊢ z ⋅ O y ∈ x ↔ y ⋅ R z ∈ x
15 14 2ralbii ⊢ ∀ z ∈ x ∀ y ∈ x z ⋅ O y ∈ x ↔ ∀ z ∈ x ∀ y ∈ x y ⋅ R z ∈ x
16 9 15 bitr4i ⊢ ∀ y ∈ x ∀ z ∈ x y ⋅ R z ∈ x ↔ ∀ z ∈ x ∀ y ∈ x z ⋅ O y ∈ x
17 16 a1i ⊢ R ∈ Ring → ∀ y ∈ x ∀ z ∈ x y ⋅ R z ∈ x ↔ ∀ z ∈ x ∀ y ∈ x z ⋅ O y ∈ x
18 8 17 3anbi13d ⊢ R ∈ Ring → x ∈ SubGrp ⁡ R ∧ 1 R ∈ x ∧ ∀ y ∈ x ∀ z ∈ x y ⋅ R z ∈ x ↔ x ∈ SubGrp ⁡ O ∧ 1 R ∈ x ∧ ∀ z ∈ x ∀ y ∈ x z ⋅ O y ∈ x
19 eqid ⊢ 1 R = 1 R
20 10 19 11 issubrg2 ⊢ R ∈ Ring → x ∈ SubRing ⁡ R ↔ x ∈ SubGrp ⁡ R ∧ 1 R ∈ x ∧ ∀ y ∈ x ∀ z ∈ x y ⋅ R z ∈ x
21 1 10 opprbas ⊢ Base R = Base O
22 1 19 oppr1 ⊢ 1 R = 1 O
23 21 22 12 issubrg2 ⊢ O ∈ Ring → x ∈ SubRing ⁡ O ↔ x ∈ SubGrp ⁡ O ∧ 1 R ∈ x ∧ ∀ z ∈ x ∀ y ∈ x z ⋅ O y ∈ x
24 4 23 sylbi ⊢ R ∈ Ring → x ∈ SubRing ⁡ O ↔ x ∈ SubGrp ⁡ O ∧ 1 R ∈ x ∧ ∀ z ∈ x ∀ y ∈ x z ⋅ O y ∈ x
25 18 20 24 3bitr4d ⊢ R ∈ Ring → x ∈ SubRing ⁡ R ↔ x ∈ SubRing ⁡ O
26 2 5 25 pm5.21nii ⊢ x ∈ SubRing ⁡ R ↔ x ∈ SubRing ⁡ O
27 26 eqriv ⊢ SubRing ⁡ R = SubRing ⁡ O