Metamath Proof Explorer


Theorem iscrngd

Description: Properties that determine a commutative ring. (Contributed by Mario Carneiro, 7-Jan-2015)

Ref Expression
Hypotheses isringd.b φB=BaseR
isringd.p φ+˙=+R
isringd.t φ·˙=R
isringd.g φRGrp
isringd.c φxByBx·˙yB
isringd.a φxByBzBx·˙y·˙z=x·˙y·˙z
isringd.d φxByBzBx·˙y+˙z=x·˙y+˙x·˙z
isringd.e φxByBzBx+˙y·˙z=x·˙z+˙y·˙z
isringd.u φ1˙B
isringd.i φxB1˙·˙x=x
isringd.h φxBx·˙1˙=x
iscrngd.c φxByBx·˙y=y·˙x
Assertion iscrngd φRCRing

Proof

Step Hyp Ref Expression
1 isringd.b φB=BaseR
2 isringd.p φ+˙=+R
3 isringd.t φ·˙=R
4 isringd.g φRGrp
5 isringd.c φxByBx·˙yB
6 isringd.a φxByBzBx·˙y·˙z=x·˙y·˙z
7 isringd.d φxByBzBx·˙y+˙z=x·˙y+˙x·˙z
8 isringd.e φxByBzBx+˙y·˙z=x·˙z+˙y·˙z
9 isringd.u φ1˙B
10 isringd.i φxB1˙·˙x=x
11 isringd.h φxBx·˙1˙=x
12 iscrngd.c φxByBx·˙y=y·˙x
13 1 2 3 4 5 6 7 8 9 10 11 isringd φRRing
14 eqid mulGrpR=mulGrpR
15 eqid BaseR=BaseR
16 14 15 mgpbas BaseR=BasemulGrpR
17 1 16 eqtrdi φB=BasemulGrpR
18 eqid R=R
19 14 18 mgpplusg R=+mulGrpR
20 3 19 eqtrdi φ·˙=+mulGrpR
21 17 20 5 6 9 10 11 ismndd φmulGrpRMnd
22 17 20 21 12 iscmnd φmulGrpRCMnd
23 14 iscrng RCRingRRingmulGrpRCMnd
24 13 22 23 sylanbrc φRCRing