Metamath Proof Explorer

Theorem dfring3

Description: The predicate "is a (unital) ring" based on a ring being abelian and with the definition of a monoid expanded. (Contributed by Jeff Hankins, 21-Nov-2006) (Revised by AV, 24-Aug-2026)

Ref Expression
Hypotheses isringrng.b 
|- B = ( Base ` R )
isringrng.t 
|- .x. = ( .r ` R )
dfring2.g 
|- G = ( mulGrp ` R )
dfring2.p 
|- .+ = ( +g ` R )
Assertion dfring3 
|- ( R e. Ring <-> ( ( R e. Abel /\ G e. Mgm ) /\ A. x e. B A. y e. B A. z e. B ( ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) /\ ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) )

Proof

Step Hyp Ref Expression
1 isringrng.b 
 |-  B = ( Base ` R )
2 isringrng.t 
 |-  .x. = ( .r ` R )
3 dfring2.g 
 |-  G = ( mulGrp ` R )
4 dfring2.p 
 |-  .+ = ( +g ` R )
5 1 2 3 4 dfring2 
 |-  ( R e. Ring <-> ( R e. Abel /\ 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 ) ) ) ) )
6 3 1 mgpbas 
 |-  B = ( Base ` G )
7 3 2 mgpplusg 
 |-  .x. = ( +g ` G )
8 6 7 ismnddef 
 |-  ( G e. Mnd <-> ( G e. Smgrp /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) )
9 6 7 issgrp 
 |-  ( G e. Smgrp <-> ( G e. Mgm /\ A. x e. B A. y e. B A. z e. B ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) ) )
10 8 9 bianbi 
 |-  ( G e. Mnd <-> ( ( G e. Mgm /\ A. x e. B A. y e. B A. z e. B ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) ) /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) )
11 10 anbi1i 
 |-  ( ( 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 ) ) ) ) <-> ( ( ( G e. Mgm /\ A. x e. B A. y e. B A. z e. B ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) ) /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) /\ 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 ) ) ) ) )
12 anass 
 |-  ( ( ( ( G e. Mgm /\ A. x e. B A. y e. B A. z e. B ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) ) /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) /\ 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 ) ) ) ) <-> ( ( G e. Mgm /\ A. x e. B A. y e. B A. z e. B ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) ) /\ ( E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) /\ 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 ) ) ) ) ) )
13 anass 
 |-  ( ( ( G e. Mgm /\ A. x e. B A. y e. B A. z e. B ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) ) /\ ( E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) /\ 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 ) ) ) ) ) <-> ( G e. Mgm /\ ( A. x e. B A. y e. B A. z e. B ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) /\ ( E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) /\ 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 ) ) ) ) ) ) )
14 12 13 bitri 
 |-  ( ( ( ( G e. Mgm /\ A. x e. B A. y e. B A. z e. B ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) ) /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) /\ 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 ) ) ) ) <-> ( G e. Mgm /\ ( A. x e. B A. y e. B A. z e. B ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) /\ ( E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) /\ 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 ) ) ) ) ) ) )
15 ancom 
 |-  ( ( E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) /\ 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 ) ) ) ) <-> ( 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 ) ) ) /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) )
16 15 anbi2i 
 |-  ( ( A. x e. B A. y e. B A. z e. B ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) /\ ( E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) /\ 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 ) ) ) ) ) <-> ( A. x e. B A. y e. B A. z e. B ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. 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 ) ) ) /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) ) )
17 anass 
 |-  ( ( ( A. x e. B A. y e. B A. z e. B ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. 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 ) ) ) ) /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) <-> ( A. x e. B A. y e. B A. z e. B ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. 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 ) ) ) /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) ) )
18 r19.26-2 
 |-  ( A. x e. B A. y e. B ( A. z e. B ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. 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 ) ) ) ) <-> ( A. x e. B A. y e. B A. z e. B ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. 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 ) ) ) ) )
19 r19.26 
 |-  ( A. z e. B ( ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) /\ ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) <-> ( A. z e. B ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. 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 ) ) ) ) )
20 3anass 
 |-  ( ( ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) /\ ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) <-> ( ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) /\ ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) )
