Metamath Proof Explorer


Theorem isringd

Description: Properties that determine a ring. (Contributed by NM, 2-Aug-2013)

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
Assertion isringd φ R Ring

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 eqid mulGrp R = mulGrp R
13 eqid Base R = Base R
14 12 13 mgpbas Base R = Base mulGrp R
15 1 14 eqtrdi φ B = Base mulGrp R
16 eqid R = R
17 12 16 mgpplusg R = + mulGrp R
18 3 17 eqtrdi φ · ˙ = + mulGrp R
19 15 18 5 6 9 10 11 ismndd φ mulGrp R Mnd
20 1 eleq2d φ x B x Base R
21 1 eleq2d φ y B y Base R
22 1 eleq2d φ z B z Base R
23 20 21 22 3anbi123d φ x B y B z B x Base R y Base R z Base R
24 23 biimpar φ x Base R y Base R z Base R x B y B z B
25 3 adantr φ x B y B z B · ˙ = R
26 eqidd φ x B y B z B x = x
27 2 oveqdr φ x B y B z B y + ˙ z = y + R z
28 25 26 27 oveq123d φ x B y B z B x · ˙ y + ˙ z = x R y + R z
29 2 adantr φ x B y B z B + ˙ = + R
30 3 oveqdr φ x B y B z B x · ˙ y = x R y
31 3 oveqdr φ x B y B z B x · ˙ z = x R z
32 29 30 31 oveq123d φ x B y B z B x · ˙ y + ˙ x · ˙ z = x R y + R x R z
33 7 28 32 3eqtr3d φ x B y B z B x R y + R z = x R y + R x R z
34 2 oveqdr φ x B y B z B x + ˙ y = x + R y
35 eqidd φ x B y B z B z = z
36 25 34 35 oveq123d φ x B y B z B x + ˙ y · ˙ z = x + R y R z
37 3 oveqdr φ x B y B z B y · ˙ z = y R z
38 29 31 37 oveq123d φ x B y B z B x · ˙ z + ˙ y · ˙ z = x R z + R y R z
39 8 36 38 3eqtr3d φ x B y B z B x + R y R z = x R z + R y R z
40 33 39 jca φ x B y B z B x R y + R z = x R y + R x R z x + R y R z = x R z + R y R z
41 24 40 syldan φ x Base R y Base R z Base R x R y + R z = x R y + R x R z x + R y R z = x R z + R y R z
42 41 ralrimivvva φ x Base R y Base R z Base R x R y + R z = x R y + R x R z x + R y R z = x R z + R y R z
43 eqid + R = + R
44 13 12 43 16 isring R Ring R Grp mulGrp R Mnd x Base R y Base R z Base R x R y + R z = x R y + R x R z x + R y R z = x R z + R y R z
45 4 19 42 44 syl3anbrc φ R Ring