Metamath Proof Explorer

Theorem isring

Description: The predicate "is a (unital) ring". Definition of ring with unit in Schechter p. 187. (Contributed by NM, 18-Oct-2012) (Revised by Mario Carneiro, 6-Jan-2015)

Ref Expression
Hypotheses isring.b 
|- B = ( Base ` R )
isring.g 
|- G = ( mulGrp ` R )
isring.p 
|- .+ = ( +g ` R )
isring.t 
|- .x. = ( .r ` R )
Assertion isring 
|- ( R e. Ring <-> ( R e. Grp /\ G e. Mnd /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isring.b 
 |-  B = ( Base ` R )
2 isring.g 
 |-  G = ( mulGrp ` R )
3 isring.p 
 |-  .+ = ( +g ` R )
4 isring.t 
 |-  .x. = ( .r ` R )
5 fveq2 
 |-  ( r = R -> ( mulGrp ` r ) = ( mulGrp ` R ) )
6 5 2 eqtr4di 
 |-  ( r = R -> ( mulGrp ` r ) = G )
7 6 eleq1d 
 |-  ( r = R -> ( ( mulGrp ` r ) e. Mnd <-> G e. Mnd ) )
8 fvexd 
 |-  ( r = R -> ( Base ` r ) e. _V )
9 fveq2 
 |-  ( r = R -> ( Base ` r ) = ( Base ` R ) )
10 9 1 eqtr4di 
 |-  ( r = R -> ( Base ` r ) = B )
11 fvexd 
 |-  ( ( r = R /\ b = B ) -> ( +g ` r ) e. _V )
12 simpl 
 |-  ( ( r = R /\ b = B ) -> r = R )
13 12 fveq2d 
 |-  ( ( r = R /\ b = B ) -> ( +g ` r ) = ( +g ` R ) )
14 13 3 eqtr4di 
 |-  ( ( r = R /\ b = B ) -> ( +g ` r ) = .+ )
15 fvexd 
 |-  ( ( ( r = R /\ b = B ) /\ p = .+ ) -> ( .r ` r ) e. _V )
16 simpll 
 |-  ( ( ( r = R /\ b = B ) /\ p = .+ ) -> r = R )
17 16 fveq2d 
 |-  ( ( ( r = R /\ b = B ) /\ p = .+ ) -> ( .r ` r ) = ( .r ` R ) )
18 17 4 eqtr4di 
 |-  ( ( ( r = R /\ b = B ) /\ p = .+ ) -> ( .r ` r ) = .x. )
19 simpllr 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> b = B )
20 simpr 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> t = .x. )
21 eqidd 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> x = x )
22 simplr 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> p = .+ )
23 22 oveqd 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> ( y p z ) = ( y .+ z ) )
24 20 21 23 oveq123d 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> ( x t ( y p z ) ) = ( x .x. ( y .+ z ) ) )
25 20 oveqd 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> ( x t y ) = ( x .x. y ) )
26 20 oveqd 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> ( x t z ) = ( x .x. z ) )
27 22 25 26 oveq123d 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> ( ( x t y ) p ( x t z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) )
28 24 27 eqeq12d 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) <-> ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) ) )
29 22 oveqd 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> ( x p y ) = ( x .+ y ) )
30 eqidd 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> z = z )
31 20 29 30 oveq123d 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> ( ( x p y ) t z ) = ( ( x .+ y ) .x. z ) )
32 20 oveqd 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> ( y t z ) = ( y .x. z ) )
33 22 26 32 oveq123d 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> ( ( x t z ) p ( y t z ) ) = ( ( x .x. z ) .+ ( y .x. z ) ) )
34 31 33 eqeq12d 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> ( ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) <-> ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) )
35 28 34 anbi12d 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> ( ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) <-> ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) )
36 19 35 raleqbidv 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> ( A. z e. b ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) <-> A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) )
37 19 36 raleqbidv 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> ( A. y e. b A. z e. b ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) <-> A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) )
38 19 37 raleqbidv 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> ( A. x e. b A. y e. b A. z e. b ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) <-> A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) )
39 15 18 38 sbcied2 
 |-  ( ( ( r = R /\ b = B ) /\ p = .+ ) -> ( [. ( .r ` r ) / t ]. A. x e. b A. y e. b A. z e. b ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) <-> A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) )
40 11 14 39 sbcied2 
 |-  ( ( r = R /\ b = B ) -> ( [. ( +g ` r ) / p ]. [. ( .r ` r ) / t ]. A. x e. b A. y e. b A. z e. b ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) <-> A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) )
41 8 10 40 sbcied2 
 |-  ( r = R -> ( [. ( Base ` r ) / b ]. [. ( +g ` r ) / p ]. [. ( .r ` r ) / t ]. A. x e. b A. y e. b A. z e. b ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) <-> A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) )
42 7 41 anbi12d 
 |-  ( r = R -> ( ( ( mulGrp ` r ) e. Mnd /\ [. ( Base ` r ) / b ]. [. ( +g ` r ) / p ]. [. ( .r ` r ) / t ]. A. x e. b A. y e. b A. z e. b ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) ) <-> ( G e. Mnd /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) ) )
43 df-ring 
 |-  Ring = { r e. Grp | ( ( mulGrp ` r ) e. Mnd /\ [. ( Base ` r ) / b ]. [. ( +g ` r ) / p ]. [. ( .r ` r ) / t ]. A. x e. b A. y e. b A. z e. b ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) ) }
44 42 43 elrab2 
 |-  ( R e. Ring <-> ( R e. Grp /\ ( G e. Mnd /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) ) )
45 3anass 
 |-  ( ( R e. Grp /\ G e. Mnd /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) <-> ( R e. Grp /\ ( G e. Mnd /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) ) )
46 44 45 bitr4i 
 |-  ( R e. Ring <-> ( R e. Grp /\ G e. Mnd /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) )