21 20 bicomi 
 |-  ( ( ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) /\ ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) <-> ( ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) /\ ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) )
22 21 ralbii 
 |-  ( A. z e. B ( ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) /\ ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) <-> A. z e. B ( ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) /\ ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) )
23 19 22 bitr3i 
 |-  ( ( A. z e. B ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. 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 ) ) ) ) <-> A. z e. B ( ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) /\ ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) )
24 23 2ralbii 
 |-  ( A. x e. B A. y e. B ( A. z e. B ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. 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 ) ) ) ) <-> A. x e. B A. y e. B A. z e. B ( ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) /\ ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) )
25 18 24 bitr3i 
 |-  ( ( A. x e. B A. y e. B A. z e. B ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. 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 ) ) ) ) <-> A. x e. B A. y e. B A. z e. B ( ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) /\ ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) )
26 25 anbi1i 
 |-  ( ( ( A. x e. B A. y e. B A. z e. B ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. 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 ) ) ) ) /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) <-> ( A. x e. B A. y e. B A. z e. B ( ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) /\ ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) )
27 17 26 bitr3i 
 |-  ( ( A. x e. B A. y e. B A. z e. B ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. 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 ) ) ) /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) ) <-> ( A. x e. B A. y e. B A. z e. B ( ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) /\ ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) )
28 16 27 bitri 
 |-  ( ( A. x e. B A. y e. B A. z e. B ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) /\ ( E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) /\ 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 ) ) ) ) ) <-> ( A. x e. B A. y e. B A. z e. B ( ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) /\ ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) )
29 28 anbi2i 
 |-  ( ( G e. Mgm /\ ( A. x e. B A. y e. B A. z e. B ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) /\ ( E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) /\ 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 ) ) ) ) ) ) <-> ( G e. Mgm /\ ( A. x e. B A. y e. B A. z e. B ( ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) /\ ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) ) )
30 14 29 bitri 
 |-  ( ( ( ( G e. Mgm /\ A. x e. B A. y e. B A. z e. B ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) ) /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) /\ 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 ) ) ) ) <-> ( G e. Mgm /\ ( A. x e. B A. y e. B A. z e. B ( ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) /\ ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) ) )
31 11 30 bitri 
 |-  ( ( 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 ) ) ) ) <-> ( G e. Mgm /\ ( A. x e. B A. y e. B A. z e. B ( ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) /\ ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) ) )
32 31 anbi2i 
 |-  ( ( R e. Abel /\ ( 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. Abel /\ ( G e. Mgm /\ ( A. x e. B A. y e. B A. z e. B ( ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) /\ ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) ) ) )
33 3anass 
 |-  ( ( R e. Abel /\ 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. Abel /\ ( 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 ) ) ) ) ) )
34 3anass 
 |-  ( ( ( R e. Abel /\ G e. Mgm ) /\ A. x e. B A. y e. B A. z e. B ( ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) /\ ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) <-> ( ( R e. Abel /\ G e. Mgm ) /\ ( A. x e. B A. y e. B A. z e. B ( ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) /\ ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) ) )
35 anass 
 |-  ( ( ( R e. Abel /\ G e. Mgm ) /\ ( A. x e. B A. y e. B A. z e. B ( ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) /\ ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) ) <-> ( R e. Abel /\ ( G e. Mgm /\ ( A. x e. B A. y e. B A. z e. B ( ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) /\ ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) ) ) )
36 34 35 bitri 
 |-  ( ( ( R e. Abel /\ G e. Mgm ) /\ A. x e. B A. y e. B A. z e. B ( ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) /\ ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) <-> ( R e. Abel /\ ( G e. Mgm /\ ( A. x e. B A. y e. B A. z e. B ( ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) /\ ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) ) ) )
37 32 33 36 3bitr4i 
 |-  ( ( R e. Abel /\ 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. Abel /\ G e. Mgm ) /\ A. x e. B A. y e. B A. z e. B ( ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) /\ ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) )
38 5 37 bitri 
 |-  ( R e. Ring <-> ( ( R e. Abel /\ G e. Mgm ) /\ A. x e. B A. y e. B A. z e. B ( ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) /\ ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) )