Description: Closure property of subrings. (Contributed by Stefan O'Rear, 12-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | subrgacs.b | |
|
Assertion | subrgacs | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | subrgacs.b | |
|
2 | eqid | |
|
3 | 2 | issubrg3 | |
4 | elin | |
|
5 | 3 4 | bitr4di | |
6 | 5 | eqrdv | |
7 | 1 | fvexi | |
8 | mreacs | |
|
9 | 7 8 | mp1i | |
10 | ringgrp | |
|
11 | 1 | subgacs | |
12 | 10 11 | syl | |
13 | 2 | ringmgp | |
14 | 2 1 | mgpbas | |
15 | 14 | submacs | |
16 | 13 15 | syl | |
17 | mreincl | |
|
18 | 9 12 16 17 | syl3anc | |
19 | 6 18 | eqeltrd | |