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 = Base R
isringd.p φ + ˙ = + R
isringd.t φ · ˙ = R
isringd.g φ R Grp
isringd.c φ x B y B x · ˙ y B
isringd.a φ x B y B z B x · ˙ y · ˙ z = x · ˙ y · ˙ z
isringd.d φ x B y B z B x · ˙ y + ˙ z = x · ˙ y + ˙ x · ˙ z
isringd.e φ x B y B z B x + ˙ y · ˙ z = x · ˙ z + ˙ y · ˙ z
isringd.u φ 1 ˙ B
isringd.i φ x B 1 ˙ · ˙ x = x
isringd.h φ x B x · ˙ 1 ˙ = x
iscrngd.c φ x B y B x · ˙ y = y · ˙ x
Assertion iscrngd φ R CRing

Proof

Step Hyp Ref Expression
1 isringd.b φ B = Base R
2 isringd.p φ + ˙ = + R
3 isringd.t φ · ˙ = R
4 isringd.g φ R Grp
5 isringd.c φ x B y B x · ˙ y B
6 isringd.a φ x B y B z B x · ˙ y · ˙ z = x · ˙ y · ˙ z
7 isringd.d φ x B y B z B x · ˙ y + ˙ z = x · ˙ y + ˙ x · ˙ z
8 isringd.e φ x B y B z B x + ˙ y · ˙ z = x · ˙ z + ˙ y · ˙ z
9 isringd.u φ 1 ˙ B
10 isringd.i φ x B 1 ˙ · ˙ x = x
11 isringd.h φ x B x · ˙ 1 ˙ = x
12 iscrngd.c φ x B y B x · ˙ y = y · ˙ x
13 1 2 3 4 5 6 7 8 9 10 11 isringd φ R Ring
14 eqid mulGrp R = mulGrp R
15 eqid Base R = Base R
16 14 15 mgpbas Base R = Base mulGrp R
17 1 16 eqtrdi φ B = Base mulGrp R
18 eqid R = R
19 14 18 mgpplusg R = + mulGrp R
20 3 19 eqtrdi φ · ˙ = + mulGrp R
21 17 20 5 6 9 10 11 ismndd φ mulGrp R Mnd
22 17 20 21 12 iscmnd φ mulGrp R CMnd
23 14 iscrng R CRing R Ring mulGrp R CMnd
24 13 22 23 sylanbrc φ R CRing