Metamath Proof Explorer


Theorem iscrngd

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

Ref Expression
Hypotheses isringd.b
|- ( ph -> B = ( Base ` R ) )
isringd.p
|- ( ph -> .+ = ( +g ` R ) )
isringd.t
|- ( ph -> .x. = ( .r ` R ) )
isringd.g
|- ( ph -> R e. Grp )
isringd.c
|- ( ( ph /\ x e. B /\ y e. B ) -> ( x .x. y ) e. B )
isringd.a
|- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) )
isringd.d
|- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) )
isringd.e
|- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) )
isringd.u
|- ( ph -> .1. e. B )
isringd.i
|- ( ( ph /\ x e. B ) -> ( .1. .x. x ) = x )
isringd.h
|- ( ( ph /\ x e. B ) -> ( x .x. .1. ) = x )
iscrngd.c
|- ( ( ph /\ x e. B /\ y e. B ) -> ( x .x. y ) = ( y .x. x ) )
Assertion iscrngd
|- ( ph -> R e. CRing )

Proof

Step Hyp Ref Expression
1 isringd.b
 |-  ( ph -> B = ( Base ` R ) )
2 isringd.p
 |-  ( ph -> .+ = ( +g ` R ) )
3 isringd.t
 |-  ( ph -> .x. = ( .r ` R ) )
4 isringd.g
 |-  ( ph -> R e. Grp )
5 isringd.c
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( x .x. y ) e. B )
6 isringd.a
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) )
7 isringd.d
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) )
8 isringd.e
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) )
9 isringd.u
 |-  ( ph -> .1. e. B )
10 isringd.i
 |-  ( ( ph /\ x e. B ) -> ( .1. .x. x ) = x )
11 isringd.h
 |-  ( ( ph /\ x e. B ) -> ( x .x. .1. ) = x )
12 iscrngd.c
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( x .x. y ) = ( y .x. x ) )
13 1 2 3 4 5 6 7 8 9 10 11 isringd
 |-  ( ph -> R e. 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
 |-  ( ph -> B = ( Base ` ( mulGrp ` R ) ) )
18 eqid
 |-  ( .r ` R ) = ( .r ` R )
19 14 18 mgpplusg
 |-  ( .r ` R ) = ( +g ` ( mulGrp ` R ) )
20 3 19 eqtrdi
 |-  ( ph -> .x. = ( +g ` ( mulGrp ` R ) ) )
21 17 20 5 6 9 10 11 ismndd
 |-  ( ph -> ( mulGrp ` R ) e. Mnd )
22 17 20 21 12 iscmnd
 |-  ( ph -> ( mulGrp ` R ) e. CMnd )
23 14 iscrng
 |-  ( R e. CRing <-> ( R e. Ring /\ ( mulGrp ` R ) e. CMnd ) )
24 13 22 23 sylanbrc
 |-  ( ph -> R e. CRing )