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 )