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 e. Ring -> ( SubRing ` R ) e. ( ACS ` B ) )

Proof

Step Hyp Ref Expression
1 subrgacs.b 
 |-  B = ( Base ` R )
2 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
3 2 issubrg3 
 |-  ( R e. Ring -> ( x e. ( SubRing ` R ) <-> ( x e. ( SubGrp ` R ) /\ x e. ( SubMnd ` ( mulGrp ` R ) ) ) ) )
4 elin 
 |-  ( x e. ( ( SubGrp ` R ) i^i ( SubMnd ` ( mulGrp ` R ) ) ) <-> ( x e. ( SubGrp ` R ) /\ x e. ( SubMnd ` ( mulGrp ` R ) ) ) )
5 3 4 bitr4di 
 |-  ( R e. Ring -> ( x e. ( SubRing ` R ) <-> x e. ( ( SubGrp ` R ) i^i ( SubMnd ` ( mulGrp ` R ) ) ) ) )
6 5 eqrdv 
 |-  ( R e. Ring -> ( SubRing ` R ) = ( ( SubGrp ` R ) i^i ( SubMnd ` ( mulGrp ` R ) ) ) )
7 1 fvexi 
 |-  B e. _V
8 mreacs 
 |-  ( B e. _V -> ( ACS ` B ) e. ( Moore ` ~P B ) )
9 7 8 mp1i 
 |-  ( R e. Ring -> ( ACS ` B ) e. ( Moore ` ~P B ) )
10 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
11 1 subgacs 
 |-  ( R e. Grp -> ( SubGrp ` R ) e. ( ACS ` B ) )
12 10 11 syl 
 |-  ( R e. Ring -> ( SubGrp ` R ) e. ( ACS ` B ) )
13 2 ringmgp 
 |-  ( R e. Ring -> ( mulGrp ` R ) e. Mnd )
14 2 1 mgpbas 
 |-  B = ( Base ` ( mulGrp ` R ) )
15 14 submacs 
 |-  ( ( mulGrp ` R ) e. Mnd -> ( SubMnd ` ( mulGrp ` R ) ) e. ( ACS ` B ) )
16 13 15 syl 
 |-  ( R e. Ring -> ( SubMnd ` ( mulGrp ` R ) ) e. ( ACS ` B ) )
17 mreincl 
 |-  ( ( ( ACS ` B ) e. ( Moore ` ~P B ) /\ ( SubGrp ` R ) e. ( ACS ` B ) /\ ( SubMnd ` ( mulGrp ` R ) ) e. ( ACS ` B ) ) -> ( ( SubGrp ` R ) i^i ( SubMnd ` ( mulGrp ` R ) ) ) e. ( ACS ` B ) )
18 9 12 16 17 syl3anc 
 |-  ( R e. Ring -> ( ( SubGrp ` R ) i^i ( SubMnd ` ( mulGrp ` R ) ) ) e. ( ACS ` B ) )
19 6 18 eqeltrd 
 |-  ( R e. Ring -> ( SubRing ` R ) e. ( ACS ` B ) )