Metamath Proof Explorer


Theorem isringd

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

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 )
Assertion isringd
|- ( ph -> R e. Ring )

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