Metamath Proof Explorer


Theorem subrgacs

Description: Closure property of subrings. (Contributed by Stefan O'Rear, 12-Sep-2015)

Ref Expression
Hypothesis subrgacs.b B=BaseR
Assertion subrgacs RRingSubRingRACSB

Proof

Step Hyp Ref Expression
1 subrgacs.b B=BaseR
2 eqid mulGrpR=mulGrpR
3 2 issubrg3 RRingxSubRingRxSubGrpRxSubMndmulGrpR
4 elin xSubGrpRSubMndmulGrpRxSubGrpRxSubMndmulGrpR
5 3 4 bitr4di RRingxSubRingRxSubGrpRSubMndmulGrpR
6 5 eqrdv RRingSubRingR=SubGrpRSubMndmulGrpR
7 1 fvexi BV
8 mreacs BVACSBMoore𝒫B
9 7 8 mp1i RRingACSBMoore𝒫B
10 ringgrp RRingRGrp
11 1 subgacs RGrpSubGrpRACSB
12 10 11 syl RRingSubGrpRACSB
13 2 ringmgp RRingmulGrpRMnd
14 2 1 mgpbas B=BasemulGrpR
15 14 submacs mulGrpRMndSubMndmulGrpRACSB
16 13 15 syl RRingSubMndmulGrpRACSB
17 mreincl ACSBMoore𝒫BSubGrpRACSBSubMndmulGrpRACSBSubGrpRSubMndmulGrpRACSB
18 9 12 16 17 syl3anc RRingSubGrpRSubMndmulGrpRACSB
19 6 18 eqeltrd RRingSubRingRACSB