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 ⊢ 𝑂 = ( oppr ‘ 𝑅 )
Assertion opprsubrg ( SubRing ‘ 𝑅 ) = ( SubRing ‘ 𝑂 )

Proof

Step Hyp Ref Expression
1 opprsubrg.o ⊢ 𝑂 = ( oppr ‘ 𝑅 )
2 subrgrcl ⊢ ( 𝑥 ∈ ( SubRing ‘ 𝑅 ) → 𝑅 ∈ Ring )
3 subrgrcl ⊢ ( 𝑥 ∈ ( SubRing ‘ 𝑂 ) → 𝑂 ∈ Ring )
4 1 opprringb ⊢ ( 𝑅 ∈ Ring ↔ 𝑂 ∈ Ring )
5 3 4 sylibr ⊢ ( 𝑥 ∈ ( SubRing ‘ 𝑂 ) → 𝑅 ∈ Ring )
6 1 opprsubg ⊢ ( SubGrp ‘ 𝑅 ) = ( SubGrp ‘ 𝑂 )
7 6 a1i ⊢ ( 𝑅 ∈ Ring → ( SubGrp ‘ 𝑅 ) = ( SubGrp ‘ 𝑂 ) )
8 7 eleq2d ⊢ ( 𝑅 ∈ Ring → ( 𝑥 ∈ ( SubGrp ‘ 𝑅 ) ↔ 𝑥 ∈ ( SubGrp ‘ 𝑂 ) ) )
9 ralcom ⊢ ( ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ∈ 𝑥 ↔ ∀ 𝑧 ∈ 𝑥 ∀ 𝑦 ∈ 𝑥 ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ∈ 𝑥 )
10 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
11 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
12 eqid ⊢ ( .r ‘ 𝑂 ) = ( .r ‘ 𝑂 )
13 10 11 1 12 opprmul ⊢ ( 𝑧 ( .r ‘ 𝑂 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 )
14 13 eleq1i ⊢ ( ( 𝑧 ( .r ‘ 𝑂 ) 𝑦 ) ∈ 𝑥 ↔ ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ∈ 𝑥 )
15 14 2ralbii ⊢ ( ∀ 𝑧 ∈ 𝑥 ∀ 𝑦 ∈ 𝑥 ( 𝑧 ( .r ‘ 𝑂 ) 𝑦 ) ∈ 𝑥 ↔ ∀ 𝑧 ∈ 𝑥 ∀ 𝑦 ∈ 𝑥 ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ∈ 𝑥 )
16 9 15 bitr4i ⊢ ( ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ∈ 𝑥 ↔ ∀ 𝑧 ∈ 𝑥 ∀ 𝑦 ∈ 𝑥 ( 𝑧 ( .r ‘ 𝑂 ) 𝑦 ) ∈ 𝑥 )
17 16 a1i ⊢ ( 𝑅 ∈ Ring → ( ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ∈ 𝑥 ↔ ∀ 𝑧 ∈ 𝑥 ∀ 𝑦 ∈ 𝑥 ( 𝑧 ( .r ‘ 𝑂 ) 𝑦 ) ∈ 𝑥 ) )
18 8 17 3anbi13d ⊢ ( 𝑅 ∈ Ring → ( ( 𝑥 ∈ ( SubGrp ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ∈ 𝑥 ) ↔ ( 𝑥 ∈ ( SubGrp ‘ 𝑂 ) ∧ ( 1r ‘ 𝑅 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑦 ∈ 𝑥 ( 𝑧 ( .r ‘ 𝑂 ) 𝑦 ) ∈ 𝑥 ) ) )
19 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
20 10 19 11 issubrg2 ⊢ ( 𝑅 ∈ Ring → ( 𝑥 ∈ ( SubRing ‘ 𝑅 ) ↔ ( 𝑥 ∈ ( SubGrp ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ∈ 𝑥 ) ) )
21 1 10 opprbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 )
22 1 19 oppr1 ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑂 )
23 21 22 12 issubrg2 ⊢ ( 𝑂 ∈ Ring → ( 𝑥 ∈ ( SubRing ‘ 𝑂 ) ↔ ( 𝑥 ∈ ( SubGrp ‘ 𝑂 ) ∧ ( 1r ‘ 𝑅 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑦 ∈ 𝑥 ( 𝑧 ( .r ‘ 𝑂 ) 𝑦 ) ∈ 𝑥 ) ) )
24 4 23 sylbi ⊢ ( 𝑅 ∈ Ring → ( 𝑥 ∈ ( SubRing ‘ 𝑂 ) ↔ ( 𝑥 ∈ ( SubGrp ‘ 𝑂 ) ∧ ( 1r ‘ 𝑅 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑦 ∈ 𝑥 ( 𝑧 ( .r ‘ 𝑂 ) 𝑦 ) ∈ 𝑥 ) ) )
25 18 20 24 3bitr4d ⊢ ( 𝑅 ∈ Ring → ( 𝑥 ∈ ( SubRing ‘ 𝑅 ) ↔ 𝑥 ∈ ( SubRing ‘ 𝑂 ) ) )
26 2 5 25 pm5.21nii ⊢ ( 𝑥 ∈ ( SubRing ‘ 𝑅 ) ↔ 𝑥 ∈ ( SubRing ‘ 𝑂 ) )
27 26 eqriv ⊢ ( SubRing ‘ 𝑅 ) = ( SubRing ‘ 𝑂 )