Description: A subring is an additive subgroup which is also a multiplicative submonoid. (Contributed by Mario Carneiro, 7-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | issubrg3.m | |
|
Assertion | issubrg3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | issubrg3.m | |
|
2 | eqid | |
|
3 | eqid | |
|
4 | eqid | |
|
5 | 2 3 4 | issubrg2 | |
6 | 3anass | |
|
7 | 5 6 | bitrdi | |
8 | 1 | ringmgp | |
9 | 2 | subgss | |
10 | 1 2 | mgpbas | |
11 | 1 3 | ringidval | |
12 | 1 4 | mgpplusg | |
13 | 10 11 12 | issubm | |
14 | 3anass | |
|
15 | 13 14 | bitrdi | |
16 | 15 | baibd | |
17 | 8 9 16 | syl2an | |
18 | 17 | pm5.32da | |
19 | 7 18 | bitr4d | |