This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )