Description: Properties that determine a commutative ring. (Contributed by Mario Carneiro, 7-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | isringd.b | |
|
isringd.p | |
||
isringd.t | |
||
isringd.g | |
||
isringd.c | |
||
isringd.a | |
||
isringd.d | |
||
isringd.e | |
||
isringd.u | |
||
isringd.i | |
||
isringd.h | |
||
iscrngd.c | |
||
Assertion | iscrngd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isringd.b | |
|
2 | isringd.p | |
|
3 | isringd.t | |
|
4 | isringd.g | |
|
5 | isringd.c | |
|
6 | isringd.a | |
|
7 | isringd.d | |
|
8 | isringd.e | |
|
9 | isringd.u | |
|
10 | isringd.i | |
|
11 | isringd.h | |
|
12 | iscrngd.c | |
|
13 | 1 2 3 4 5 6 7 8 9 10 11 | isringd | |
14 | eqid | |
|
15 | eqid | |
|
16 | 14 15 | mgpbas | |
17 | 1 16 | eqtrdi | |
18 | eqid | |
|
19 | 14 18 | mgpplusg | |
20 | 3 19 | eqtrdi | |
21 | 17 20 5 6 9 10 11 | ismndd | |
22 | 17 20 21 12 | iscmnd | |
23 | 14 | iscrng | |
24 | 13 22 23 | sylanbrc | |