Metamath Proof Explorer


Theorem subrgacs

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

Ref Expression
Hypothesis subrgacs.b B = Base R
Assertion subrgacs R Ring SubRing R ACS B

Proof

Step Hyp Ref Expression
1 subrgacs.b B = Base R
2 eqid mulGrp R = mulGrp R
3 2 issubrg3 R Ring x SubRing R x SubGrp R x SubMnd mulGrp R
4 elin x SubGrp R SubMnd mulGrp R x SubGrp R x SubMnd mulGrp R
5 3 4 bitr4di R Ring x SubRing R x SubGrp R SubMnd mulGrp R
6 5 eqrdv R Ring SubRing R = SubGrp R SubMnd mulGrp R
7 1 fvexi B V
8 mreacs B V ACS B Moore 𝒫 B
9 7 8 mp1i R Ring ACS B Moore 𝒫 B
10 ringgrp R Ring R Grp
11 1 subgacs R Grp SubGrp R ACS B
12 10 11 syl R Ring SubGrp R ACS B
13 2 ringmgp R Ring mulGrp R Mnd
14 2 1 mgpbas B = Base mulGrp R
15 14 submacs mulGrp R Mnd SubMnd mulGrp R ACS B
16 13 15 syl R Ring SubMnd mulGrp R ACS B
17 mreincl ACS B Moore 𝒫 B SubGrp R ACS B SubMnd mulGrp R ACS B SubGrp R SubMnd mulGrp R ACS B
18 9 12 16 17 syl3anc R Ring SubGrp R SubMnd mulGrp R ACS B
19 6 18 eqeltrd R Ring SubRing R ACS B