# 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}={\mathrm{Base}}_{{R}}$
isring.g ${⊢}{G}={\mathrm{mulGrp}}_{{R}}$
isring.p
isring.t
Assertion isring

### Proof

Step Hyp Ref Expression
1 isring.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
2 isring.g ${⊢}{G}={\mathrm{mulGrp}}_{{R}}$
3 isring.p
4 isring.t
5 fveq2 ${⊢}{r}={R}\to {\mathrm{mulGrp}}_{{r}}={\mathrm{mulGrp}}_{{R}}$
6 5 2 syl6eqr ${⊢}{r}={R}\to {\mathrm{mulGrp}}_{{r}}={G}$
7 6 eleq1d ${⊢}{r}={R}\to \left({\mathrm{mulGrp}}_{{r}}\in \mathrm{Mnd}↔{G}\in \mathrm{Mnd}\right)$
8 fvexd ${⊢}{r}={R}\to {\mathrm{Base}}_{{r}}\in \mathrm{V}$
9 fveq2 ${⊢}{r}={R}\to {\mathrm{Base}}_{{r}}={\mathrm{Base}}_{{R}}$
10 9 1 syl6eqr ${⊢}{r}={R}\to {\mathrm{Base}}_{{r}}={B}$
11 fvexd ${⊢}\left({r}={R}\wedge {b}={B}\right)\to {+}_{{r}}\in \mathrm{V}$
12 simpl ${⊢}\left({r}={R}\wedge {b}={B}\right)\to {r}={R}$
13 12 fveq2d ${⊢}\left({r}={R}\wedge {b}={B}\right)\to {+}_{{r}}={+}_{{R}}$
14 13 3 syl6eqr
15 fvexd
16 simpll
17 16 fveq2d
18 17 4 syl6eqr
19 simpllr
20 simpr
21 eqidd
22 simplr
23 22 oveqd
24 20 21 23 oveq123d
25 20 oveqd
26 20 oveqd
27 22 25 26 oveq123d
28 24 27 eqeq12d
29 22 oveqd
30 eqidd
31 20 29 30 oveq123d
32 20 oveqd
33 22 26 32 oveq123d
34 31 33 eqeq12d
35 28 34 anbi12d
36 19 35 raleqbidv
37 19 36 raleqbidv
38 19 37 raleqbidv
39 15 18 38 sbcied2
40 11 14 39 sbcied2
41 8 10 40 sbcied2
42 7 41 anbi12d
43 df-ring
44 42 43 elrab2
45 3anass
46 44 45 bitr4i